@phdthesis(ahmed:phd,
 author       = "Amal Ahmed",
 year         = "2004",
 title        = "Semantics of Types for Mutable State",
 school       = "Princeton University",
 url          = "http://www.cs.princeton.edu/research/techreps/TR-713-04",
)
@inproceedings(ahmed:steps,
 author       = "Amal Ahmed",
 year         = "2006",
 title        = "Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types",
 booktitle    = "ESOP, 2006",
 doi          = "10.1007/11693024\_6",
)
@article(appel:steps,
 author       = "Andrew W. Appel and David McAllester",
 year         = "2001",
 title        = "An indexed model of recursive types for foundational proof-carrying code",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "23",
 number       = "5",
 pages        = "657--683",
 doi          = "10.1145/504709.504712",
)
@inproceedings(birkedal:synthetic,
 author       = "Lars Birkedal and Rasmus Ejlers Mogelberg and Jan Schwinghammer and Kristian Stovring",
 year         = "2011",
 title        = "First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees",
 booktitle    = "LICS 2011",
 pages        = "55--64",
 doi          = "10.1109/LICS.2011.16",
)
@article(capretta:general,
 author       = "Venanzio Capretta",
 year         = "2005",
 title        = "General Recursion via Coinductive Types",
 journal      = "Logical Methods in Computer Science",
 volume       = "1",
 number       = "2",
 pages        = "1--18",
 doi          = "10.2168/LMCS-1(2:1)2005",
)
@misc(ccasin:plpv11talk,
 author       = "Chris Casinghino and Harley D. Eades III and Garrin Kimmell and Vilhelm Sj\"{o}berg and Tim Sheard and Aaron Stump and Stephanie Weirich",
 title        = "The Preliminary Design of the {Trellys} Core Language",
 url          = "http://www.seas.upenn.edu/~ccasin/papers/plpv11_slides.pdf",
 note         = "Talk and discussion session at PLPV 2011",
)
@article(chlipala:cpdtjfp,
 author       = "Adam Chlipala",
 year         = "2010",
 title        = "An Introduction to Programming and Proving with Dependent Types in Coq",
 journal      = "Journal of Formalized Reasoning",
 volume       = "3(2)",
 pages        = "1--93",
 url          = "http://adam.chlipala.net/papers/CpdtJFR/",
)
@manual(chlipala:cpdt,
 author       = "Adam Chlipala",
 year         = "2011",
 title        = "Certified Programming with Dependent Types",
 url          = "http://adam.chlipala.net/cpdt/",
)
@inproceedings(constable:partial-objects,
 author       = "Robert L. Constable and Scott Fraser Smith",
 year         = "1987",
 title        = "Partial Objects in Constructive Type Theory",
 booktitle    = "LICS, 1987",
 pages        = "183--193",
)
@inproceedings(coquand:infinite,
 author       = "Thierry Coquand",
 year         = "1994",
 title        = "Infinite objects in type theory",
 booktitle    = "Proceedings of the international workshop on Types for proofs and programs",
 publisher    = "Springer-Verlag New York, Inc.",
 address      = "Secaucus, NJ, USA",
 pages        = "62--78",
 url          = "http://dl.acm.org/citation.cfm?id=189973.189976",
)
@phdthesis(crary:phd,
 author       = "Karl Crary",
 year         = "1998",
 title        = "Type Theoretic Methodology for Practical Programming Languages",
 school       = "Cornell University",
)
@inproceedings(nils:parsers,
 author       = "Nils Anders Danielsson",
 year         = "2010",
 title        = "Total parser combinators",
 booktitle    = "ICFP, 2010",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "285--296",
 doi          = "10.1145/1863543.1863585",
)
@incollection(nils:subtyping,
 author       = "Nils Anders Danielsson and Thorsten Altenkirch",
 year         = "2010",
 title        = "Subtyping, Declaratively",
 editor       = "Claude Bolduc and Jules Desharnais and Béchir Ktari",
 booktitle    = "Mathematics of Program Construction",
 series       = "Lecture Notes in Computer Science",
 volume       = "6120",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "100--118",
 doi          = "10.1007/978-3-642-13321-3\_8",
)
@inproceedings(dockins:terminationviaindirection,
 author       = "Robert Dockins and Aquinas Hobor",
 year         = "2010",
 title        = "A Theory of Termination via Indirection",
 editor       = "Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann",
 booktitle    = "Modelling, Controlling and Reasoning About State",
 series       = "Dagstuhl Seminar Proceedings",
 volume       = "10351",
 publisher    = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany",
 address      = "Dagstuhl, Germany",
 url          = "http://drops.dagstuhl.de/opus/volltexte/2010/2805",
)
@phdthesis(girard:phd,
 author       = "Jean-Yves Girard",
 year         = "1972",
 title        = "Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur",
 school       = "Universit\'{e} Paris VII",
)
@inproceedings(hobor09:knot,
 author       = "Aquinas Hobor and Robert Dockins and Andrew W. Appel",
 year         = "2010",
 title        = "A Theory of Indirection via Approximation",
 booktitle    = "POPL, 2010",
 pages        = "171--185",
 url          = "http://msl.cs.princeton.edu/indirection.pdf",
)
@inproceedings(Jia04modalproofs,
 author       = "Limin Jia and David Walker",
 year         = "2004",
 title        = "Modal proofs as distributed programs (Extended Abstract)",
 booktitle    = "ESOP, 2004",
 publisher    = "Springer",
 pages        = "219--233",
 doi          = "10.1007/978-3-540-24725-8\_16",
)
@inproceedings(kimmel:plpv12,
 author       = "Garrin Kimmell and Aaron Stump and Harley D. Eades III and Peng Fu and Tim Sheard and Stephanie Weirich and Chris Casinghino and Vilhelm Sj\"oberg and Nathan Collins and Ki Yung Ahn",
 year         = "2012",
 title        = "Equational Reasoning about Programs with General Recursion and Call-by-value Semantics",
 booktitle    = "PLPV, 2012",
 doi          = "10.1145/2103776.2103780",
)
@inproceedings(krishnaswami:semantic,
 author       = "Neelakantan Krishnaswami and Nick Benton",
 year         = "2011",
 title        = "A semantic model for graphical user interfaces",
 booktitle    = "ICFP, 2011",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "45--57",
 doi          = "10.1145/2034773.2034782",
)
@inproceedings(krishnaswami:ultrametric,
 author       = "Neelakantan Krishnaswami and Nick Benton",
 year         = "2011",
 title        = "Ultrametric Semantics of Reactive Programs",
 booktitle    = "LICS, 2011",
 pages        = "257--266",
 doi          = "10.1109/LICS.2011.38",
)
@phdthesis(murphy2008modal,
 author       = "Tom Murphy, VII",
 year         = "2008",
 title        = "Modal Types for Mobile Code",
 school       = "Carnegie Mellon",
 url          = "http://tom7.org/papers/",
 note         = "Available as technical report CMU-CS-08-126",
)
@inproceedings(murphy2007ml5,
 author       = "Tom Murphy, VII and Karl Crary and Robert Harper",
 year         = "2007",
 title        = "Type-safe Distributed Programming with {ML5}",
 booktitle    = "Trustworthy Global Computing 2007",
 doi          = "10.1007/978-3-540-78663-4\_9",
)
@inproceedings(Nakano:modality,
 author       = "Hiroshi Nakano",
 year         = "2000",
 title        = "A Modality for Recursion",
 booktitle    = "LICS, 2000",
 publisher    = "IEEE Computer Society",
 address      = "Washington, DC, USA",
 pages        = "255--",
 doi          = "10.1109/LICS.2000.855774",
)
@phdthesis(norell:thesis,
 author       = "Ulf Norell",
 year         = "2007",
 title        = "Towards a practical programming language based on dependent type theory",
 school       = "Department of Computer Science and Engineering, Chalmers University of Technology",
)
@book(pierce:tapl,
 author       = "Benjamin C. Pierce",
 year         = "2002",
 title        = "Types and Programming Languages",
 publisher    = "MIT Press",
)
@article(tait:reducibility,
 author       = "William W. Tait",
 year         = "1967",
 title        = "Intensional Interpretations of Functionals of Finite Type I",
 journal      = "The Journal of Symbolic Logic",
 volume       = "32",
 number       = "2",
 pages        = "pp. 198--212",
 doi          = "10.2307/2271658",
)
@manual(coqfaq,
 author       = "The {Coq} Development Team",
 year         = "2011",
 title        = "The {Coq} Proof Assistant, Frequently Asked Questions",
 organization = "INRIA",
 url          = "http://coq.inria.fr/faq/",
)
@manual(coq-83,
 author       = "{The {Coq} Development Team}",
 year         = "2011",
 title        = "The {Coq} Proof Assistant Reference Manual, Version 8.3",
 organization = "INRIA",
 url          = "http://coq.inria.fr/V8.3/refman/",
)
@misc(weirich:rta-talk,
 author       = "Stephanie Weirich",
 year         = "2011",
 title        = "Combining Proofs and Programs",
 note         = "Invited lecture for RTA 2011 and TLCA 2011, Novi Sad, Serbia",
)
@misc(weirich:dtp-talk,
 author       = "Stephanie Weirich",
 year         = "2011",
 title        = "Combining Proofs and Programs",
 note         = "Presentation at DTP 2011, Shonan Meeting Seminar 007, Japan",
)
@misc(weirich:mfps-talk,
 author       = "Stephanie Weirich",
 year         = "2011",
 title        = "Combining Proofs and Programs in Trellys",
 note         = "Plenary Address at MFPS 26, Pittburgh, PA",
)
@article(wright:syntactic,
 author       = "Andrew K. Wright and Matthias Felleisen",
 year         = "1992",
 title        = "A Syntactic Approach to Type Soundness",
 journal      = "Information and Computation",
 volume       = "115",
 pages        = "38--94",
 doi          = "10.1006/inco.1994.1093",
)