6 citations · 9 across the 5 of their papers we have counts for
5 papers
Dependently Sorted Nominal Signatures
Maribel Fernández, Miguel Pagano, Nora Szasz +1
We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to…
Derivation and Verification of Array Sorting by Merging, and its Certification in Dafny
Juan Pablo Carbonell, José E. Solsona, Nora Szasz +1
We provide full certifications of two versions of merge sort of arrays in the verification-aware programming language Dafny. We start by considering schemas for applying the divide…
Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution
Martín Copes, Nora Szasz, Álvaro Tasistro
We present a full formalization in Martin-Löf's Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using first-order syntax with one sort of names for…
Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
Ernesto Copello, Nora Szasz, Álvaro Tasistro
We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then…
Presentation of Classical Propositional Tableaux on Program Design Premises
Juan Michelini, Alvaro Tasistro
We propose a presentation of classical propositional tableaux elaborated by application of methods that are noteworthy in program design, namely program derivation with separation…