Iliano Cervesato & Frank Pfenning (2002):
A Linear Logical Framework.
Information & Computation 179(1),
pp. 19–75,
doi:10.1006/inco.2001.2951.
Iliano Cervesato & Frank Pfenning (2003):
A Linear Spine Calculus.
Journal of Logic and Computation 13(5),
pp. 639–688,
doi:10.1093/logcom/13.5.639.
Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann & Robert J. Simmons (2012):
Trace Matching in a Concurrent Logical Framework.
In: Adam Chlipala & Carsten Schürmann: 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice — LFMTP'12,
Copenhagen, Denmark,
doi:10.1145/2364406.2364408.
Iliano Cervesato, Frank Pfenning, David Walker & Kevin Watkins (2003):
A Concurrent Logical Framework II: Examples and Applications.
Technical Report CMU-CS-02-102.
Department of Computer Science, Carnegie Mellon University,
Pittsburgh, PA.
Matt Fairtlough & Michael Mendler (1997):
Propositional Lax Logic.
Information and Computation 137(1),
pp. 1–33,
doi:10.1006/inco.1997.2627.
Robert Harper, Furio Honsell & Gordon Plotkin (1993):
A framework for defining logics.
Journal of the ACM 40(1),
pp. 143–184,
doi:10.1145/138027.138060.
INRIA (2010):
The Coq Proof Assistant Reference Manual — Version 8.3.
Available at http://coq.inria.fr/refman/.
Dale Miller & Alwen Fernanto Tiu (2003):
A Proof Theory for Generic Judgments: An extended abstract.
In: LICS.
IEEE Computer Society,
pp. 118–127,
doi:10.1109/LICS.2003.1210051.
Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002):
Isabelle/HOL - A Proof Assistant for Higher-Order Logic.
LNCS 2283.
Springer,
doi:10.1007/3-540-45949-9.
Ulf Norell (2007):
Towards a practical programming language based on dependent type theory.
Chalmers University of Technology.
Frank Pfenning (2004):
Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk).
In: Wei-Ngan Chin: APLAS,
LNCS 3302.
PUB-SP,
pp. 196,
doi:10.1007/978-3-540-30477-7_13.
Frank Pfenning & Carsten Schürmann (1999):
System Description: Twelf - A Meta-Logical Framework for Deductive Systems.
In: Harald Ganzinger: CADE,
LNCS 1632.
Springer,
pp. 202–206,
doi:10.1007/3-540-48660-7_14.
Anders Schack-Nielsen (2011):
Implementing Substructural Logical Frameworks.
IT University of Copenhagen.
Robert J. Simmons (2012):
Substructural Logical Specifications.
Carnegie Mellon University.
Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2003):
A Concurrent Logical Framework I: Judgments and Properties.
Technical Report CMU-CS-02-101.
Department of Computer Science, Carnegie Mellon University,
Pittsburgh, PA.
Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2004):
A Concurrent Logical Framework: The Propositional Fragment.
In: Stefano Berardi, Mario Coppo & Ferruccio Damiani: TYPES,
LNCS 3085.
PUB-SV,
pp. 355–377,
doi:10.1007/978-3-540-24849-1_23.
Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2008):
Specifying Properties of Concurrent Computations in CLF.
ENTCS 199,
pp. 67–87,
doi:10.1016/j.entcs.2007.11.013.