Ernesto Copello

Available identifiers

zbMath Open copello.ernestoMaRDI QIDQ530863

List of research outcomes

Publication	Date of Publication	Type
Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention	2022-01-20	Paper
Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory	2019-11-12	Paper
Alpha-structural induction and recursion for the lambda calculus in constructive type theory	2018-04-23	Paper
Formal metatheory of the lambda calculus using Stoughton's substitution	2017-06-15	Paper
Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus	2016-08-01	Paper

Research outcomes over time

This page was built for person: Ernesto Copello