Extension of Martin-Löf's Type Theory with Record Types and Subtyping (1998)
Gustavo Betarte, Alvaro Tasistro
this paper, the implementation has been used to verify an abstract version of sorting by insertion in (Tasistro 1997). In this latter work, dependent record types are used to express speciøcations...
Thesis (doctoral)--Göteborg University, 1997.
Type Theory and Functional Programming: a work proposal (1997)
Gustavo Betarte, Ana Bove, Juan José Cabezas, Guillermo Calderón, Cristina Cornes, Sylvia Da Rosa, ...
We propose a series of work areas related to program verification, type theory and functional programming. The areas presented are: the implementation of an environment for carrying out constructions...
at is, to investigate the production of verified implementations of programming languages. Writing programs in constructive type theory amounts to writing completely formal proofs of often complex...
Formulation of Martin-Löf's theory of types with explicit substitutions (1993)
In various lectures given during 1992, Martin-Lof has presented the main ideas of a formulation of the theory of types in which substitution is not left unspecied and instead appears explicit in the...