Edit Profile (opens in new tab) Constable, Robert Lee Co-Author Distance Author ID: constable.robert-l Published as: Constable, Robert L.; Constable, Robert; Constable, R. L.; Constable, Robert C. more...less Further Spellings: Constable, Bob Homepage: http://www.cs.cornell.edu/home/rc/ External Links: MGP · Wikidata · ResearchGate · IdRef Documents Indexed: 68 Publications since 1971, including 2 Books 1 Contribution as Editor · 3 Further Contributions Co-Authors: 37 Co-Authors with 44 Joint Publications 721 Co-Co-Authors all top 5 Co-Authors 25 single-authored 9 Bickford, Mark 4 Cohen, Liron 4 Moczydłowski, Wojciech 3 Allen, Stuart F. 3 Eaton, Richard 3 Lorigo, Lori 3 Muchnick, Steven S. 3 Rahli, Vincent 2 Bates, Joseph L. 2 Egli, Herbert 2 Gries, David 2 Halpern, Joseph Yehuda 2 Kreitz, Christoph 2 O’Donnell, Michael J. 2 Petride, Sabina 2 Zlatin, Daniel R. 1 Aczel, Peter 1 Aho, Alfred Vaino 1 Ahrens, Benedikt 1 Aitken, William E. 1 Altenkirch, Thorsten 1 Andler, Sten F. 1 Andrews, Gregory R. 1 Angiuli, Carlo 1 Avigad, Jeremy 1 Awodey, Steve 1 Banning, John 1 Barras, Bruno 1 Basin, David A. 1 Bauer, Andrej 1 Bernstein, Philip A. 1 Bertot, Yves 1 Bezem, Marc 1 Bordg, Anthony 1 Borodin, Allan B. 1 Brunerie, Guillaume 1 Cartwright, Robert 1 Casanova, Marco Antonio 1 Clarke, Edmund Melson jun. 1 Cohen, Cyril 1 Cohen, Norman H. 1 Cohen, Richard M. 1 Cohen, Rina S. 1 Coquand, Thierry 1 Cousot, Patrick 1 Cousot, Radhia 1 Crary, Karl 1 Critcher, Adrienne 1 Curien, Pierre-Louis 1 1 Dybjer, Peter 1 Eichenlaub, C. D. 1 Finster, Eric 1 Fleck, Arthur C. 1 Fong, Amelia C. 1 Fraser, Christopher W. 1 Gambino, Nicola 1 Garner, Richard 1 Gerhart, Susan L. 1 Glicksberg, Irving Leonard 1 Gonthier, Georges 1 Good, Donald I. 1 Grayson, Daniel Richard 1 Greif, Irene 1 Gull, Walter E. 1 Hales, Thomas Callister 1 Harel, David 1 Harper, Robert 1 Harry, E. 1 Hartmanis, Juris 1 Herbelin, Hugo 1 Hickey, Jason J. 1 Hoffmann, Christoph M. 1 Hofmann, Martin 1 Hofstra, Pieter J. W. 1 Hötzel Escardó, Martín 1 Hou (Favonia), Kuen-Bang 1 Howe, Douglas J. 1 Hunt, Harry Bowen III 1 Jenkins, Michael A. 1 Jones, Neil D. 1 Joyal, André 1 Kamareddine, Fairouz D. 1 Kapulkin, Krzysztof 1 Kellison, Ariel 1 Kleinberg, Jon Michael 1 Knoblock, Todd B. 1 Kock, Joachim 1 Kraus, Nicolai 1 Laan, Twan 1 Lee, Stanley 1 Li, Nuo 1 Licata, Dan 1 Liu, Ken-Chih 1 Lumsdaine, Peter LeFanu 1 Luo, Zhaohui 1 Mahboubi, Assia 1 Martin-Löf, Per 1 McCarthy, John 1 Melikhov, Sergey Aleksandrovich ...and 42 more Co-Authors all top 5 Serials 3 ACM Transactions on Programming Languages and Systems 2 Journal of the Association for Computing Machinery 2 Journal of Computer and System Sciences 2 SIAM Journal on Computing 2 Theoretical Computer Science 2 Annals of Pure and Applied Logic 2 Journal of Automated Reasoning 2 Lecture Notes in Computer Science 2 Logical Methods in Computer Science 1 Information Processing Letters 1 Kiberneticheskiĭ Sbornik. Novaya Seriya 1 Utilitas Mathematica 1 Information and Computation 1 Journal of Logic and Computation 1 Annals of Mathematics and Artificial Intelligence 1 Journal of the ACM 1 Journal of Applied Logic 1 Contemporary Mathematics all top 5 Fields 60 Computer science (68-XX) 42 Mathematical logic and foundations (03-XX) 4 History and biography (01-XX) 3 General and overarching topics; collections (00-XX) 1 Combinatorics (05-XX) 1 Category theory; homological algebra (18-XX) 1 Geometry (51-XX) 1 Algebraic topology (55-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 52 Publications have been cited 244 times in 191 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 On classes of program schemata. Zbl 0247.68031Constable, Robert L.; Gries, David 21 1972 Computability concepts for programming language semantics. Zbl 0352.68042Egli, Herbert; Constable, Robert L. 20 1976 Innovations in computational type theory using Nuprl. Zbl 1107.68090Allen, S. F.; Bickford, M.; Constable, R. L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. 15 2006 The operator gap. Zbl 0229.68016Constable, Robert L. 15 1972 On the computational complexity of program scheme equivalence. Zbl 0447.68038Hunt, H. B. III; Constable, R. L.; Sahni, S. 13 1980 Proofs as programs. Zbl 0555.68003Bates, Joseph L.; Constable, Robert L. 12 1985 Recursive definitions in type theory. Zbl 0579.68019Constable, R. L.; Mendler, N. P. 12 1985 Subrecursive programming languages. I: Efficiency and program structure. Zbl 0259.68036Constable, Robert L.; Borodin, Allan B. 12 1972 Metalogical frameworks. Zbl 0922.03019Basin, David A.; Constable, Robert L. 10 1993 Type two computational complexity. Zbl 0306.68022Constable, Robert L. 9 1973 The type theory of PL/CV3. Zbl 0522.68020Constable, Robert L.; Zlatin, Daniel R. 6 1984 Intuitionistic completeness of first-order logic. Zbl 1345.03114Constable, Robert; Bickford, Mark 6 2014 Constructive mathematics and automatic program writers. Zbl 0255.68014Constable, Robert L. 6 1972 Writing programs that construct proofs. Zbl 0615.68063Constable, R. L.; Knoblock, T. B.; Bates, J. L. 5 1985 An introduction to the PL/CV2 programming logic. Zbl 0496.68008Constable, R. L.; Johnson, S. D.; Eichenlaub, C. D. 5 1982 Programs as proofs: A synopsis. Zbl 0514.68043Constable, Robert L. 5 1983 Finding computational content in classical proofs. Zbl 0754.03040Constable, Robert; Murthy, Chet 5 1991 Computational foundations of basic recursive function theory. Zbl 0798.03046Constable, Robert L.; Smith, Scott F. 5 1993 The Nuprl open logical environment. Zbl 0963.68532Allen, Stuart F.; Constable, Robert L.; Eaton, Rich; Kreitz, Christoph; Lorigo, Lori 4 2000 Nuprl’s class theory and its applications. Zbl 0995.68014Constable, Robert L.; Hickey, Jason 4 2000 Types in logic, mathematics and programming. Zbl 0914.03056Constable, Robert L. 4 1998 Complexity of formal translations and speed-up results. Zbl 0257.68036Constable, R. L.; Hartmanis, J. 4 1971 The type theory of PL/CV3. Zbl 0506.03002Constable, Robert L.; Zlatin, Daniel R. 3 1982 Implementing metamathematics as an approach to automatic theorem proving. Zbl 0704.68094Constable, R. L.; Howe, D. J. 3 1990 Computability concepts for programming language semantics. Zbl 0359.68017Egli, Herbert; Constable, Robert L. 3 1975 Extracting programs from constructive HOL proofs via IZF set-theoretic semantics. Zbl 1222.68359Constable, Robert; Moczydłowski, Wojciech 3 2006 Computability beyond Church-Turing via choice sequences. Zbl 1452.03133Bickford, Mark; Cohen, Liron; Constable, Robert L.; Rahli, Vincent 3 2018 Constructive mathematics as a programming logic. I: Some principles of theory. Zbl 0561.68028Constable, Robert L. 2 1985 Errett Bishop: reflections on him and his research. (Proceedings of the Memorial Meeting for Errett Bishop held at the University of California, San Diego, September 24, 1983). Zbl 0579.01015 2 1985 Naïve computational type theory. Zbl 1127.03322Constable, Robert L. 2 2002 On classes of program schemata. Zbl 0408.68019Constable, Robert L.; Gries, David 2 1977 Knowledge-based synthesis of distributed systems using event structures. Zbl 1108.68491Bickford, Mark; Constable, Robert C.; Halpern, Joseph Y.; Petride, Sabina 2 2005 Extracting the resolution algorithm from a completeness proof for the propositional calculus. Zbl 1221.03015Constable, Robert; Moczydłowski, Wojciech 2 2009 Bar induction. The good, the bad, and the ugly. Zbl 1457.68298Rahli, Vincent; Bickford, Mark; Constable, Robert L. 2 2017 The structure of Nuprl’s type theory. Zbl 0876.03010Constable, Robert L. 2 1997 Using reflection to explain and enhance type theory. Zbl 0831.68101Constable, Robert L. 2 1995 Bar induction is compatible with constructive type theory. Zbl 1427.03066Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L. 1 2019 The role of finite automata in the development of modern computing theory. Zbl 0468.68060Constable, Robert L. 1 1980 Partial functions in constructive formal theories. Zbl 0505.03027Constable, Robert L. 1 1982 Logic and program semantics. Essays dedicated to Dexter Kozen on the occasion of his 60th birthday. Zbl 1241.68012 1 2012 Computational complexity and induction for partial computable functions in type theory. Zbl 1016.03044Constable, Robert L.; Crary, Karl 1 2002 Subrecursive program schemata. I, II. Zbl 0354.68022Constable, Robert L.; Muchnick, Steven S. 1 1972 A constructive programming logic. Zbl 0363.68029Constable, Robert L. 1 1977 A graph-based approach towards discerning inherent structures in a digital library of formal mathematics. Zbl 1108.68595Lorigo, Lori; Kleinberg, Jon; Eaton, Richard; Constable, Robert 1 2004 Subrecursive programming languages. II. On program size. Zbl 0218.68011Constable, R. L. 1 1971 Polymorphic logic. Zbl 1315.03043Bickford, Mark; Constable, Robert 1 2012 A note on complexity measures for inductive classes in constructive type theory. Zbl 0916.03039Constable, Robert L. 1 1998 Metalogical frameworks. II: Developing a reflected decision procedure. Zbl 0922.03020Aitken, William E.; Constable, Robert L.; Underwood, Judith L. 1 1999 Loop schemata. Zbl 0257.68025Constable, Robert L. 1 1971 Subrecursive-programming languages. III: The multiple-recursive functions. Zbl 0265.68019Constable, Robert L. 1 1971 Type theory as a foundation for computer science. Zbl 1496.03054Constable, Robert L. 1 1991 Bar induction is compatible with constructive type theory. Zbl 1427.03066Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L. 1 2019 Computability beyond Church-Turing via choice sequences. Zbl 1452.03133Bickford, Mark; Cohen, Liron; Constable, Robert L.; Rahli, Vincent 3 2018 Bar induction. The good, the bad, and the ugly. Zbl 1457.68298Rahli, Vincent; Bickford, Mark; Constable, Robert L. 2 2017 Intuitionistic completeness of first-order logic. Zbl 1345.03114Constable, Robert; Bickford, Mark 6 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 Logic and program semantics. Essays dedicated to Dexter Kozen on the occasion of his 60th birthday. Zbl 1241.68012 1 2012 Polymorphic logic. Zbl 1315.03043Bickford, Mark; Constable, Robert 1 2012 Extracting the resolution algorithm from a completeness proof for the propositional calculus. Zbl 1221.03015Constable, Robert; Moczydłowski, Wojciech 2 2009 Innovations in computational type theory using Nuprl. Zbl 1107.68090Allen, S. F.; Bickford, M.; Constable, R. L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. 15 2006 Extracting programs from constructive HOL proofs via IZF set-theoretic semantics. Zbl 1222.68359Constable, Robert; Moczydłowski, Wojciech 3 2006 Knowledge-based synthesis of distributed systems using event structures. Zbl 1108.68491Bickford, Mark; Constable, Robert C.; Halpern, Joseph Y.; Petride, Sabina 2 2005 A graph-based approach towards discerning inherent structures in a digital library of formal mathematics. Zbl 1108.68595Lorigo, Lori; Kleinberg, Jon; Eaton, Richard; Constable, Robert 1 2004 Naïve computational type theory. Zbl 1127.03322Constable, Robert L. 2 2002 Computational complexity and induction for partial computable functions in type theory. Zbl 1016.03044Constable, Robert L.; Crary, Karl 1 2002 The Nuprl open logical environment. Zbl 0963.68532Allen, Stuart F.; Constable, Robert L.; Eaton, Rich; Kreitz, Christoph; Lorigo, Lori 4 2000 Nuprl’s class theory and its applications. Zbl 0995.68014Constable, Robert L.; Hickey, Jason 4 2000 Metalogical frameworks. II: Developing a reflected decision procedure. Zbl 0922.03020Aitken, William E.; Constable, Robert L.; Underwood, Judith L. 1 1999 Types in logic, mathematics and programming. Zbl 0914.03056Constable, Robert L. 4 1998 A note on complexity measures for inductive classes in constructive type theory. Zbl 0916.03039Constable, Robert L. 1 1998 The structure of Nuprl’s type theory. Zbl 0876.03010Constable, Robert L. 2 1997 Using reflection to explain and enhance type theory. Zbl 0831.68101Constable, Robert L. 2 1995 Metalogical frameworks. Zbl 0922.03019Basin, David A.; Constable, Robert L. 10 1993 Computational foundations of basic recursive function theory. Zbl 0798.03046Constable, Robert L.; Smith, Scott F. 5 1993 Finding computational content in classical proofs. Zbl 0754.03040Constable, Robert; Murthy, Chet 5 1991 Type theory as a foundation for computer science. Zbl 1496.03054Constable, Robert L. 1 1991 Implementing metamathematics as an approach to automatic theorem proving. Zbl 0704.68094Constable, R. L.; Howe, D. J. 3 1990 Proofs as programs. Zbl 0555.68003Bates, Joseph L.; Constable, Robert L. 12 1985 Recursive definitions in type theory. Zbl 0579.68019Constable, R. L.; Mendler, N. P. 12 1985 Writing programs that construct proofs. Zbl 0615.68063Constable, R. L.; Knoblock, T. B.; Bates, J. L. 5 1985 Constructive mathematics as a programming logic. I: Some principles of theory. Zbl 0561.68028Constable, Robert L. 2 1985 Errett Bishop: reflections on him and his research. (Proceedings of the Memorial Meeting for Errett Bishop held at the University of California, San Diego, September 24, 1983). Zbl 0579.01015 2 1985 The type theory of PL/CV3. Zbl 0522.68020Constable, Robert L.; Zlatin, Daniel R. 6 1984 Programs as proofs: A synopsis. Zbl 0514.68043Constable, Robert L. 5 1983 An introduction to the PL/CV2 programming logic. Zbl 0496.68008Constable, R. L.; Johnson, S. D.; Eichenlaub, C. D. 5 1982 The type theory of PL/CV3. Zbl 0506.03002Constable, Robert L.; Zlatin, Daniel R. 3 1982 Partial functions in constructive formal theories. Zbl 0505.03027Constable, Robert L. 1 1982 On the computational complexity of program scheme equivalence. Zbl 0447.68038Hunt, H. B. III; Constable, R. L.; Sahni, S. 13 1980 The role of finite automata in the development of modern computing theory. Zbl 0468.68060Constable, Robert L. 1 1980 On classes of program schemata. Zbl 0408.68019Constable, Robert L.; Gries, David 2 1977 A constructive programming logic. Zbl 0363.68029Constable, Robert L. 1 1977 Computability concepts for programming language semantics. Zbl 0352.68042Egli, Herbert; Constable, Robert L. 20 1976 Computability concepts for programming language semantics. Zbl 0359.68017Egli, Herbert; Constable, Robert L. 3 1975 Type two computational complexity. Zbl 0306.68022Constable, Robert L. 9 1973 On classes of program schemata. Zbl 0247.68031Constable, Robert L.; Gries, David 21 1972 The operator gap. Zbl 0229.68016Constable, Robert L. 15 1972 Subrecursive programming languages. I: Efficiency and program structure. Zbl 0259.68036Constable, Robert L.; Borodin, Allan B. 12 1972 Constructive mathematics and automatic program writers. Zbl 0255.68014Constable, Robert L. 6 1972 Subrecursive program schemata. I, II. Zbl 0354.68022Constable, Robert L.; Muchnick, Steven S. 1 1972 Complexity of formal translations and speed-up results. Zbl 0257.68036Constable, R. L.; Hartmanis, J. 4 1971 Subrecursive programming languages. II. On program size. Zbl 0218.68011Constable, R. L. 1 1971 Loop schemata. Zbl 0257.68025Constable, Robert L. 1 1971 Subrecursive-programming languages. III: The multiple-recursive functions. Zbl 0265.68019Constable, Robert L. 1 1971 all cited Publications top 5 cited Publications all top 5 Cited by 231 Authors 12 Constable, Robert Lee 7 Spreen, Dieter 5 Weihrauch, Klaus 4 Basin, David A. 4 Bickford, Mark 4 Harper, Robert 4 Ibarra, Oscar H. 4 Meseguer Guaita, José 4 Stewart, Iain A. 4 Urzyczyn, Paweł 3 Angiuli, Carlo 3 Anisimov, Anatoly V. 3 Cohen, Liron 3 Danicic, Sebastian 3 Hierons, Robert Mark 3 Kfoury, Assaf J. 3 Kreitz, Christoph 3 Laurence, Michael R. 3 Leininger, Brian S. 3 Meyer, Albert Ronald 3 Moczydłowski, Wojciech 3 Seiferas, Joel I. 3 Stump, Aaron 2 Bel’tyukov, Anatoliĭ Petrovich 2 Berger, Ulrich 2 Calude, Cristian S. 2 Coquand, Thierry 2 Hainry, Emmanuel 2 Huet, Gerard P. 2 Hunt, Harry Bowen III 2 Jenkins, Christopher 2 Kapron, Bruce M. 2 Longo, Giuseppe 2 Matthews, Seán 2 Nepeĭvoda, Nikolaĭ Nikolaevich 2 Péchoux, Romain 2 Rabe, Florian 2 Rahli, Vincent 2 Rosenkrantz, Daniel J. 2 Smyth, Michael B. 2 Steinberg, Florian 2 Sterling, Jonathan 2 Stoltenberg-Hansen, Viggo 2 Tiuryn, Jerzy 2 Zimand, Marius 1 Abramsky, Samson 1 Allen, Stuart F. 1 Arnold, André 1 Arratia-Quesada, Argimiro Alejandro 1 Arratia, Argimiro A. 1 Aspinall, David 1 Atkinson, Mike D. 1 Autexier, Serge 1 Ayala-Rincón, Mauricio 1 Ayari, Abdelwaheb 1 Backhouse, Roland C. 1 Barringer, Howard 1 Beeri, Catriel 1 Beeson, Michael J. 1 Bellman, Kirstie L. 1 Bentzen, Bruno 1 Benzinger, Ralph 1 Benzmüller, Christoph Ewald 1 Berarducci, Alessandro 1 Bhaskar, Siddharth 1 Böhm, Corrado 1 Bossi, Annalisa 1 Bove, Ana 1 Buchholz, Wilfried 1 Caldwell, James L. 1 Capkun, Srdjan 1 Capretta, Venanzio 1 Case, John 1 Chen, Shuwei 1 Cherniavsky, John C. 1 Chisholm, Paul 1 Cialdea Mayer, Marta 1 Ciraulo, Francesco 1 Clavel, Manuel 1 Coy, Wolfgang 1 Cristiá, Maximiliano 1 Cuykendall, R. 1 Damnjanovic, Zlatan 1 David, Rene 1 Denney, Ewen 1 Di Paola, Robert A. 1 Diehl, Larry 1 Dikovskii, A. Ja. 1 Drămnesc, Isabela 1 Duggan, Dominic 1 Eaton, Richard 1 Egli, Herbert 1 Farmer, William M. 1 Faro, Sofia Abreu 1 Fehr, Elfriede 1 Felty, Amy P. 1 Fernández, Maribel 1 Fischer, Michael J. 1 Fischer, Patrick Carl 1 Friedman, Harvey M. ...and 131 more Authors all top 5 Cited in 43 Serials 40 Theoretical Computer Science 19 Journal of Computer and System Sciences 11 Annals of Pure and Applied Logic 9 Information and Computation 7 Journal of Symbolic Computation 6 Information Processing Letters 6 The Journal of Symbolic Logic 5 Acta Informatica 5 MSCS. Mathematical Structures in Computer Science 3 Mathematical Systems Theory 3 The Journal of Logic and Algebraic Programming 3 Logical Methods in Computer Science 2 Artificial Intelligence 2 Mathematical Notes 2 Computing 2 Journal of Soviet Mathematics 2 Cybernetics 2 Journal of Functional Programming 2 Annals of Mathematics and Artificial Intelligence 2 Journal of Applied Logic 1 Archiv für Mathematische Logik und Grundlagenforschung 1 International Journal of Theoretical Physics 1 Journal of Mathematical Analysis and Applications 1 Algebra Universalis 1 BIT 1 Notre Dame Journal of Formal Logic 1 Proceedings of the American Mathematical Society 1 RAIRO, Informatique Théorique 1 Rendiconti dell’Istituto di Matematica dell’Università di Trieste 1 Transactions of the American Mathematical Society 1 Journal of Automated Reasoning 1 Formal Aspects of Computing 1 Distributed Computing 1 Indagationes Mathematicae. New Series 1 Cybernetics and Systems Analysis 1 Topology Proceedings 1 Soft Computing 1 Philosophical Transactions of the Royal Society of London. Series A. Mathematical, Physical and Engineering Sciences 1 Higher-Order and Symbolic Computation 1 BIT. Nordisk Tidskrift for Informationsbehandling 1 Mathematics in Computer Science 1 Computer Science Review 1 Journal of Membrane Computing all top 5 Cited in 16 Fields 158 Computer science (68-XX) 117 Mathematical logic and foundations (03-XX) 6 Order, lattices, ordered algebraic structures (06-XX) 6 Category theory; homological algebra (18-XX) 4 General topology (54-XX) 3 General algebraic systems (08-XX) 3 Information and communication theory, circuits (94-XX) 2 General and overarching topics; collections (00-XX) 2 History and biography (01-XX) 1 Combinatorics (05-XX) 1 Group theory and generalizations (20-XX) 1 Geometry (51-XX) 1 Algebraic topology (55-XX) 1 Numerical analysis (65-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year Wikidata Timeline The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.