Gustavo Betarte

I took my PhD degree at Computing Science Department at Chalmers University of Technology and University of Göteborg.

Now I am a lecturer at Computing Science Department (InCo) at the Engineering School of the Universidad de la Republica, Montevideo, Uruguay and http://www.fing.edu.uy/~gustun is my new homepage.

• Extension of Martin-Löf's theory of types with record types and subtyping (with Alvaro Tasistro).
• Formal verification of Reactive Systems (with Cristina Cornes and Luis Sierra).

• PhD thesis: Dependent Record Types and Algebraic Structures in Type Theory
  Department of Computing Science, Chalmers University of Technology and University of Göteborg, Göteborg, Sweden, February 1998.

• Dependent Record Types, Subtyping and Proof Reutilization
  Presented at the workshop on "Subtyping, inheritance and modular development of proofs", held at Durham, England, 1997.

• Extension of Martin-Löf's type theory with record types and subtyping. (with Alvaro Tasistro)
  To appear in "25 Years of Constructive Type Theory", Oxford University Press, 1997.

• Formalisation of Systems of Algebras using Dependent Record Types and Subtyping: An Example. (with Alvaro Tasistro)
  In Proceedings of the 7th. Nordic workshop on Programming Theory, held at Göteborg, Sweden, 1995.

• A case study in machine-assisted proofs: The Integers form an Integral Domain.
  Licentiate thesis, 1993.

• Experiences with a mechanisation of Martin-Löf's theory of types. (with Eduardo Gimenez)
  Technical report 91-08, Inco, Pedeciba, 1991.