Deprecated : The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Gustavo Betarte
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.
Research interests: constructive type theory,
implementation and use of proof assistants, programming logic.
Current work:
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).
Some papers you might be interested in:
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.
(
To Chalmers CS Dept. Welcome page .)