Verification of the Interface of a Small Proof System in Coq. - Bruno Barras (TYPES, 1996)

Programming and Computing in HOL. - Bruno Barras (TPHOLs, 2000)

On the Role of Type Decorations in the Calculus of Inductive Constructions. - Bruno Barras; Benjamin Grégoire (CSL, 2005)

The Implicit Calculus of Constructions as a Programming Language with Dependent Types. - Bruno Barras; Bruno Bernardo (FoSSaCS, 2008)

A New Elimination Rule for the Calculus of Inductive Constructions. - Bruno Barras; Pierre Corbineau; Benjamin Grégoire; Hugo Herbelin; Jorge Luis Sacchini (TYPES, 2008)

Sets in Coq, Coq in Sets. - Bruno Barras (J. Formaliz. Reason., 2010)

CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. - Bruno Barras; Jean-Pierre Jouannaud; Pierre-Yves Strub; Qian Wang (LICS, 2011)

Semantics of Intensional Type Theory extended with Decidable Equational Theories. - Qian Wang; Bruno Barras (CSL, 2013)

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. - Bruno Barras; Lourdes Del Carmen González-Huesca; Hugo Herbelin; Yann Régis-Gianas; Enrico Tassi; Makarius Wenzel; Burkhart Wolff (MKM/Calculemus/DML, 2013)

Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. - Bruno Barras; Carst Tankink; Enrico Tassi (ITP, 2015)

A generalization of the Takeuti-Gandy interpretation. - Bruno Barras; Thierry Coquand; Simon Huber (Math. Struct. Comput. Sci., 2015)

The Negligible and Yet Subtle Cost of Pattern Matching. - Beniamino Accattoli; Bruno Barras (APLAS, 2017)

Environments and the complexity of abstract machines. - Beniamino Accattoli; Bruno Barras (PPDP, 2017)

Using linear codes as a fault countermeasure for nonlinear operations: application to AES and formal verification. - Sabine Azzi; Bruno Barras; Maria Christofi; David Vigilant (J. Cryptogr. Eng., 2017)

Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory. - Bruno Barras; Valentin Maestracci (LFMTP, 2020)