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