1. Amal Ahmed (2004): Semantics of Types for Mutable State. Princeton University. Available at
  2. Amal Ahmed (2006): Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In: ESOP, 2006, doi:10.1007/11693024_6.
  3. 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.
  4. 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.
  5. 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.
  6. 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 Talk and discussion session at PLPV 2011.
  7. 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
  8. Adam Chlipala (2011): Certified Programming with Dependent Types. Available at
  9. Robert L. Constable & Scott Fraser Smith (1987): Partial Objects in Constructive Type Theory. In: LICS, 1987, pp. 183–193.
  10. 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
  11. Karl Crary (1998): Type Theoretic Methodology for Practical Programming Languages. Cornell University.
  12. Nils Anders Danielsson (2010): Total parser combinators. In: ICFP, 2010. ACM, New York, NY, USA, pp. 285–296, doi:10.1145/1863543.1863585.
  13. 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.
  14. 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
  15. Jean-Yves Girard (1972): Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. Université Paris VII.
  16. Aquinas Hobor, Robert Dockins & Andrew W. Appel (2010): A Theory of Indirection via Approximation. In: POPL, 2010, pp. 171–185. Available at
  17. 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.
  18. 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.
  19. 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.
  20. Neelakantan Krishnaswami & Nick Benton (2011): Ultrametric Semantics of Reactive Programs. In: LICS, 2011, pp. 257–266, doi:10.1109/LICS.2011.38.
  21. Tom Murphy, VII (2008): Modal Types for Mobile Code. Carnegie Mellon. Available at Available as technical report CMU-CS-08-126.
  22. 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.
  23. Hiroshi Nakano (2000): A Modality for Recursion. In: LICS, 2000. IEEE Computer Society, Washington, DC, USA, pp. 255–, doi:10.1109/LICS.2000.855774.
  24. Ulf Norell (2007): Towards a practical programming language based on dependent type theory. Department of Computer Science and Engineering, Chalmers University of Technology.
  25. Benjamin C. Pierce (2002): Types and Programming Languages. MIT Press.
  26. 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.
  27. The Coq Development Team (2011): The Coq Proof Assistant, Frequently Asked Questions. INRIA. Available at
  28. The Coq Development Team (2011): The Coq Proof Assistant Reference Manual, Version 8.3. INRIA. Available at
  29. Stephanie Weirich (2011): Combining Proofs and Programs. Invited lecture for RTA 2011 and TLCA 2011, Novi Sad, Serbia.
  30. Stephanie Weirich (2011): Combining Proofs and Programs. Presentation at DTP 2011, Shonan Meeting Seminar 007, Japan.
  31. Stephanie Weirich (2011): Combining Proofs and Programs in Trellys. Plenary Address at MFPS 26, Pittburgh, PA.
  32. 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.

Comments and questions to:
For website issues: