Robert L. Constable

Publication Activity (10 Years)

Years Active: 1969-2021
Publications (10 Years): 9

Top Topics

Classical Logic

Formal Specification

Top Venues

Electron. Commun. Eur. Assoc. Softw. Sci. Technol.

Ann. Math. Artif. Intell.

Publications

Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. CSL (2021)
Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable
Bar Induction is Compatible with Constructive Type Theory. J. ACM 66 (2) (2019)
Ariel Kellison, Mark Bickford, Robert L. Constable
Implementing Euclid's straightedge and compass constructions in type theory. Ann. Math. Artif. Intell. 85 (2-4) (2019)
Liron Cohen, Robert L. Constable
Intuitionistic ancestral logic. J. Log. Comput. 29 (4) (2019)
Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
Computability Beyond Church-Turing via Choice Sequences. LICS (2018)
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 (2017)
Vincent Rahli, Mark Bickford, Robert L. Constable
Bar induction: The good, the bad, and the ugly. LICS (2017)
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)
Liron Cohen, Robert L. Constable
Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language. WoLLIC (2015)
Robert L. Constable
Virtual Evidence: A Constructive Semantics for Classical Logics. CoRR (2014)
Robert L. Constable, Mark Bickford
Intuitionistic completeness of first-order logic. Ann. Pure Appl. Log. 165 (1) (2014)
Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
Developing Correctly Replicated Databases Using Formal Tools. DSN (2014)
Robert L. Constable
Proof Assistants and the Dynamic Nature of Formal Theories. PxTP (2012)
Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable
A diversified and correct-by-construction broadcast service. ICNP (2012)
Robert L. Constable
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer. LICS (2012)
Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
ShadowDB: A Replicated Database on a Synthesized Consensus Core. HotDep (2012)
Robert L. Constable
Proof Assistants and the Dynamic Nature of Formal Theories. ATx/WInG@IJCAR (2012)
Robert L. Constable
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP CoRR (2011)
Robert L. Constable, Mark Bickford
Intuitionistic Completeness of First-Order Logic CoRR (2011)
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)
Robert L. Constable
Computational type theory. Scholarpedia 4 (2) (2009)
Robert L. Constable
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge. Efficient Algorithms (2009)
Robert L. Constable, Wojciech Moczydlowski
Extracting the resolution algorithm from a completeness proof for the propositional calculus. Ann. Pure Appl. Log. 161 (3) (2009)
Robert L. Constable, Wojciech Moczydlowski
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics CoRR (2008)
Robert L. Constable, Wojciech Moczydlowski
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. Log. Methods Comput. Sci. 4 (3) (2008)
Robert L. Constable, Wojciech Moczydlowski
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. LFCS (2007)
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) (2006)
Robert L. Constable, Wojciech Moczydlowski
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics. IJCAR (2006)
Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
Knowledge-Based Synthesis of Distributed Systems Using Event Structures. LPAR (2004)
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)
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)
Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
Protocol Switching: Exploiting Meta-Properties. ICDCS Workshops (2001)
Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan C. Uribe
Constructively formalizing automata theory. Proof, Language, and Interaction (2000)
Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
The Nuprl Open Logical Environment. CADE (2000)
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)
Amanda M. Holland-Minkley, Regina Barzilay, Robert L. Constable
Verbalization of High-Level Formal Proofs. AAAI/IAAI (1999)
William E. Aitken, Robert L. Constable, Judith L. Underwood
Metalogical Frameworks II: Developing a Reflected Decision Procedure. J. Autom. Reason. 22 (2) (1999)
Robert L. Constable
A Note on Complexity Measures for Inductive Classes in Constructive Type Theory. Inf. Comput. 143 (2) (1998)
Robert L. Constable
ML Programming in Constructive Type Theory (abstract). TPHOLs (1997)
Robert L. Constable, Donald A. Preece, Nicholas C. K. Phillips, Thomas Dale Porter, Walter D. Wallis
Single change neighbor designs. Australas. J Comb. 11 (1995)
Robert L. Constable
Experience with Type Theory as a Foundation for Computer Science LICS (1995)
Robert L. Constable
Expressing Computational Complexity in Constructive Type Theory. LCC (1994)
Robert L. Constable
Exporting and Refecting Abstract Metamathematics. CADE (1994)
Robert L. Constable, Scott F. Smith
Computational Foundations of Basic Recursive Function Theory. Theor. Comput. Sci. 121 (1&2) (1993)
Robert L. Constable
Formal Theories and Software Systems: Fundamental Connections between Computer Science and Logic. 25th Anniversary of INRIA (1992)
Robert L. Constable
Type Theory as a Foundation for Computer Science. TACS (1991)
Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William E. Aitken
The Semantics of Reflected Proof LICS (1990)
Robert L. Constable, Scott F. Smith
Computational Foundations of Basic Recursive Function Theory LICS (1988)
Robert L. Constable, Scott F. Smith
Partial Objects In Constructive Type Theory LICS (1987)
N. P. Mendler, Prakash Panangaden, Robert L. Constable
Infinite Objects in Type Theory LICS (1986)
Todd B. Knoblock, Robert L. Constable
Formalized Metareasoning in Type Theory LICS (1986)
Joseph L. Bates, Robert L. Constable
Proofs as Programs. ACM Trans. Program. Lang. Syst. 7 (1) (1985)
Robert L. Constable, N. P. Mendler
Recursive Definitions in Type Theory. Logic of Programs (1985)
Robert L. Constable, Todd B. Knoblock, Joseph L. Bates
Writing Programs that Construct Proofs. J. Autom. Reason. 1 (3) (1985)
Robert L. Constable, Daniel R. Zlatin
The Type Theory of PL/CV3. ACM Trans. Program. Lang. Syst. 6 (1) (1984)
Robert L. Constable
Partial functions in constructive formal theories. Theoretical Computer Science (1983)
Robert L. Constable
Programs as Proofs: A Synopsis. Inf. Process. Lett. 16 (3) (1983)
Robert L. Constable
Mathematics as Programming. Logic of Programs (1983)
Robert L. Constable
Constructive Mathematics as a Programming Logic I: Some Principles of Theory. FCT (1983)
Robert L. Constable
VERking in constructive set theory. ACM SIGSOFT Softw. Eng. Notes 6 (3) (1981)
Robert L. Constable, Daniel R. Zlatin
The Type Theory of PL/CV 3. Logic of Programs (1981)
Harry B. Hunt III, Robert L. Constable, Sartaj Sahni
On the Computational Complexity of Program Scheme Equivalence. SIAM J. Comput. 9 (2) (1980)
Robert L. Constable
Programs and Types FOCS (1980)
Robert L. Constable, Scott Johnson
A PL/CV Precis. POPL (1979)
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) (1979)
Robert L. Constable
A Constructive Programming Logic. IFIP Congress (1977)
Robert L. Constable
On the Theory of Programming Logics STOC (1977)
Herbert Egli, Robert L. Constable
Computability Concepts for Programming Language Semantics. Theor. Comput. Sci. 2 (2) (1976)
Herbert Egli, Robert L. Constable
Computability Concepts for Programming Language Semantics STOC (1975)
Robert L. Constable, David Park
Special issue on semantics and program schemas SIAM journal on computing. SIGACT News 6 (4) (1974)
Robert L. Constable
Type Two Computational Complexity STOC (1973)
Robert L. Constable
The Operator Gap. J. ACM 19 (1) (1972)
Robert L. Constable, David Gries
On Classes of Program Schemata. SIAM J. Comput. 1 (1) (1972)
John C. Cherniavsky, Robert L. Constable
Representing Program Schemes in Logic SWAT (1972)
Robert L. Constable, Steven S. Muchnick
Subrecursive Program Schemata I & II: I. Undecidable Equivalence Problems; II. Decidable Equivalence Problems STOC (1972)
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) (1972)
Robert L. Constable, Allan Borodin
Subrecursive Programming Languages, Part I: efficiency and program structure. J. ACM 19 (3) (1972)
Robert L. Constable
Loop Schemata STOC (1971)
Robert L. Constable
Subrecursive Programming Languages. II. On Program Size. J. Comput. Syst. Sci. 5 (3) (1971)
Robert L. Constable
Constructive Mathematics and Automatic Program Writers. IFIP Congress (1) (1971)
Robert L. Constable, David Gries
On Classes of Program Schemata SWAT (1971)
Robert L. Constable, Juris Hartmanis
Complexity of Formal Translations and Speed-Up Results STOC (1971)
Robert L. Constable, Allan Borodin
On the Efficiency of Programs in Subrecursive Formalisms (Incomplete Version, Extended Abstract) SWAT (1970)
Robert L. Constable
On the Size of Programs in Subrecursive Formalisms STOC (1970)
Robert L. Constable
The Operator Gap SWAT (1969)
Allan Borodin, Robert L. Constable, John E. Hopcroft
Dense and Non-Dense Families of Complexity Classes SWAT (1969)