Edit Profile (opens in new tab) Barras, Bruno Co-Author Distance Author ID: barras.bruno Published as: Barras, Bruno Homepage: http://www.lix.polytechnique.fr/Labo/Bruno.Barras/ External Links: MGP · ResearchGate · dblp · IdRef · theses.fr Documents Indexed: 11 Publications since 1998 1 Further Contribution Co-Authors: 15 Co-Authors with 9 Joint Publications 544 Co-Co-Authors all top 5 Co-Authors 3 single-authored 3 Herbelin, Hugo 2 Coquand, Thierry 2 Grégoire, Benjamin 2 Tassi, Enrico 1 Accattoli, Beniamino 1 Aczel, Peter 1 Ahrens, Benedikt 1 Altenkirch, Thorsten 1 Angiuli, Carlo 1 Avigad, Jeremy 1 Awodey, Steve 1 Bauer, Andrej 1 Bernardo, Bruno 1 Bertot, Yves 1 Bezem, Marc 1 Bordg, Anthony 1 Brunerie, Guillaume 1 Cohen, Cyril 1 Constable, Robert Lee 1 Corbineau, Pierre 1 Curien, Pierre-Louis 1 del Carmen González Huesca, Lourdes 1 Dybjer, Peter 1 Finster, Eric 1 Gambino, Nicola 1 Garner, Richard 1 Gonthier, Georges 1 Grayson, Daniel Richard 1 Hales, Thomas Callister 1 Harper, Robert 1 Hofmann, Martin 1 Hofstra, Pieter J. W. 1 Hötzel Escardó, Martín 1 Hou (Favonia), Kuen-Bang 1 Huber, Simon 1 Joyal, André 1 Kapulkin, Krzysztof 1 Kock, Joachim 1 Kraus, Nicolai 1 Li, Nuo 1 Licata, Dan 1 Lumsdaine, Peter LeFanu 1 Luo, Zhaohui 1 Mahboubi, Assia 1 Martin-Löf, Per 1 Melikhov, Sergey Aleksandrovich 1 Nahas, Michael 1 Palmgren, Erik 1 Pelayo, Alvaro 1 Polonsky, Andrew 1 Régis-Gianas, Yann 1 Riehl, Emily 1 Rijke, Egbert 1 Sacchini, Jorge Luis 1 Scott, Dana Stewart 1 Scott, Philip J. 1 Shulman, Michael A. 1 Sojakova, Kristina 1 Solov’ëv, Sergeĭ Vladimirovich 1 Sozeau, Matthieu 1 Spitters, Bas 1 Tankink, Carst 1 1 Van den Berg, Benno 1 Voevodskiĭ, Vladimir Aleksandrovich 1 Wang, Qian 1 Warren, Michael Alton 1 Wenzel, Makarius 1 Wolff, Burkhart 1 Zeilberger, Noam Serials 1 MSCS. Mathematical Structures in Computer Science 1 Journal of Formalized Reasoning Fields 10 Computer science (68-XX) 7 Mathematical logic and foundations (03-XX) 2 Category theory; homological algebra (18-XX) 1 Algebraic topology (55-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 12 Publications have been cited 50 times in 44 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 Sets in Coq, Coq in Sets. Zbl 1211.03023Barras, Bruno 21 2010 Programming and computing in HOL. Zbl 0974.68187Barras, Bruno 7 2000 Verification of the interface of a small proof system in Coq. Zbl 0927.03018Barras, Bruno 7 1998 A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005Barras, Bruno; Coquand, Thierry; Huber, Simon 4 2015 Asynchronous processing of Coq documents: from the kernel up to the user interface. Zbl 1465.68275Barras, Bruno; Tankink, Carst; Tassi, Enrico 2 2015 The implicit calculus of constructions as a programming language with dependent types. Zbl 1138.68356Barras, Bruno; Bernardo, Bruno 2 2008 Semantics of intensional type theory extended with decidable equational theories. Zbl 1356.68205Wang, Qian; Barras, Bruno 2 2013 The negligible and yet subtle cost of pattern matching. Zbl 1503.68034Accattoli, Beniamino; Barras, Bruno 2 2017 On the role of type decorations in the calculus of inductive constructions. Zbl 1136.03305Barras, Bruno; Grégoire, Benjamin 1 2005 A new elimination rule for the calculus of inductive constructions. Zbl 1246.68085Barras, Bruno; Corbineau, Pierre; Grégoire, Benjamin; Herbelin, Hugo; Sacchini, Jorge Luis 1 2009 Pervasive parallelism in highly-trustable interactive theorem proving systems. Zbl 1390.68571Barras, Bruno; del Carmen González Huesca, Lourdes; Herbelin, Hugo; Régis-Gianas, Yann; Tassi, Enrico; Wenzel, Makarius; Wolff, Burkhart 1 2013 The negligible and yet subtle cost of pattern matching. Zbl 1503.68034Accattoli, Beniamino; Barras, Bruno 2 2017 A generalization of the Takeuti-Gandy interpretation. Zbl 1362.03005Barras, Bruno; Coquand, Thierry; Huber, Simon 4 2015 Asynchronous processing of Coq documents: from the kernel up to the user interface. Zbl 1465.68275Barras, Bruno; Tankink, Carst; Tassi, Enrico 2 2015 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 Semantics of intensional type theory extended with decidable equational theories. Zbl 1356.68205Wang, Qian; Barras, Bruno 2 2013 Pervasive parallelism in highly-trustable interactive theorem proving systems. Zbl 1390.68571Barras, 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.03023Barras, Bruno 21 2010 A new elimination rule for the calculus of inductive constructions. Zbl 1246.68085Barras, 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.68356Barras, Bruno; Bernardo, Bruno 2 2008 On the role of type decorations in the calculus of inductive constructions. Zbl 1136.03305Barras, Bruno; Grégoire, Benjamin 1 2005 Programming and computing in HOL. Zbl 0974.68187Barras, Bruno 7 2000 Verification of the interface of a small proof system in Coq. Zbl 0927.03018Barras, Bruno 7 1998 all cited Publications top 5 cited Publications all top 5 Cited by 72 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 Wiedijk, Freek 1 Accattoli, Beniamino 1 Aehlig, Klaus 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 Chapman, James T. E. 1 Cockx, Jesper 1 Cohen, Liron 1 Constable, Robert Lee 1 Coquand, Thierry 1 Crégut, Pierre 1 Devriese, Dominique 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 Kishida, Kohei 1 Licata, Daniel R. 1 Malecha, Gregory 1 Milo, Mikkel 1 Mitsch, 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 Vouillon, Jérôme 1 Wang, Qian 1 Weber, Tjark all top 5 Cited in 13 Serials 9 Journal of Automated Reasoning 4 Journal of Functional Programming 3 Theoretical Computer Science 2 MSCS. Mathematical Structures in Computer Science 2 Logical Methods in Computer Science 1 Journal of the London Mathematical Society. Second Series 1 Annals of Pure and Applied Logic 1 Annals of Mathematics and Artificial Intelligence 1 Philosophical Transactions of the Royal Society of London. Series A. Mathematical, Physical and Engineering Sciences 1 Higher-Order and Symbolic Computation 1 The Journal of Logic and Algebraic Programming 1 Journal of Applied Mathematics 1 Sādhanā all top 5 Cited in 10 Fields 40 Computer science (68-XX) 27 Mathematical logic and foundations (03-XX) 3 Category theory; homological algebra (18-XX) 3 Algebraic topology (55-XX) 1 Convex and discrete geometry (52-XX) 1 Quantum theory (81-XX) 1 Operations research, mathematical programming (90-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Systems theory; control (93-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year