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