default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDRobert L. Constable
Person information
- affiliation: Cornell University, Ithaca, USA
- award (2014): Herbrand Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2021
[c53]Mark Bickford
, Liron Cohen, Robert L. Constable, Vincent Rahli:
Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. CSL 2021: 11:1-11:23
2010 – 2019
- 2019
- [j29]Ariel Kellison, Mark Bickford, Robert L. Constable:
Implementing Euclid's straightedge and compass constructions in type theory. Ann. Math. Artif. Intell. 85(2-4): 175-192 (2019) - [j28]Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable:
Bar Induction is Compatible with Constructive Type Theory. J. ACM 66(2): 13:1-13:35 (2019) - [j27]Liron Cohen, Robert L. Constable:
Intuitionistic ancestral logic. J. Log. Comput. 29(4): 469-486 (2019) - 2018
- [c52]Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli:
Computability Beyond Church-Turing via Choice Sequences. LICS 2018: 245-254 - 2017
- [j26]Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable:
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. 148: 26-48 (2017) - [c51]Vincent Rahli, Mark Bickford, Robert L. Constable:
Bar induction: The good, the bad, and the ugly. LICS 2017: 1-12 - 2015
- [j25]Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable:
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015) - [c50]Liron Cohen, Robert L. Constable:
Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language. WoLLIC 2015: 14-26 - 2014
- [j24]Robert L. Constable, Mark Bickford:
Intuitionistic completeness of first-order logic. Ann. Pure Appl. Log. 165(1): 164-198 (2014) - [c49]Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable:
Developing Correctly Replicated Databases Using Formal Tools. DSN 2014: 395-406 - [i4]Robert L. Constable:
Virtual Evidence: A Constructive Semantics for Classical Logics. CoRR abs/1409.0266 (2014) - 2012
- [c48]Robert L. Constable:
Proof Assistants and the Dynamic Nature of Formal Theories. ATx/WInG@IJCAR 2012: 1-15 - [c47]Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable:
ShadowDB: A Replicated Database on a Synthesized Consensus Core. HotDep 2012 - [c46]Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable:
A diversified and correct-by-construction broadcast service. ICNP 2012: 1-6 - [c45]Robert L. Constable:
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer. LICS 2012: 2-8 - [c44]Robert L. Constable:
Proof Assistants and the Dynamic Nature of Formal Theories. PxTP 2012: 1-15 - [e3]Robert L. Constable, Alexandra Silva:
Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 7230, Springer 2012, ISBN 978-3-642-29484-6 [contents] - [r1]Fairouz Kamareddine, Twan Laan, Robert L. Constable:
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory. Sets and Extensions in the Twentieth Century 2012: 801-845 - 2011
- [j23]Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride:
Knowledge-Based Synthesis of Distributed Systems Using Event Structures. Log. Methods Comput. Sci. 7(2) (2011) - [i3]Robert L. Constable:
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP. CoRR abs/1109.3370 (2011) - [i2]Robert L. Constable, Mark Bickford:
Intuitionistic Completeness of First-Order Logic. CoRR abs/1110.1614 (2011)
2000 – 2009
- 2009
- [j22]Robert L. Constable, Wojciech Moczydlowski:
Extracting the resolution algorithm from a completeness proof for the propositional calculus. Ann. Pure Appl. Log. 161(3): 337-348 (2009) - [j21]Robert L. Constable:
Computational type theory. Scholarpedia 4(2): 7618 (2009) - [c43]Robert L. Constable:
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge. Efficient Algorithms 2009: 3-17 - 2008
- [j20]Robert L. Constable, Wojciech Moczydlowski:
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. Log. Methods Comput. Sci. 4(3) (2008) - [i1]Robert L. Constable, Wojciech Moczydlowski:
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. CoRR abs/0806.1281 (2008) - 2007
- [c42]Robert L. Constable, Wojciech Moczydlowski:
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. LFCS 2007: 147-161 - 2006
- [j19]Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, E. Moran:
Innovations in computational type theory using Nuprl. J. Appl. Log. 4(4): 428-469 (2006) - [c41]Robert L. Constable, Wojciech Moczydlowski:
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics. IJCAR 2006: 162-176 - 2004
- [c40]Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride:
Knowledge-Based Synthesis of Distributed Systems Using Event Structures. LPAR 2004: 449-465 - [c39]Lori Lorigo, Jon M. Kleinberg, Richard Eaton, Robert L. Constable:
A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. MKM 2004: 220-235 - 2003
- [c38]Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, Xin Yu:
MetaPRL - A Modular Logical Environment. TPHOLs 2003: 287-303 - 2001
- [c37]Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable:
Protocol Switching: Exploiting Meta-Properties. ICDCS Workshops 2001: 37-42 - 2000
- [c36]Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan C. Uribe:
Constructively formalizing automata theory. Proof, Language, and Interaction 2000: 213-238 - [c35]Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo:
The Nuprl Open Logical Environment. CADE 2000: 170-176
1990 – 1999
- 1999
- [j18]William E. Aitken, Robert L. Constable, Judith L. Underwood:
Metalogical Frameworks II: Developing a Reflected Decision Procedure. J. Autom. Reason. 22(2): 171-221 (1999) - [c34]Amanda M. Holland-Minkley, Regina Barzilay, Robert L. Constable:
Verbalization of High-Level Formal Proofs. AAAI/IAAI 1999: 277-284 - [c33]Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth P. Birman, Robert L. Constable:
Building reliable, high-performance communication systems from components. SOSP 1999: 80-92 - 1998
- [j17]Robert L. Constable:
A Note on Complexity Measures for Inductive Classes in Constructive Type Theory. Inf. Comput. 143(2): 137-153 (1998) - 1997
- [c32]Robert L. Constable:
ML Programming in Constructive Type Theory (abstract). TPHOLs 1997: 87 - 1995
- [j16]Robert L. Constable, Donald A. Preece, Nicholas C. K. Phillips, Thomas Dale Porter, Walter D. Wallis:
Single change neighbor designs. Australas. J Comb. 11: 247-256 (1995) - [c31]Robert L. Constable:
Experience with Type Theory as a Foundation for Computer Science. LICS 1995: 266-279 - 1994
- [c30]Robert L. Constable:
Exporting and Refecting Abstract Metamathematics. CADE 1994: 529 - [c29]Robert L. Constable:
Expressing Computational Complexity in Constructive Type Theory. LCC 1994: 131-144 - 1993
- [j15]Robert L. Constable, Scott F. Smith:
Computational Foundations of Basic Recursive Function Theory. Theor. Comput. Sci. 121(1&2): 89-112 (1993) - 1992
- [c28]Robert L. Constable:
Formal Theories and Software Systems: Fundamental Connections between Computer Science and Logic. 25th Anniversary of INRIA 1992: 105-127 - 1991
- [c27]Robert L. Constable:
Type Theory as a Foundation for Computer Science. TACS 1991: 226-243 - 1990
- [c26]Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William E. Aitken:
The Semantics of Reflected Proof. LICS 1990: 95-105
1980 – 1989
- 1988
- [c25]Robert L. Constable, Scott F. Smith:
Computational Foundations of Basic Recursive Function Theory. LICS 1988: 360-371 - 1987
- [c24]Robert L. Constable, Scott F. Smith:
Partial Objects In Constructive Type Theory. LICS 1987: 183-193 - 1986
- [b2]Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper, Douglas J. Howe, Todd B. Knoblock, Nax Paul Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith:
Implementing mathematics with the Nuprl proof development system. Prentice Hall 1986, ISBN 978-0-13-451832-9, pp. I-X, 1-299 - [c23]Todd B. Knoblock, Robert L. Constable:
Formalized Metareasoning in Type Theory. LICS 1986: 237-248 - [c22]Nax Paul Mendler, Prakash Panangaden, Robert L. Constable:
Infinite Objects in Type Theory. LICS 1986: 249-255 - 1985
- [j14]Robert L. Constable, Todd B. Knoblock, Joseph L. Bates:
Writing Programs that Construct Proofs. J. Autom. Reason. 1(3): 285-326 (1985) - [j13]Joseph L. Bates, Robert L. Constable:
Proofs as Programs. ACM Trans. Program. Lang. Syst. 7(1): 113-136 (1985) - [c21]Robert L. Constable, Nax Paul Mendler:
Recursive Definitions in Type Theory. Logic of Programs 1985: 61-78 - 1984
- [j12]Robert L. Constable, Daniel R. Zlatin:
The Type Theory of PL/CV3. ACM Trans. Program. Lang. Syst. 6(1): 94-117 (1984) - 1983
- [j11]Robert L. Constable:
Programs as Proofs: A Synopsis. Inf. Process. Lett. 16(3): 105-112 (1983) - [c20]Robert L. Constable:
Constructive Mathematics as a Programming Logic I: Some Principles of Theory. FCT 1983: 64-77 - [c19]Robert L. Constable:
Mathematics as Programming. Logic of Programs 1983: 116-128 - [c18]Robert L. Constable:
Partial functions in constructive formal theories. Theoretical Computer Science 1983: 1-18 - 1982
- [b1]Robert L. Constable, Scott Johnson, C. D. Eichenlaub:
An Introduction to the PL/CV2 Programming Logic. Lecture Notes in Computer Science 135, Springer 1982, ISBN 3-540-11492-0 - 1981
- [j10]Robert L. Constable:
VERking in constructive set theory. ACM SIGSOFT Softw. Eng. Notes 6(3): 58-60 (1981) - [c17]Robert L. Constable, Daniel R. Zlatin:
The Type Theory of PL/CV 3. Logic of Programs 1981: 72-93 - 1980
- [j9]Harry B. Hunt III, Robert L. Constable, Sartaj Sahni:
On the Computational Complexity of Program Scheme Equivalence. SIAM J. Comput. 9(2): 396-416 (1980) - [c16]Robert L. Constable:
Programs and Types. FOCS 1980: 118-128
1970 – 1979
- 1979
- [j8]Robert L. Constable, James E. Donahue:
A Hierarchial Approach to Formal Semantics With Application to the Definition of PL/CS. ACM Trans. Program. Lang. Syst. 1(1): 98-114 (1979) - [c15]Robert L. Constable, Scott Johnson:
A PL/CV Precis. POPL 1979: 7-20 - 1977
- [c14]Robert L. Constable:
A Constructive Programming Logic. IFIP Congress 1977: 733-738 - [c13]Robert L. Constable:
On the Theory of Programming Logics. STOC 1977: 269-285 - 1976
- [j7]Herbert Egli, Robert L. Constable:
Computability Concepts for Programming Language Semantics. Theor. Comput. Sci. 2(2): 133-145 (1976) - 1975
- [c12]Herbert Egli, Robert L. Constable:
Computability Concepts for Programming Language Semantics. STOC 1975: 98-106 - 1974
- [j6]Robert L. Constable, David Park:
Special issue on semantics and program schemas SIAM journal on computing. SIGACT News 6(4): 32 (1974) - [e2]Robert L. Constable, Robert W. Ritchie, Jack W. Carlyle, Michael A. Harrison:
Proceedings of the 6th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1974, Seattle, Washington, USA. ACM 1974 [contents] - 1973
- [c11]Robert L. Constable:
Type Two Computational Complexity. STOC 1973: 108-121 - [e1]Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, H. Raymond Strong:
Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA. ACM 1973 [contents] - 1972
- [j5]Robert L. Constable:
The Operator Gap. J. ACM 19(1): 175-183 (1972) - [j4]Robert L. Constable, Allan Borodin:
Subrecursive Programming Languages, Part I: efficiency and program structure. J. ACM 19(3): 526-568 (1972) - [j3]Robert L. Constable, Steven S. Muchnick:
Subrecursive Program Schemata I & II: I. Undecidable Equivalence problems; II. Decidable Equivalence Problems. J. Comput. Syst. Sci. 6(6): 480-537 (1972) - [j2]Robert L. Constable, David Gries:
On Classes of Program Schemata. SIAM J. Comput. 1(1): 66-118 (1972) - [c10]John C. Cherniavsky, Robert L. Constable:
Representing Program Schemes in Logic. SWAT 1972: 27-39 - [c9]Robert L. Constable, Steven S. Muchnick:
Subrecursive Program Schemata I & II: I. Undecidable Equivalence Problems; II. Decidable Equivalence Problems. STOC 1972: 1-17 - 1971
- [j1]Robert L. Constable:
Subrecursive Programming Languages. II. On Program Size. J. Comput. Syst. Sci. 5(3): 315-334 (1971) - [c8]Robert L. Constable, David Gries:
On Classes of Program Schemata. SWAT 1971: 5-19 - [c7]Robert L. Constable:
Constructive Mathematics and Automatic Program Writers. IFIP Congress (1) 1971: 229-233 - [c6]Robert L. Constable:
Loop Schemata. STOC 1971: 24-39 - [c5]Robert L. Constable, Juris Hartmanis:
Complexity of Formal Translations and Speed-Up Results. STOC 1971: 244-250 - 1970
- [c4]Robert L. Constable, Allan Borodin:
On the Efficiency of Programs in Subrecursive Formalisms (Incomplete Version, Extended Abstract). SWAT 1970: 60-67 - [c3]Robert L. Constable:
On the Size of Programs in Subrecursive Formalisms. STOC 1970: 1-9
1960 – 1969
- 1969
- [c2]Allan Borodin, Robert L. Constable, John E. Hopcroft:
Dense and Non-Dense Families of Complexity Classes. SWAT 1969: 7-19 - [c1]Robert L. Constable:
The Operator Gap. SWAT 1969: 20-26
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-21 00:13 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
