Proof Editors
-
Subrec: a proof checker for an extension of Martin-Löf's type theory extended with dependent record types and subtyping. G. Betarte
-
Experiences with a mechanisation of Martin-Löf's theory of
types. G. Betarte, E. Giménez. Technical Report 92-04, InCo - Pedeciba, Montevideo, Uruguay, 1992.
-
"Compilation du Filtrage avec Types Dépendants dans le Système Coq". C. Cornes .
Actes de la réunion du pôle Spécification et Preuves du GDR Programmation. Orleans, Novembre 1996.
-
"Automating Inversion of Inductive Predicates in Coq".
C. Cornes, D. Terrasse.
In BRA Workshop on Types for Proofs and Programs, LNCS 1158, Turin, June 1995.
Formal methods
Last modified: Fri Feb 5 14:12:25 GMT 1999