Bruno Barras

According to our database, Bruno Barras authored at least 15 papers between 1996 and 2020.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2020

Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory.

Bruno Barras, Valentin Maestracci

Proceedings of the Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2020

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

Environments and the complexity of abstract machines.

Beniamino Accattoli, Bruno Barras

Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09, 2017

The Negligible and Yet Subtle Cost of Pattern Matching.

Beniamino Accattoli, Bruno Barras

Proceedings of the Programming Languages and Systems - 15th Asian Symposium, 2017

2015

A generalization of the Takeuti-Gandy interpretation.

Bruno Barras, Thierry Coquand, Simon Huber

Math. Struct. Comput. Sci., 2015

Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface.

Bruno Barras, Carst Tankink, Enrico Tassi

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

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

Proceedings of the Intelligent Computer Mathematics, 2013

Semantics of Intensional Type Theory extended with Decidable Equational Theories.

Qian Wang, Bruno Barras

Proceedings of the Computer Science Logic 2013 (CSL 2013), 2013

2011

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

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

2010

Sets in Coq, Coq in Sets.

Bruno Barras

J. Formaliz. Reason., 2010

2008

A New Elimination Rule for the Calculus of Inductive Constructions.

Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini

Proceedings of the Types for Proofs and Programs, International Conference, 2008

The Implicit Calculus of Constructions as a Programming Language with Dependent Types.

Bruno Barras, Bruno Bernardo

Proceedings of the Foundations of Software Science and Computational Structures, 2008

2005

On the Role of Type Decorations in the Calculus of Inductive Constructions.

Bruno Barras, Benjamin Grégoire

Proceedings of the Computer Science Logic, 19th International Workshop, 2005

2000

Programming and Computing in HOL.

Bruno Barras

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1996

Verification of the Interface of a Small Proof System in Coq.

Bruno Barras

Proceedings of the Types for Proofs and Programs, 1996