B. Accattoli, Sources, https://sites.google.com/site

D. Baelde, On the Expressivity of Minimal Generic Quantification, Electronic Notes in Theoretical Computer Science, vol.228, pp.3-19, 2009.
DOI : 10.1016/j.entcs.2008.12.113
URL : https://hal.archives-ouvertes.fr/inria-00284186

H. P. Barendregt, The Lambda Calculus ? Its Syntax and Semantics, 1984.

G. Berry and J. J. Lévy, Minimal and optimal computations of recursive programs, pp.215-226, 1977.

J. Brotherston and R. Vestergaard, A formalised first-order confluence proof for the ?-calculus using one-sorted variable names, Inf. Comput, vol.183, issue.2, pp.212-244, 2003.

J. Dunfield and B. Pientka, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), IJCAR 2010, pp.15-21, 2010.

C. Elliott and F. Pfenning, Higher-order abstract syntax, pp.199-208, 1988.

A. Gacek, The Abella Interactive Theorem Prover (System Description), IJCAR 2008, pp.154-161, 2008.
DOI : 10.1007/978-3-540-71070-7_13

A. Gacek, A framework for specifying, prototyping, and reasoning about computational systems, 2009.

A. Gacek, Relating nominal and higher-order abstract syntax specifications, Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '10, pp.177-186, 2010.
DOI : 10.1145/1836089.1836112
URL : http://arxiv.org/abs/1003.5447

A. Gacek, D. Miller, and G. Nadathur, Combining Generic Judgments with Recursive Definitions, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.33-44, 2008.
DOI : 10.1109/LICS.2008.33
URL : http://arxiv.org/abs/0802.0865

A. Gacek, D. Miller, and G. Nadathur, Reasoning in Abella about Structural Operational Semantics Specifications, Electronic Notes in Theoretical Computer Science, vol.228, pp.85-100, 2009.
DOI : 10.1016/j.entcs.2008.12.118

A. Gacek, D. Miller, and G. Nadathur, Nominal abstraction, Information and Computation, vol.209, issue.1, pp.48-73, 2011.
DOI : 10.1016/j.ic.2010.09.004
URL : http://doi.org/10.1016/j.ic.2010.09.004

A. Gacek, D. Miller, and G. Nadathur, A Two-Level Logic Approach to Reasoning About Computations, Journal of Automated Reasoning, vol.40, issue.4, pp.241-273, 2012.
DOI : 10.1007/s10817-011-9218-1
URL : https://hal.archives-ouvertes.fr/hal-00776208

J. R. Glauert and Z. Khasidashvili, Relating conflict-free stable transition and event models via redex families, Theor. Comput. Sci, vol.286, issue.1, pp.65-95, 2002.

P. V. Homeier, A proof of the Church-Rosser theorem for the ?-calculus in higher order logic, TPHOLs 2001: Supplemental Proceedings, pp.207-222, 2001.

G. P. Huet, Abstract, Journal of Functional Programming, vol.34, issue.03, pp.371-394, 1994.
DOI : 10.1017/S0956796800001106

G. P. Huet and J. J. Lévy, Computations in orthogonal rewriting systems, I. In: Computational Logic -Essays in Honor of Alan Robinson, pp.395-414, 1991.

G. P. Huet and J. J. Lévy, Computations in orthogonal rewriting systems, II. In: Computational Logic -Essays in Honor of Alan Robinson, pp.415-443, 1991.

J. J. Lévy, Réductions correctes et optimales dans le lambda-calcul, Thése d'Etat, 1978.

J. Mckinna and R. Pollack, Pure type systems formalized, TLCA 1993, pp.289-305, 1993.
DOI : 10.1007/BFb0037113

P. Mellì-es, Axiomatic Rewriting Theory VI Residual Theory Revisited, RTA 2002, pp.24-50, 2002.

D. Miller and G. Nadathur, A logic programming approach to manipulating formulas and programs, pp.379-388, 1987.

D. Miller and A. Tiu, A proof theory for generic judgments, ACM Transactions on Computational Logic, vol.6, issue.4, pp.749-783, 2005.
DOI : 10.1145/1094622.1094628

D. Miller and A. Tiu, Proof search specifications of bisimulation and modal logics for the ?-calculus, ACM Trans. Comput. Log, vol.11, issue.2, 2010.

T. Nipkow, More Church-Rosser proofs, Journal of Automated Reasoning, pp.733-747, 1996.

F. Pfenning, A proof of the Church-Rosser theorem and its representation in a logical framework, 1992.

F. Pfenning and C. Schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, CADE 1999, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

B. Pientka, Beluga: Programming with Dependent Types, Contextual Data, and Contexts, FLOPS 2010, pp.1-12, 2010.
DOI : 10.1007/978-3-642-12251-4_1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.163.4071

R. Pollack, Polishing up the Tait-Martin-Löf proof of the Church-Rosser theorem, 1995.

O. Rasmussen, The Church-Rosser theorem in Isabelle: a proof porting experiment, 1995.

N. Shankar, A mechanical proof of the Church-Rosser theorem, Journal of the ACM, vol.35, issue.3, pp.475-522, 1988.
DOI : 10.1145/44483.44484

M. Takahashi, Parallel Reductions in ??-Calculus, Information and Computation, vol.118, issue.1, pp.120-127, 1995.
DOI : 10.1006/inco.1995.1057

R. Vestergaard, The Primitive Proof Theory of the lambda-Calculus, 2003.