Bruno Barras

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