@article(andreoli92jlc,
author = {Jean-Marc Andreoli},
year = {1992},
title = {Logic Programming with Focusing Proofs in Linear Logic},
journal = {J. of Logic and Computation},
volume = {2},
number = {3},
pages = {297--347},
doi = {10.1093/logcom/2.3.297},
)
@article(baelde12tocl,
author = {David Baelde},
year = {2012},
title = {Least and greatest fixed points in linear logic},
journal = {ACM Trans.\ on Computational Logic},
volume = {13},
number = {1},
doi = {10.1145/2071368.2071370},
)
@inproceedings(baelde07cade,
author = {David Baelde and Andrew Gacek and Dale Miller and Gopalan Nadathur and Alwen Tiu},
year = {2007},
title = {The {Bedwyr} system for model checking over syntactic expressions},
editor = {F. Pfenning},
booktitle = {21th Conf.\ on Automated Deduction (CADE)},
series = {LNAI},
volume = {4603},
publisher = {Springer},
address = {New York},
pages = {391--397},
doi = {10.1007/978-3-540-73595-3\_28},
)
@inproceedings(baelde07lpar,
author = {David Baelde and Dale Miller},
year = {2007},
title = {Least and greatest fixed points in linear logic},
editor = {N. Dershowitz and A. Voronkov},
booktitle = {International Conference on Logic for Programming and Automated Reasoning (LPAR)},
series = {LNCS},
volume = {4790},
pages = {92--106},
doi = {10.1007/978-3-540-75560-9\_9},
)
@inproceedings(emerson08bmc,
author = {E. Allen Emerson},
year = {2008},
title = {The Beginning of Model Checking: {A} Personal Perspective},
editor = {Orna Grumberg and Helmut Veith},
booktitle = {25 Years of Model Checking - History, Achievements, Perspectives},
series = {Lecture Notes in Computer Science},
volume = {5000},
publisher = {Springer},
pages = {27--45},
doi = {10.1007/978-3-540-69850-0\_2},
)
@incollection(gentzen35,
author = {Gerhard Gentzen},
year = {1935},
title = {Investigations into Logical Deduction},
editor = {M. E. Szabo},
booktitle = {{The Collected Papers of Gerhard Gentzen}},
publisher = {North-Holland},
address = {Amsterdam},
pages = {68--131},
doi = {10.1007/BF01201353},
)
@article(girard87tcs,
author = {Jean-Yves Girard},
year = {1987},
title = {Linear Logic},
journal = {Theoretical Computer Science},
volume = {50},
pages = {1--102},
doi = {10.1016/0304-3975(87)90045-4},
)
@article(girard91mscs,
author = {Jean-Yves Girard},
year = {1991},
title = {A new constructive logic: classical logic},
journal = {Math. Structures in Comp. Science},
volume = {1},
pages = {255--296},
doi = {10.1017/S0960129500001328},
)
@unpublished(girard92mail,
author = {Jean-Yves Girard},
year = {1992},
title = {A Fixpoint Theorem in Linear Logic},
note = {An email posting to the mailing list linear@cs.stanford.edu},
)
@article(kanovich95apal,
author = {Max I. Kanovich},
year = {1995},
title = {Petri Nets, {Horn} programs, {Linear} {Logic} and vector games},
journal = {Annals of Pure and Applied Logic},
volume = {75},
number = {1--2},
pages = {107--135},
doi = {10.1016/0168-0072(94)00060-G},
)
@article(mcdowell00tcs,
author = {Raymond McDowell and Dale Miller},
year = {2000},
title = {Cut-elimination for a logic with definitions and induction},
journal = {Theoretical Computer Science},
volume = {232},
pages = {91--119},
doi = {10.1016/S0304-3975(99)00171-1},
)
@article(miller05tocl,
author = {Dale Miller and Alwen Tiu},
year = {2005},
title = {A proof theory for generic judgments},
journal = {ACM Trans.\ on Computational Logic},
volume = {6},
number = {4},
pages = {749--783},
doi = {10.1145/1094622.1094628},
)
@inproceedings(schroeder-heister93lics,
author = {Schroeder-Heister, Peter},
year = {1993},
title = {Rules of Definitional Reflection},
editor = {M. Vardi},
booktitle = {8th Symp.\ on Logic in Computer Science},
organization = {IEEE Computer Society Press},
publisher = {IEEE},
pages = {222--232},
doi = {10.1109/LICS.1993.287585},
)
@incollection(schwichtenberg77hml,
author = {Helmut Schwichtenberg},
year = {1977},
title = {Proof Theory: Some applications of cut-elimination},
editor = {J. Barwise},
booktitle = {Handbook of Mathematical Logic},
series = {Studies in Logic and the Foundations of Mathematics},
volume = {90},
publisher = {North-Holland},
address = {Amsterdam},
pages = {739--782},
doi = {10.1016/S0049-237X(08)71124-8},
)
@inproceedings(tiu05fguc,
author = {Alwen Tiu and Dale Miller},
year = {2005},
title = {A Proof Search Specification of the $\pi$-Calculus},
booktitle = {3rd Workshop on the Foundations of Global Ubiquitous Computing},
series = {ENTCS},
volume = {138},
pages = {79--101},
doi = {10.1016/j.entcs.2005.05.006},
)
@article(tiu10tocl,
author = {Alwen Tiu and Dale Miller},
year = {2010},
title = {Proof Search Specifications of Bisimulation and Modal Logics for the $\pi$-calculus},
journal = {ACM Trans.\ on Computational Logic},
volume = {11},
number = {2},
doi = {10.1145/1656242.1656248},
)
@article(tiu12jal,
author = {Alwen Tiu and Alberto Momigliano},
year = {2012},
title = {Cut elimination for a logic with induction and co-induction},
journal = {Journal of Applied Logic},
volume = {10},
number = {4},
pages = {330--367},
doi = {10.1016/j.jal.2012.07.007},
)