Edit Profile (opens in new tab) Herbelin, Hugo Co-Author Distance Author ID: herbelin.hugo Published as: Herbelin, Hugo; Herbelin, H. Homepage: http://pauillac.inria.fr/~herbelin/ External Links: MGP · dblp · IdRef · theses.fr Documents Indexed: 29 Publications since 1989, including 1 Book 1 Contribution as Editor · 1 Further Contribution Co-Authors: 30 Co-Authors with 25 Joint Publications 559 Co-Co-Authors all top 5 Co-Authors 6 single-authored 7 Ariola, Zena M. 4 Curien, Pierre-Louis 3 Barras, Bruno 3 Sabry, Amr 2 Coquand, Thierry 2 Lee, Gyesik 2 Miquey, Étienne 2 Saurin, Alexis 2 Sozeau, Matthieu 1 Aczel, Peter 1 Ahrens, Benedikt 1 Altenkirch, Thorsten 1 Angiuli, Carlo 1 Avigad, Jeremy 1 Awodey, Steve 1 Bauer, Andrej 1 Bertot, Yves 1 Bezem, Marc 1 Bordg, Anthony 1 Brunerie, Guillaume 1 Cohen, Cyril 1 Constable, Robert Lee 1 Corbineau, Pierre 1 Cosnard, Michel Y. 1 del Carmen González Huesca, Lourdes 1 Downen, Paul 1 Dybjer, Peter 1 Ferreira, Afonso Galvao 1 Finster, Eric 1 Gambino, Nicola 1 Garner, Richard 1 Ghilezan, Silvia 1 Gonthier, Georges 1 Grayson, Daniel Richard 1 Grégoire, Benjamin 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 Huet, Gerard P. 1 Ilik, Danko 1 Joyal, André 1 Kapulkin, Krzysztof 1 Kock, Joachim 1 Kraus, Nicolai 1 Krivine, Jean-Louis 1 Letouzey, Pierre 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 Melliès, Paul-André 1 Nahas, Michael 1 Nakata, Keiko 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 Siles, Vincent 1 Sojakova, Kristina 1 Solov’ëv, Sergeĭ Vladimirovich 1 Spitters, Bas 1 Spiwack, Arnaud 1 Tassi, Enrico 1 1 Van den Berg, Benno 1 Voevodskiĭ, Vladimir Aleksandrovich 1 Warren, Michael Alton 1 Wenzel, Makarius 1 Wolff, Burkhart 1 Zeilberger, Noam 1 Zimmermann, Stéphane all top 5 Serials 3 Journal of Functional Programming 2 Higher-Order and Symbolic Computation 1 Annals of Pure and Applied Logic 1 Parallel Computing 1 Journal of Logic and Computation 1 MSCS. Mathematical Structures in Computer Science 1 Panoramas et Synthèses 1 LIPIcs – Leibniz International Proceedings in Informatics all top 5 Fields 25 Mathematical logic and foundations (03-XX) 21 Computer science (68-XX) 2 Category theory; homological algebra (18-XX) 1 General and overarching topics; collections (00-XX) 1 Algebraic topology (55-XX) 1 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 27 Publications have been cited 212 times in 157 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 The duality of computation. Zbl 1321.68146Curien, Pierre-Louis; Herbelin, Hugo 73 2000 A \(\lambda\)-caclulus structure isomorphic to Gentzen-style sequent calculus structure. Zbl 1044.03509Herbelin, Hugo 33 1995 Minimal classical logic and control operators. Zbl 1039.03019Ariola, Zena M.; Herbelin, Hugo 14 2003 A proof-theoretic foundation of abortive continuations. Zbl 1128.68089Ariola, Zena M.; Herbelin, Hugo; Sabry, Amr 10 2007 \(A\)-translation and looping combinators in pure type systems. Zbl 0817.03007Coquand, Thierry; Herbelin, Hugo 8 1994 An operational account of call-by-value minimal and classical \(\lambda \)-calculus in “natural deduction” form. Zbl 1246.03030Herbelin, Hugo; Zimmermann, Stéphane 7 2009 Kripke models for classical logic. Zbl 1225.03009Ilik, Danko; Lee, Gyesik; Herbelin, Hugo 6 2010 Classical call-by-need and duality. Zbl 1331.68041Ariola, Zena M.; Herbelin, Hugo; Saurin, Alexis 6 2011 A type-theoretic foundation of continuations and prompts. Zbl 1323.68090Ariola, Zena M.; Herbelin, Hugo; Sabry, Amr 6 2004 On the degeneracy of \(\Sigma\)-types in presence of computational classical logic. Zbl 1114.03029Herbelin, Hugo 6 2005 An approach to call-by-name delimited continuations. Zbl 1295.68063Herbelin, Hugo; Ghilezan, Silvia 5 2008 A constructive proof of dependent choice, compatible with classical logic. Zbl 1364.03070Herbelin, Hugo 5 2012 30 years of research and development around Coq. Zbl 1284.68517Huet, Gérard; Herbelin, Hugo 4 2014 Control reduction theories: The benefit of structural substitution. Zbl 1138.68020Ariola, Zena M.; Herbelin, Hugo 4 2008 A type-theoretic foundation of delimited continuations. Zbl 1213.68187Ariola, Zena M.; Herbelin, Hugo; Sabry, Amr 4 2009 Pure type system conversion is always typable. Zbl 1271.68080Siles, Vincent; Herbelin, Hugo 3 2012 Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus. Zbl 1246.03072Herbelin, Hugo; Lee, Gyesik 3 2009 The two list algorithm for the knapsack problem on an FPS T20. Zbl 0669.65051Cosnard, M.; Ferreira, A. G.; Herbelin, H. 3 1989 Explicit substitutions and reducibility. Zbl 0984.03014Herbelin, Hugo 3 2001 Abstract machines for dialogue games. Zbl 1206.03016Curien, Pierre-Louis; Herbelin, Hugo 2 2009 Realizability interpretation and normalization of typed call-by-need \(\lambda\)-calculus with control. Zbl 1504.68034Miquey, Étienne; Herbelin, Hugo 2 2018 A dependently-typed construction of semi-simplicial types. Zbl 1362.03006Herbelin, Hugo 1 2015 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 Classical call-by-need sequent calculi: the unity of semantic artifacts. Zbl 1354.68043Ariola, Zena M.; Downen, Paul; Herbelin, Hugo; Nakata, Keiko; Saurin, Alexis 1 2012 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 Interactive models of computation and program behavior. Zbl 1205.03045Curien, Pierre-Louis; Herbelin, Hugo; Krivine, Jean-Louis; Melliès, Paul-André 1 2009 Realizability interpretation and normalization of typed call-by-need \(\lambda\)-calculus with control. Zbl 1504.68034Miquey, Étienne; Herbelin, Hugo 2 2018 A dependently-typed construction of semi-simplicial types. Zbl 1362.03006Herbelin, Hugo 1 2015 30 years of research and development around Coq. Zbl 1284.68517Huet, Gérard; Herbelin, Hugo 4 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 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 A constructive proof of dependent choice, compatible with classical logic. Zbl 1364.03070Herbelin, Hugo 5 2012 Pure type system conversion is always typable. Zbl 1271.68080Siles, Vincent; Herbelin, Hugo 3 2012 Classical call-by-need sequent calculi: the unity of semantic artifacts. Zbl 1354.68043Ariola, Zena M.; Downen, Paul; Herbelin, Hugo; Nakata, Keiko; Saurin, Alexis 1 2012 Classical call-by-need and duality. Zbl 1331.68041Ariola, Zena M.; Herbelin, Hugo; Saurin, Alexis 6 2011 Kripke models for classical logic. Zbl 1225.03009Ilik, Danko; Lee, Gyesik; Herbelin, Hugo 6 2010 An operational account of call-by-value minimal and classical \(\lambda \)-calculus in “natural deduction” form. Zbl 1246.03030Herbelin, Hugo; Zimmermann, Stéphane 7 2009 A type-theoretic foundation of delimited continuations. Zbl 1213.68187Ariola, Zena M.; Herbelin, Hugo; Sabry, Amr 4 2009 Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus. Zbl 1246.03072Herbelin, Hugo; Lee, Gyesik 3 2009 Abstract machines for dialogue games. Zbl 1206.03016Curien, Pierre-Louis; Herbelin, Hugo 2 2009 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 Interactive models of computation and program behavior. Zbl 1205.03045Curien, Pierre-Louis; Herbelin, Hugo; Krivine, Jean-Louis; Melliès, Paul-André 1 2009 An approach to call-by-name delimited continuations. Zbl 1295.68063Herbelin, Hugo; Ghilezan, Silvia 5 2008 Control reduction theories: The benefit of structural substitution. Zbl 1138.68020Ariola, Zena M.; Herbelin, Hugo 4 2008 A proof-theoretic foundation of abortive continuations. Zbl 1128.68089Ariola, Zena M.; Herbelin, Hugo; Sabry, Amr 10 2007 On the degeneracy of \(\Sigma\)-types in presence of computational classical logic. Zbl 1114.03029Herbelin, Hugo 6 2005 A type-theoretic foundation of continuations and prompts. Zbl 1323.68090Ariola, Zena M.; Herbelin, Hugo; Sabry, Amr 6 2004 Minimal classical logic and control operators. Zbl 1039.03019Ariola, Zena M.; Herbelin, Hugo 14 2003 Explicit substitutions and reducibility. Zbl 0984.03014Herbelin, Hugo 3 2001 The duality of computation. Zbl 1321.68146Curien, Pierre-Louis; Herbelin, Hugo 73 2000 A \(\lambda\)-caclulus structure isomorphic to Gentzen-style sequent calculus structure. Zbl 1044.03509Herbelin, Hugo 33 1995 \(A\)-translation and looping combinators in pure type systems. Zbl 0817.03007Coquand, Thierry; Herbelin, Hugo 8 1994 The two list algorithm for the knapsack problem on an FPS T20. Zbl 0669.65051Cosnard, M.; Ferreira, A. G.; Herbelin, H. 3 1989 all cited Publications top 5 cited Publications all top 5 Cited by 217 Authors 10 Ariola, Zena M. 7 Herbelin, Hugo 6 Downen, Paul 6 Espírito Santo, José Carlos 4 Guerrieri, Giulio 4 Kesner, Delia 4 Lengrand, Stéphane Jean Eric 4 Pinto, Luís F. 3 Accattoli, Beniamino 3 Aschieri, Federico 3 Barthe, Gilles 3 Biernacka, Małgorzata 3 Biernacki, Dariusz 3 de’Liguoro, Ugo 3 Geuvers, Jan Herman 3 Hatcliff, John 3 Ilik, Danko 3 Kimura, Daisuke 3 Pimentel, Elaine 3 Saurin, Alexis 3 Sørensen, Morten Heine B. 3 van Bakel, Steffen 2 Bonelli, Eduardo 2 Doczkal, Christian 2 Feller, Federico 2 Ghilezan, Silvia 2 Haeusler, Edward Hermann 2 Hetzl, Stefan 2 Hyland, J. Martin E. 2 Ivetić, Jelena 2 Johnson-Freyd, Philip 2 Kaliszyk, Cezary 2 Kikuchi, Kentaro 2 Lee, Gyesik 2 Lenglet, Sergueï 2 Lescanne, Pierre 2 Levy, Paul Blain 2 Liang, Chuck 2 Marin, Sonia 2 Matthes, Ralph 2 Miller, Dale Allen 2 Miquey, Étienne 2 Moortgat, Michael 2 Naibo, Alberto 2 Petković, Miodrag S. 2 Petrolo, Mattia 2 Polonsky, Andrew 2 Sabry, Amr 2 Sacerdoti Coen, Claudio 2 Smolka, Gert 2 Tatsuta, Makoto 2 Terui, Kazushige 2 Urban, Christian 2 Vial, Pierre 1 Abramsky, Samson 1 Ahmed, Amal 1 Aiguier, Marc 1 Ayhan, Sara 1 Barbanera, Franco 1 Basaldella, Michele 1 Battyányi, Péter 1 Bellin, Gianluigi 1 Bentzen, Bruno 1 Bernardi, Raffaella 1 Bimbó, Katalin 1 Bohrer, Brandon 1 Bowman, William J. 1 Boyer, Vincent 1 Brock-Nannestad, Taus 1 Brunel, Aloïs 1 Caires, Luís 1 Cerrito, Serenella 1 Ciabattoni, Agata 1 Cockx, Jesper 1 Cohen, Liron 1 Coquand, Thierry 1 Crolard, Tristan 1 Curien, Pierre-Louis 1 Dabrowski, Yoann 1 Dal Lago, Ugo 1 Danos, Vincent 1 Danvy, Olivier 1 de Barros Santos, Jefferson 1 del Carmen González Huesca, Lourdes 1 Devesas Campos, Marco 1 Devriese, Dominique 1 Dezani-Ciancaglini, Mariangiola 1 Dinis, Bruno 1 Dougherty, Dan 1 Dowek, Gilles 1 Dunn, Jon Michael 1 Dyckhoff, Roy 1 Eades, Harley III 1 Ehrhard, Thomas 1 El Baz, Didier 1 Elkihel, Moussa 1 Endrullis, Jörg 1 Englander, Cecilia 1 Faggian, Claudia 1 Faro, Sofia Abreu ...and 117 more Authors all top 5 Cited in 29 Serials 17 Theoretical Computer Science 12 Annals of Pure and Applied Logic 8 Information and Computation 8 Journal of Functional Programming 8 Logical Methods in Computer Science 7 MSCS. Mathematical Structures in Computer Science 4 Journal of Automated Reasoning 4 Higher-Order and Symbolic Computation 3 Journal of Philosophical Logic 2 Studia Logica 2 Archive for Mathematical Logic 2 Theory of Computing Systems 2 The Journal of Logic and Algebraic Programming 2 Logica Universalis 2 Journal of Logical and Algebraic Methods in Programming 1 The Journal of Symbolic Logic 1 Notre Dame Journal of Formal Logic 1 Journal of Symbolic Computation 1 New Generation Computing 1 Computers & Operations Research 1 Japan Journal of Industrial and Applied Mathematics 1 Numerical Algorithms 1 Journal of Applied Non-Classical Logics 1 Theory and Applications of Categories 1 Topoi 1 ACM Transactions on Computational Logic 1 RAIRO. Theoretical Informatics and Applications 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Higher Structures all top 5 Cited in 13 Fields 118 Mathematical logic and foundations (03-XX) 96 Computer science (68-XX) 7 Category theory; homological algebra (18-XX) 2 Algebraic topology (55-XX) 2 Numerical analysis (65-XX) 1 Field theory and polynomials (12-XX) 1 Real functions (26-XX) 1 Functions of a complex variable (30-XX) 1 Functional analysis (46-XX) 1 Convex and discrete geometry (52-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) Citations by Year