• 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)


  • 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.