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