1. Abhishek Anand & Greg Morrisett (2017): Revisiting Parametricity: Inductives and Uniformity of Propositions. CoRR abs/1705.01163. Available at
  2. B. Aydemir, A. Bohannon, M. Fairbairn, N. Foster, B. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich & S. Zdancewic (2005): Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Proceedings of TPHOLs'05. Springer-Verlag, pp. 50–65, doi:10.1007/11541868_4.
  3. Hendrik Barendregt (1984): The λ-calculus Its Syntax and Semantics, revised edition, Studies in Logic and the Foundations of Mathematics 103. North Holland, doi:10.2307/2274112.
  4. Marcin Benke, Peter Dybjer & Patrik Jansson (2003): Universes for Generic Programs and Proofs in Dependent Type Theory. Nordic Journal of Computing 10(4), pp. 265–289. Available at
  5. James Cheney (2005): Scrap Your Nameplate: (Functional Pearl). In: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, ICFP '05. ACM, New York, NY, USA, pp. 180–191, doi:10.1145/1086365.1086389.
  6. Ernesto Copello, Nora Szasz & Álvaro Tasistro (2017 in press): Machine-checked proof of the Church-Rosser Theorem for the Lambda Calculus using the Barendregt Variable Convention in Constructive Type Theory. In: LSFA 2017. Available at
  7. Ernesto Copello, Álvaro Tasistro, Nora Szasz, Ana Bove & Maribel Fernández (2016): Alpha-Structural Induction and Recursion for the λ-calculus in Constructive Type Theory. ENTCS 323, pp. 109 – 124, doi:10.1016/j.entcs.2016.06.008.
  8. Benjamin Delaware, Bruno C. d. S. Oliveira & Tom Schrijvers (2013): Meta-theory à La Carte. SIGPLAN Not. 48(1), pp. 207–218, doi:10.1145/2429069.2429094.
  9. Murdoch J. Gabbay & Andrew M. Pitts (2001): A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing 13(35), pp. 341363, doi:10.1007/s001650200016.
  10. Gyesik Lee, Bruno Oliveira, Sungkeun Cho & Kwangkeun Yi (2012): GMeta: A Generic Formal Metatheory Framework for First-Order Representations. Springer, doi:
  11. Daniel R. Licata & Robert Harper (2009): A universe of binding and computation. In: International Conference on Functional Programming (ICFP), pp. 123–134, doi:10.1145/1596550.1596571.
  12. Per Martin-Löf (1984): Intuitionistic type theory. Studies in Proof Theory. Lecture Notes 1. Naples.
  13. Peter Morris, Thorsten Altenkirch & Conor McBride (2006): Exploring the Regular Tree Types. In: International Conference on Types for Proofs and Programs, TYPES'04. Springer-Verlag, Berlin, Heidelberg, doi:10.1007/11617990_16.
  14. Ulf Norell (2009): Dependently Typed Programming in Agda. In: Proceedings of the 6th International Conference on Advanced Functional Programming, AFP'08. Springer-Verlag, Berlin, doi:10.1145/1481861.1481862.
  15. Benjamin C. Pierce (2002): Types and Programming Languages, 1st edition. The MIT Press.
  16. Mark R. Shinwell (2006): Fresh O'Caml: Nominal Abstract Syntax for the Masses. ENTCS 148(2), doi:10.1016/j.entcs.2005.11.040.
  17. Mark R. Shinwell, Andrew M. Pitts & Murdoch James Gabbay (2003): FreshML: programming with binders made simple. SIGPLAN Notices 38(9), pp. 263–274, doi:10.1145/944746.944729.
  18. Christian Urban & Christine Tasson (2005): Nominal Techniques in Isabelle/HOL. In: Automated Deduction CADE-20, LNCS 3632. Springer Berlin Heidelberg, doi:10.1007/s10817-008-9097-2.
  19. Nobuko Yoshida & Vasco T. Vasconcelos (2007): Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication. ENTCS 171(4), pp. 73 – 93, doi:10.1016/j.entcs.2007.02.056.

Comments and questions to:
For website issues: