×
Author ID: barras.bruno Recent zbMATH articles by "Barras, Bruno"
Published as: Barras, Bruno
Homepage: http://www.lix.polytechnique.fr/Labo/Bruno.Barras/
External Links: MGP · ResearchGate · dblp · IdRef · theses.fr

Publications by Year

Citations contained in zbMATH Open

12 Publications have been cited 55 times in 49 Documents Cited by Year
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
223
2013
Sets in Coq, Coq in Sets. Zbl 1211.03023
Barras, Bruno
21
2010
Verification of the interface of a small proof system in Coq. Zbl 0927.03018
Barras, Bruno
8
1998
Programming and computing in HOL. Zbl 0974.68187
Barras, Bruno
7
2000
The implicit calculus of constructions as a programming language with dependent types. Zbl 1138.68356
Barras, Bruno; Bernardo, Bruno
5
2008
A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005
Barras, Bruno; Coquand, Thierry; Huber, Simon
4
2015
The negligible and yet subtle cost of pattern matching. Zbl 1503.68034
Accattoli, Beniamino; Barras, Bruno
3
2017
Asynchronous processing of Coq documents: from the kernel up to the user interface. Zbl 1465.68275
Barras, Bruno; Tankink, Carst; Tassi, Enrico
2
2015
Semantics of intensional type theory extended with decidable equational theories. Zbl 1356.68205
Wang, Qian; Barras, Bruno
2
2013
Pervasive parallelism in highly-trustable interactive theorem proving systems. Zbl 1390.68571
Barras, Bruno; del Carmen González Huesca, Lourdes; Herbelin, Hugo; Régis-Gianas, Yann; Tassi, Enrico; Wenzel, Makarius; Wolff, Burkhart
1
2013
On the role of type decorations in the calculus of inductive constructions. Zbl 1136.03305
Barras, Bruno; Grégoire, Benjamin
1
2005
A new elimination rule for the calculus of inductive constructions. Zbl 1246.68085
Barras, Bruno; Corbineau, Pierre; Grégoire, Benjamin; Herbelin, Hugo; Sacchini, Jorge Luis
1
2009
The negligible and yet subtle cost of pattern matching. Zbl 1503.68034
Accattoli, Beniamino; Barras, Bruno
3
2017
A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005
Barras, Bruno; Coquand, Thierry; Huber, Simon
4
2015
Asynchronous processing of Coq documents: from the kernel up to the user interface. Zbl 1465.68275
Barras, Bruno; Tankink, Carst; Tassi, Enrico
2
2015
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
223
2013
Semantics of intensional type theory extended with decidable equational theories. Zbl 1356.68205
Wang, Qian; Barras, Bruno
2
2013
Pervasive parallelism in highly-trustable interactive theorem proving systems. Zbl 1390.68571
Barras, Bruno; del Carmen González Huesca, Lourdes; Herbelin, Hugo; Régis-Gianas, Yann; Tassi, Enrico; Wenzel, Makarius; Wolff, Burkhart
1
2013
Sets in Coq, Coq in Sets. Zbl 1211.03023
Barras, Bruno
21
2010
A new elimination rule for the calculus of inductive constructions. Zbl 1246.68085
Barras, Bruno; Corbineau, Pierre; Grégoire, Benjamin; Herbelin, Hugo; Sacchini, Jorge Luis
1
2009
The implicit calculus of constructions as a programming language with dependent types. Zbl 1138.68356
Barras, Bruno; Bernardo, Bruno
5
2008
On the role of type decorations in the calculus of inductive constructions. Zbl 1136.03305
Barras, Bruno; Grégoire, Benjamin
1
2005
Programming and computing in HOL. Zbl 0974.68187
Barras, Bruno
7
2000
Verification of the interface of a small proof system in Coq. Zbl 0927.03018
Barras, Bruno
8
1998
all top 5

Cited by 85 Authors

3 Kirst, Dominik
3 Kunčar, Ondřej
3 Nipkow, Tobias
3 Popescu, Andrei
2 Bohrer, Brandon
2 Dehlinger, Christophe
2 Dufourd, Jean-François
2 Kumar, Ramana
2 Norrish, Michael
2 Platzer, André
2 Smolka, Gert
2 Weirich, Stephanie
2 Wiedijk, Freek
1 Accattoli, Beniamino
1 Aehlig, Klaus
1 Alves, Sandra
1 Angiuli, Carlo
1 Annenkov, Danil
1 Arthan, Rob D.
1 Barendregt, Hendrik Pieter
1 Barras, Bruno
1 Bengtson, Jesper
1 Berghofer, Stefan
1 Bezem, Marc
1 Bos, Nathaniel
1 Cao, Qinxiang
1 Chapman, James T. E.
1 Choudhury, Pritam
1 Cockx, Jesper
1 Cohen, Liron
1 Constable, Robert Lee
1 Coquand, Thierry
1 Crégut, Pierre
1 Devriese, Dominique
1 Eades, Harley III
1 Fernández V., Manuel
1 Forster, Yannick
1 Fridlender, Daniel
1 Fu, Peng
1 Fulton, Nathan
1 Gambino, Nicola
1 Garrigue, Jacques
1 Ghica, Dan R.
1 Haftmann, Florian
1 Harper, Robert
1 Henry, Simon
1 Hermes, Marc
1 Hurd, Joe
1 Kaliszyk, Cezary
1 Kesner, Delia
1 Kishida, Kohei
1 Kravchuk-Kirilyuk, Anastasiya
1 Licata, Daniel R.
1 Malecha, Gregory
1 Milo, Mikkel
1 Mitsch, Stefan
1 Monnier, Stefan
1 Morehouse, Edward
1 Muroya, Koko
1 Myreen, Magnus O.
1 Nielsen, Jakob Botsch
1 Obua, Steven
1 Owens, Scott
1 Pagano, Miguel
1 Pąk, Karol
1 Palmgren, Erik
1 Piessens, Frank
1 Roe, Kenneth
1 Roßkopf, Simon
1 Sato, Masahiro
1 Schack-Nielsen, Anders
1 Schürmann, Carsten
1 Selinger, Peter
1 Sestini, Filippo
1 Slind, Konrad
1 Song, Xiaoyu
1 Spitters, Bas
1 Stump, Aaron
1 Sun, Jiaguang
1 Tao, Yichen
1 Lima Ventura, Daniel
1 Voizard, Antoine
1 Vouillon, Jérôme
1 Wang, Qian
1 Weber, Tjark

Citations by Year