Bruno Barras

I'm a Researcher at Inria Saclay.

I belong to Laboratoire Spécification et Vérification (LSV)

Professional interests:

Type theory, Metatheory, Program extraction, Bootstrap,

Homotopy Type Theory

Functional programming, Reduction functions, Efficient implementations of Abstract Machines and Conversion Algorithms.

Implementations

Sets in Coq, Coq in Sets
Coq*: an implementation of the Implicit Calculus of Constructions
Proofs in Coq
Implementation of Reduction Functions
Caml-Light to Objective-Caml translator

Contact Information

Email: bruno barras at inria.fr