References

  1. 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.
  2. David Baelde (2012): Least and greatest fixed points in linear logic. ACM Trans. on Computational Logic 13(1), doi:10.1145/2071368.2071370.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. Jean-Yves Girard (1987): Linear Logic. Theoretical Computer Science 50, pp. 1–102, doi:10.1016/0304-3975(87)90045-4.
  8. Jean-Yves Girard (1991): A new constructive logic: classical logic. Math. Structures in Comp. Science 1, pp. 255–296, doi:10.1017/S0960129500001328.
  9. Jean-Yves Girard (1992): A Fixpoint Theorem in Linear Logic. An email posting to the mailing list linear@cs.stanford.edu.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org