Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda. - Ernesto Copello; Alvaro Tasistro; Bruno Bianchi (SBLP, 2014)

Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus. - Alvaro Tasistro; Ernesto Copello; Nora Szasz (LSFA, 2014)

Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory. - Ernesto Copello; Alvaro Tasistro; Nora Szasz; Ana Bove; Maribel Fernández (LSFA, 2015)

Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory. - Ernesto Copello; Nora Szasz; Álvaro Tasistro (LSFA, 2017)

Formal metatheory of the Lambda calculus using Stoughton's substitution. - Ernesto Copello; Nora Szasz; Alvaro Tasistro (Theor. Comput. Sci., 2017)

Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders. - Ernesto Copello; Nora Szasz; Álvaro Tasistro (LFMTP@FSCD, 2018)

Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention. - Ernesto Copello; Nora Szasz; Álvaro Tasistro (Math. Struct. Comput. Sci., 2021)