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, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu & Yuting Wang (2014): Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning 7(2), doi:10.6092/issn.1972-5787/4650.
  4. 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.
  5. Zakaria Chihani, Dale Miller & Fabien Renaud (2013): Foundational proof certificates in first-order logic. In: Maria Paola Bonacina: CADE 24: Conference on Automated Deduction 2013, LNAI 7898, pp. 162–177, doi:10.1007/978-3-642-38574-2_11.
  6. Edmund M. Clarke, Orna Grumberg & Doron A. Peled (1999): Model Checking. The MIT Press, Cambridge, Massachusetts.
  7. Olivier Delande, Dale Miller & Alexis Saurin (2010): Proof and refutation in MALL as a game. Annals of Pure and Applied Logic 161(5), pp. 654–672, doi:10.1016/j.apal.2009.07.017.
  8. Andrew Gacek, Dale Miller & Gopalan Nadathur (2011): Nominal abstraction. Information and Computation 209(1), pp. 48–73, doi:10.1016/j.ic.2010.09.004.
  9. Jean-Yves Girard (1987): Linear Logic. Theoretical Computer Science 50, pp. 1–102, doi:10.1016/0304-3975(87)90045-4.
  10. Jean-Yves Girard (1992): A Fixpoint Theorem in Linear Logic. An email posting to the mailing list
  11. Matthew Hennessy & Robin Milner (1985): Algebraic Laws for Nondeterminism and Concurrency. JACM 32(1), pp. 137–161, doi:10.1145/2455.2460.
  12. 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.
  13. Dale Miller (2011): A proposal for broad spectrum proof certificates. In: J.-P. Jouannaud & Z. Shao: CPP: First International Conference on Certified Programs and Proofs, LNCS 7086, pp. 54–69, doi:10.1007/978-3-642-25379-9_6.
  14. Dale Miller & Gopalan Nadathur (2012): Programming with Higher-Order Logic. Cambridge University Press, doi:10.1017/CBO9781139021326.
  15. Dale Miller, Gopalan Nadathur, Frank Pfenning & Andre Scedrov (1991): Uniform Proofs as a Foundation for Logic Programming. Annals of Pure and Applied Logic 51, pp. 125–157, doi:10.1016/0168-0072(91)90068-W.
  16. 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.
  17. Robin Milner (1989): Communication and Concurrency. Prentice-Hall International.
  18. Damien Pous & Davide Sangiorgi (2011): Enhancements of the bisimulation proof method. In: Davide Sangiorgi & Jan Rutten: Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, pp. 233–289, doi:10.1017/CBO9780511792588.007.
  19. 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.
  20. Alwen Tiu, Gopalan Nadathur & Dale Miller (2005): Mixing Finite Success and Finite Failure in an Automated Prover. In: Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05), pp. 79–98.
  21. (2015): The Bedwyr model checker. Available at

Comments and questions to:
For website issues: