Abstract Insertion Sort in an Extension of Type Theory with Record Types and Subtyping. - Alvaro Tasistro (TYPES, 1996)

Specification of a Smart Card Operating System. - Gustavo Betarte; Cristina Cornes; Nora Szasz; Alvaro Tasistro (TYPES, 1999)

A Type-Theoretic Framework for Certified Model Transformations. - Daniel Calegari; Carlos Luna 001; Nora Szasz; Alvaro Tasistro (SBMF, 2010)

Proof Assistant Based on Didactic Considerations. - Jorge Pais; Alvaro Tasistro (J. Univers. Comput. Sci., 2013)

Novel Didactic Proof Assistant for First-Order Logic Natural Deduction. - Jorge Pais; Alvaro Tasistro (HCI (14), 2014)

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)

Dependent Types for Nominal Terms with Atom Substitutions. - Elliot Fairweather; Maribel Fernández; Nora Szasz; Alvaro Tasistro (TLCA, 2015)

Presentation of Classical Propositional Tableaux on Program Design Premises. - Juan Michelini; Alvaro Tasistro (CoRR, 2015)

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 in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution. - Martín Copes; Nora Szasz; Álvaro Tasistro (LFMTP@FSCD, 2018)

Teaching of formal methods: evidence of its inclusion in curricula, results, and difficulties. - Silvana Moreno; Diego Vallespir; Álvaro Tasistro (CIbSE, 2019)

Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda. - Sebastián Urciuoli; Álvaro Tasistro; Nora Szasz (LSFA, 2020)

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)