Publications:
B. Barras, J.-P. Jouannaud, P.-Y. Strub, Q. Wang.
CoqMTU: a higher-order type theory with a predicative
hierachy of universes parameterized by a decidable first-order
theory.
LICS. (2011)
B. Barras. Sets in Coq, Coq in Sets.
Journal of Formalized Reasoning. (2010)
B. Barras, B. Bernardo. The Implicit Calculus of Constructions
as a Programming Language with Dependent Types.
In Proceedings of FoSSaCS. (2008)
Springerlink
B. Barras, P. Corbineau, B. Grégoire, H. Herbelin, J. L. Sacchini.
A New Elimination Rule for the Calculus of Inductive Constructions.
Proceedings TYPES. (2008)
Springerlink
B. Barras, B. Grégoire: On the Role of Type Decorations
in the Calculus of Inductive Constructions.
CSL. (2005)
Springerlink
B. Barras. Programming and Computing in HOL. TPHOLs. (2000)
Springerlink
B. Barras. Auto-validation d'un système de preuves avec familles
inductives. PhD thesis. (1999)
B. Barras. Verification of the Interface of a Small Proof
System in Coq. Proceedings TYPES. (1996)
Springerlink
B. Barras. Coq in Coq,
manuscript. (1996)
Talks
Formalizing a set-theoretical
model of CIC in Coq/IZF. Workgroup "Semantics" and "Type
Theory and Realizability" in Paris. (2011)
Or this update presented at
the Gallium seminar in Rocquencourt.
Back to my homepage.