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

@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}

  }

@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}

}

@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}

}

@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{KahleOitavem13,

  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},

  url       = {http://dx.doi.org/10.1016/j.apal.2012.05.006},

  doi       = {10.1016/j.apal.2012.05.006},

  timestamp = {Sat, 20 Apr 2013 19:07:47 +0200},

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

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

@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}

  }

@unpublished{BaiDas,

  TITLE = {Free-cut elimination in linear logic and an application to a feasible arithmetic},

  AUTHOR = {Baillot, Patrick and Das, Anupam},

  URL = {https://hal.archives-ouvertes.fr/hal-01316754},

  NOTE = {Preprint},

  YEAR = {2016},

  PDF = {https://hal.archives-ouvertes.fr/hal-01316754/file/main.pdf},

  HAL_ID = {hal-01316754},

  HAL_VERSION = {v1},

	}