Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

@techreport{BaiDas17:fph-techreport,

	title={An implicit characterisation of the polynomial hierarchy in an unbounded arithmetic},

	author={Patrick Baillot and Anupam Das},

	year={2017},

	note={\url{http://www.anupamdas.com/fph-unbounded-arithmetic.pdf}}

	}

@incollection{bellantoni1995fph,

	title={Predicative recursion and the polytime hierarchy},

	author={Bellantoni, Stephen},

	booktitle={Feasible Mathematics II},

	pages={15--29},

	year={1995},

	publisher={Springer}

}

@inproceedings{Lasson11,

  author    = {Marc Lasson},

  title     = {Controlling Program Extraction in Light Logics},

  booktitle = {Proceedings of Typed Lambda Calculi and Applications - 10th International Conference,

               {TLCA} 2011},

  pages     = {123--137},

  series    = {LNCS},

  volume    = {6690},

  publisher = {Springer},

  year      = {2011}

 }

@inproceedings{Leivant95,

  author    = {Daniel Leivant},

  title     = {Ramified recurrence and computational complexity I: Word recurrence and poly-time},

  booktitle = {Feasible mathematics II}, 

    pages     = {320--343},

   publisher = {Birkhauser Boston},

  year      = {1995},

 }

@inproceedings{Marion11,

  author    = {Jean{-}Yves Marion},

  title     = {A Type System for Complexity Flow Analysis},

  booktitle = {Proceedings of the 26th Annual {IEEE} Symposium on Logic in Computer

               Science, {LICS} 2011},

  pages     = {123--132},

   publisher = {{IEEE} Computer Society},

  year      = {2011},

 }

@article{Hofmann03,

  author    = {Martin Hofmann},

  title     = {Linear types and non-size-increasing polynomial time computation},

  journal   = {Inf. Comput.},

  volume    = {183},

  number    = {1},

  pages     = {57--85},

  year      = {2003}

  }

@article{OstrinWainer05,

  author    = {Geoffrey E. Ostrin and

               Stanley S. Wainer},

  title     = {Elementary arithmetic},

  journal   = {Ann. Pure Appl. Logic},

  volume    = {133},

  number    = {1-3},

  pages     = {275--292},

  year      = {2005}

  }

@article{GaboardiMarionRonchi12,

  author    = {Marco Gaboardi and

               Jean{-}Yves Marion and

               Simona Ronchi Della Rocca},

  title     = {An Implicit Characterization of {PSPACE}},

  journal   = {{ACM} Trans. Comput. Log.},

  volume    = {13},

  number    = {2},

  pages     = {18:1--18:36},

  year      = {2012},

  url       = {http://doi.acm.org/10.1145/2159531.2159540},

  doi       = {10.1145/2159531.2159540},

  timestamp = {Mon, 09 Jan 2017 14:08:26 +0100},

  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tocl/GaboardiMR12},

  bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{Baelde12,

  author    = {David Baelde},

  title     = {Least and Greatest Fixed Points in Linear Logic},

  journal   = {{ACM} Trans. Comput. Log.},

  volume    = {13},

  number    = {1},

  pages     = {2},

  year      = {2012}

  }

@inproceedings{BaillotDas16,

  author    = {Patrick Baillot and

               Anupam Das},

  title     = {Free-Cut Elimination in Linear Logic and an Application to a Feasible

               Arithmetic},

  booktitle = {Proceedings of CSL 2016},

  pages     = {40:1--40:18},

    series    = {LIPIcs},

  volume    = {62},

  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},

  year      = {2016}

 }

@article{BellantoniCook92,

  author    = {Stephen Bellantoni and

               Stephen A. Cook},

  title     = {A New Recursion-Theoretic Characterization of the Polytime Functions},

  journal   = {Computational Complexity},

  volume    = {2},

  pages     = {97--110},

  year      = {1992}

 }

 @inproceedings{Bellantoni95,

  author    = {Stephen Bellantoni},

  title     = {Predicative Recursion and The Polytime Hierarchy},

  booktitle = {Feasible Mathematics II},

  pages     = {15-29},

    series    = {Progress in Computer Science and Applied Logic},

  volume    = {13},

  editors ={Clote P., Remmel J.B.}, 

  publisher = {Birkhauser Boston},

  year      = {1995}

 }

@inproceedings{Cobham,

	author = {Cobham, A.},

	title = {On the intrinsic computational difficulty of functions},

	booktitle={Proc. of the 1964 International Congress for Logic, Methodology, and the Philosophy

	of Science},

	year = {1964},

	issn = {0001-0782},

	pages = {24--30},

		publisher = {North Holland, Amsterdam}

} 

@article{Dershowitz:1979:PTM:359138.359142,

	author = {Dershowitz, Nachum and Manna, Zohar},

	title = {Proving Termination with Multiset Orderings},

	journal = {Commun. ACM},

	issue_date = {Aug. 1979},

	volume = {22},

	number = {8},

	month = aug,

	year = {1979},

	issn = {0001-0782},

	pages = {465--476},

	numpages = {12},

	doi = {10.1145/359138.359142},

	acmid = {359142},

	publisher = {ACM},

	address = {New York, NY, USA},

	keywords = {bags, multisets, production systems, program correctness, program termination, program verification, reduction rules, term rewriting systems, tree replacement systems, well-founded orderings, well-founded sets},

} 

@article{Beckmann11,

  author    = {Arnold Beckmann and

               Samuel R. Buss},

  title     = {Corrected upper bounds for free-cut elimination},

  journal   = {Theor. Comput. Sci.},

  volume    = {412},

  number    = {39},

  pages     = {5433--5445},

  year      = {2011}

}

@Phdthesis{BellantoniThesis,

author={Stephen J. Bellantoni},

title={Predicative Recursion and Computational Complexity},

school={University of Toronto},

year={1992}

}

@article{BelHof:02,

  author    = {Stephen Bellantoni and

               Martin Hofmann},

  title     = {A New "Feasible" Arithmetic},

  journal   = {J. Symb. Log.},

  volume    = {67},

  number    = {1},

  pages     = {104--116},

  year      = {2002}

 }

@article{Girard98,

  author    = {Jean{-}Yves Girard},

  title     = {Light Linear Logic},

  journal   = {Inf. Comput.},

  volume    = {143},

  number    = {2},

  pages     = {175--204},

  year      = {1998}

 }

@article{Hofmann00,

  author    = {Martin Hofmann},

  title     = {Safe recursion with higher types and BCK-algebra},

  journal   = {Ann. Pure Appl. Logic},

  volume    = {104},

  number    = {1-3},

  pages     = {113--166},

  year      = {2000}

  }

@article{Terui04,

  author    = {Kazushige Terui},

  title     = {Light Affine Set Theory: {A} Naive Set Theory of Polynomial Time},

  journal   = {Studia Logica},

  volume    = {77},

  number    = {1},

  pages     = {9--40},

  year      = {2004}

  }

@article{Leivant94:found-delin-ptime,

  author    = {Daniel Leivant},

  title     = {A Foundational Delineation of Poly-time},

  journal   = {Inf. Comput.},

  volume    = {110},

  number    = {2},

  pages     = {391--420},

  year      = {1994}

  }

@book{Buss86book,

  title={Bounded arithmetic},

  author={Buss, Samuel R},

  volume={86},

  year={1986},

  publisher={Bibliopolis}

}

@inproceedings{Leivant94:intrinsic-theories,

  author    = {Daniel Leivant},

  title={Intrinsic Theories and Computational Complexity},

  booktitle     = {Logical and Computational Complexity. Selected Papers. Logic and Computational

               Complexity, International Workshop {LCC} '94, Indianapolis, Indiana,

               USA, 13-16 October 1994},

  series    = {Lecture Notes in Computer Science},

  volume    = {960},

  pages={177-194},

  publisher = {Springer},

  year      = {1995}

}

@article{Cantini02,

  author    = {Andrea Cantini},

  title     = {Polytime, combinatory logic and positive safe induction},

  journal   = {Arch. Math. Log.},

  volume    = {41},

  number    = {2},

  pages     = {169--189},

  year      = {2002}

  }

@inproceedings{Girard94:lll,

  author    = {Jean{-}Yves Girard},

  title     = {Light Linear Logic},

  booktitle = {Logical and Computational Complexity. Selected Papers. {LCC} '94.},

  pages     = {145--176},

  year      = {1994},

  crossref  = {DBLP:conf/lcc/1994},

  doi       = {10.1007/3-540-60178-3_83},

  timestamp = {Thu, 23 Jun 2011 19:50:18 +0200},

  bibsource = {dblp computer science bibliography, http://dblp.org}

 }

@article{LincolnMSS92,

  author    = {Patrick Lincoln and

               John C. Mitchell and

               Andre Scedrov and

               Natarajan Shankar},

  title     = {Decision Problems for Propositional Linear Logic},

  journal   = {Ann. Pure Appl. Logic},

  volume    = {56},

  number    = {1-3},

  pages     = {239--311},

  year      = {1992}

 }

@article{Murawski04,

  author    = {Andrzej S. Murawski and

               C.{-}H. Luke Ong},

  title     = {On an interpretation of safe recursion in light affine logic},

  journal   = {Theor. Comput. Sci.},

  volume    = {318},

  number    = {1-2},

  pages     = {197--223},

  year      = {2004}

}

@article{Avron88,

  author    = {Arnon Avron},

  title     = {The Semantics and Proof Theory of Linear Logic},

  journal   = {Theor. Comput. Sci.},

  volume    = {57},

  pages     = {161--184},

  year      = {1988}

}

@article{GirardSS92:bounded-ll,

  author    = {Jean{-}Yves Girard and

               Andre Scedrov and

               Philip J. Scott},

  title     = {Bounded Linear Logic: {A} Modular Approach to Polynomial-Time Computability},

  journal   = {Theor. Comput. Sci.},

  volume    = {97},

  number    = {1},

  pages     = {1--66},

  year      = {1992}

 }

@article{Lafont04,

  author    = {Yves Lafont},

  title     = {Soft linear logic and polynomial time},

  journal   = {Theor. Comput. Sci.},

  volume    = {318},

  number    = {1-2},

  pages     = {163--180},

  year      = {2004}

 }

@inproceedings{Lasson11,

  author    = {Marc Lasson},

  title     = {Controlling Program Extraction in Light Logics},

  booktitle = {Typed Lambda Calculi and Applications - 10th International Conference,

               {TLCA} 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings},

  pages     = {123--137},

  series    = {Lecture Notes in Computer Science},

  volume    = {6690},

  publisher = {Springer},

  year      = {2011}

 }

@book{Takeuti87,

  title={Proof Theory},

  author={Takeuti, G.},

  year={1987},

  publisher={North-Holland, Amsterdam},

  note={and ed.}

}

@article{Girard87,

  author    = {Jean{-}Yves Girard},

  title     = {Linear Logic},

  journal   = {Theor. Comput. Sci.},

  volume    = {50},

  pages     = {1--102},

  year      = {1987},

  url       = {http://dx.doi.org/10.1016/0304-3975(87)90045-4},

  doi       = {10.1016/0304-3975(87)90045-4},

  timestamp = {Wed, 07 Sep 2011 12:13:20 +0200},

  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tcs/Girard87},

  bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{Buss98:intro-proof-theory,

  title={An introduction to proof theory},

  author={Buss, Samuel R},

  journal={Handbook of proof theory},

  volume={137},

  pages={1--78},

  year={1998}

}

@incollection{Miller04,

	year = {2004},

	author = {Dale Miller},

	editor = {Thomas Ehrhard},

	pages = {316--119},

	booktitle = {Linear Logic in Computer Science},

	publisher = {Cambridge University Press},

	title = {Overview of Linear Logic Programming}

}

@article{Andreoli92,

	author    = {Jean{-}Marc Andreoli},

	title     = {Logic Programming with Focusing Proofs in Linear Logic},

	journal   = {J. Log. Comput.},

	volume    = {2},

	number    = {3},

	pages     = {297--347},

	year      = {1992},

	doi       = {10.1093/logcom/2.3.297},

	timestamp = {Wed, 29 Jun 2011 15:52:24 +0200},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{FriedmanM92,

	author    = {Harvey Friedman and

	Robert K. Meyer},

	title     = {Whither Relevant Arithmetic?},

	journal   = {J. Symb. Log.},

	volume    = {57},

	number    = {3},

	pages     = {824--831},

	year      = {1992},

	doi       = {10.2307/2275433},

	timestamp = {Tue, 05 Aug 2014 16:36:24 +0200},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@inproceedings{Marion01,

  author    = {Jean{-}Yves Marion},

  title     = {Actual Arithmetic and Feasibility},

  booktitle = {Proceedings of Computer Science Logic (CSL 2001)} ,

    pages     = {115--129},

   series    = {Lecture Notes in Computer Science},

  volume    = {2142},

  publisher = {Springer},

  year      = {2001}

  }

@book{Cook:2010:LFP:1734064,

	author = {Cook, Stephen and Nguyen, Phuong},

	title = {Logical Foundations of Proof Complexity},

	year = {2010},

	isbn = {052151729X, 9780521517294},

	edition = {1st},

	publisher = {Cambridge University Press},

	address = {New York, NY, USA},

} 

@article{Baillot15,

	author    = {Patrick Baillot},

	title     = {On the expressivity of elementary linear logic: Characterizing Ptime

	and an exponential time hierarchy},

	journal   = {Inf. Comput.},

	volume    = {241},

	pages     = {3--31},

	year      = {2015}

	}

@inproceedings{BaiDas16,

	author    = {Patrick Baillot and

	Anupam Das},

	title     = {Free-Cut Elimination in Linear Logic and an Application to a Feasible

	Arithmetic},

	booktitle = {25th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2016,

	August 29 - September 1, 2016, Marseille, France},

	pages     = {40:1--40:18},

	year      = {2016},

	crossref  = {DBLP:conf/csl/2016},

	url       = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.40},

	doi       = {10.4230/LIPIcs.CSL.2016.40},

	timestamp = {Tue, 30 Aug 2016 15:55:10 +0200},

	biburl    = {http://dblp.uni-trier.de/rec/bib/conf/csl/BaillotD16},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@book{Krajicek:1996:BAP:225488,

	author = {Kraj\'{\i}\v{c}ek, Jan},

	title = {Bounded arithmetic, propositional logic, and complexity theory},

	year = {1995},

	isbn = {0-521-45205-8},

	publisher = {Cambridge University Press},

	address = {New York, NY, USA},

} 

@incollection{CloTak:1995:nc-ac,

	title={First order bounded arithmetic and small boolean circuit complexity classes},

	author={Clote, Peter and Takeuti, Gaisi},

	booktitle={Feasible Mathematics II},

	pages={154--218},

	year={1995},

	publisher={Springer}

}

@article{Strahm03,

  author    = {Thomas Strahm},

  title     = {Theories with self-application and computational complexity},

  journal   = {Inf. Comput.},

  volume    = {185},

  number    = {2},

  pages     = {263--297},

  year      = {2003}

  }

@article{Zambella96,

	author    = {Domenico Zambella},

	title     = {Notes on Polynomially Bounded Arithmetic},

	journal   = {J. Symb. Log.},

	volume    = {61},

	number    = {3},

	pages     = {942--966},

	year      = {1996},

	url       = {http://dx.doi.org/10.2307/2275794},

	doi       = {10.2307/2275794},

	timestamp = {Tue, 05 Aug 2014 16:36:22 +0200},

	biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jsyml/Zambella96},

	bibsource = {dblp computer science bibliography, http://dblp.org}

}

@article{KahOit:13:ph-levels,

	author    = {Reinhard Kahle and

	Isabel Oitavem},

	title     = {Applicative theories for the polynomial hierarchy of time and its

	levels},

	journal   = {Ann. Pure Appl. Logic},

	volume    = {164},

	number    = {6},

	pages     = {663--675},

	year      = {2013}

	}

@article{Buss:95:wfm-arith,

	title={The witness function method and provably recursive functions of Peano arithmetic},

	author={Buss, Samuel R},

	journal={Studies in Logic and the Foundations of Mathematics},

	volume={134},

	pages={29--68},

	year={1995},

	publisher={Elsevier}

}

	@article{troelstra1998realizability,

		title={Realizability},

		author={Troelstra, Anne Sjerp},

		journal={Handbook of Proof Theory},

		year={1998},

		publisher={North-Holland/Elsevier}

	}

	@article{avigad1998godel,

		title={G{\"o}del’s functional (“{D}ialectica”) interpretation},

		author={Avigad, Jeremy},

		journal={Handbook of Proof Theory},

		volume={137},

		year={1998}

	}