Bruno Barras

Publication Activity (10 Years)

Years Active: 1996-2020
Publications (10 Years): 4

Top Topics

Pattern Matching

Legal Documents

Interactive Theorem Proving

Top Venues

MKM/Calculemus/DML

Math. Struct. Comput. Sci.

Publications

Bruno Barras, Valentin Maestracci
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory. LFMTP (2020)
Sabine Azzi, Bruno Barras, Maria Christofi, David Vigilant
Using linear codes as a fault countermeasure for nonlinear operations: application to AES and formal verification. J. Cryptogr. Eng. 7 (1) (2017)
Beniamino Accattoli, Bruno Barras
The Negligible and Yet Subtle Cost of Pattern Matching. APLAS (2017)
Beniamino Accattoli, Bruno Barras
Environments and the complexity of abstract machines. PPDP (2017)
Bruno Barras, Carst Tankink, Enrico Tassi
Asynchronous processing of Coq documents: from the kernel up to the user interface. CoRR (2015)
Bruno Barras, Thierry Coquand, Simon Huber
A generalization of the Takeuti-Gandy interpretation. Math. Struct. Comput. Sci. 25 (5) (2015)
Bruno Barras, Carst Tankink, Enrico Tassi
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. ITP (2015)
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. MKM/Calculemus/DML (2013)
Qian Wang, Bruno Barras
Semantics of Intensional Type Theory extended with Decidable Equational Theories. CSL (2013)
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. CoRR (2013)
Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. LICS (2011)
Bruno Barras
Sets in Coq, Coq in Sets. J. Formaliz. Reason. 3 (1) (2010)
Bruno Barras, Bruno Bernardo
The Implicit Calculus of Constructions as a Programming Language with Dependent Types. FoSSaCS (2008)
Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini
A New Elimination Rule for the Calculus of Inductive Constructions. TYPES (2008)
Bruno Barras, Benjamin Grégoire
On the Role of Type Decorations in the Calculus of Inductive Constructions. CSL (2005)
Bruno Barras
Programming and Computing in HOL. TPHOLs (2000)
Bruno Barras
Verification of the Interface of a Small Proof System in Coq. TYPES (1996)