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, 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.
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.
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.
Edmund M. Clarke, Orna Grumberg & Doron A. Peled (1999):
Model Checking.
The MIT Press,
Cambridge, Massachusetts.
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.
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.
Jean-Yves Girard (1987):
Linear Logic.
Theoretical Computer Science 50,
pp. 1–102,
doi:10.1016/0304-3975(87)90045-4.
Jean-Yves Girard (1992):
A Fixpoint Theorem in Linear Logic.
An email posting to the mailing list linear@cs.stanford.edu.
Matthew Hennessy & Robin Milner (1985):
Algebraic Laws for Nondeterminism and Concurrency.
JACM 32(1),
pp. 137–161,
doi:10.1145/2455.2460.
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 (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.
Dale Miller & Gopalan Nadathur (2012):
Programming with Higher-Order Logic.
Cambridge University Press,
doi:10.1017/CBO9781139021326.
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.
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.
Robin Milner (1989):
Communication and Concurrency.
Prentice-Hall International.
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.
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.
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.
(2015):
The Bedwyr model checker.
Available at http://slimmer.gforge.inria.fr/bedwyr/.