Alvaro Tasistro

Orcid: 0009-0003-2187-3177

According to our database1, Alvaro Tasistro authored at least 17 papers between 1996 and 2021.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2021
Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention.
Math. Struct. Comput. Sci., 2021

2020
Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda.
Proceedings of the 15th International Workshop on Logical and Semantic Frameworks with Applications, 2020

2019
Teaching of formal methods: evidence of its inclusion in curricula, results, and difficulties.
Proceedings of the XXII Iberoamerican Conference on Software Engineering, 2019

2018
Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution.
Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2018

Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders.
Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2018

2017
Formal metatheory of the Lambda calculus using Stoughton's substitution.
Theor. Comput. Sci., 2017

Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory.
Proceedings of the 12th Workshop on Logical and Semantic Frameworks, with Applications, 2017

2015
Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory.
Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Presentation of Classical Propositional Tableaux on Program Design Premises.
CoRR, 2015

Dependent Types for Nominal Terms with Atom Substitutions.
Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014
Formalisation in Constructive Type Theory of Stoughton's Substitution for the Lambda Calculus.
Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda.
Proceedings of the Programming Languages - 18th Brazilian Symposium, 2014

Novel Didactic Proof Assistant for First-Order Logic Natural Deduction.
Proceedings of the Learning and Collaboration Technologies. Designing and Developing Novel Learning Experiences, 2014

2013
Proof Assistant Based on Didactic Considerations.
J. Univers. Comput. Sci., 2013

2010
A Type-Theoretic Framework for Certified Model Transformations.
Proceedings of the Formal Methods: Foundations and Applications, 2010

1999
Specification of a Smart Card Operating System.
Proceedings of the Types for Proofs and Programs, 1999

1996
Abstract Insertion Sort in an Extension of Type Theory with Record Types and Subtyping.
Proceedings of the Types for Proofs and Programs, 1996


  Loading...