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.