Abhishek Anand & Greg Morrisett (2017):
Revisiting Parametricity: Inductives and Uniformity of Propositions.
CoRR abs/1705.01163.
Available at http://arxiv.org/abs/1705.01163.
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.
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.
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 http://dl.acm.org/citation.cfm?id=985799.985801.
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.
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 http://lsfa2017.cic.unb.br/LSFA2017.pdf.
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.
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.
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.
Gyesik Lee, Bruno Oliveira, Sungkeun Cho & Kwangkeun Yi (2012):
GMeta: A Generic Formal Metatheory Framework for First-Order Representations.
Springer,
doi:10.1.1.298.2957.
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.
Per Martin-Löf (1984):
Intuitionistic type theory.
Studies in Proof Theory. Lecture Notes 1.
Naples.
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.
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.
Benjamin C. Pierce (2002):
Types and Programming Languages,
1st edition.
The MIT Press.
Mark R. Shinwell (2006):
Fresh O'Caml: Nominal Abstract Syntax for the Masses.
ENTCS 148(2),
doi:10.1016/j.entcs.2005.11.040.
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.
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.
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.