Álvaro Tasistro

Available identifiers

zbMath Open tasistro.alvaroMaRDI QIDQ530862

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
Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda	2021-02-22	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
Dependent Types for Nominal Terms with Atom Substitutions	2017-07-12	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
A Type-Theoretic Framework for Certified Model Transformations	2011-05-12	Paper
https://portal.mardi4nfdi.de/entity/Q2766801	2002-07-22	Paper
https://portal.mardi4nfdi.de/entity/Q4247299	1999-06-16	Paper
https://portal.mardi4nfdi.de/entity/Q4246954	1999-06-16	Paper

Research outcomes over time

This page was built for person: Álvaro Tasistro