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