Robert L. Constable

According to our database, Robert L. Constable authored at least 78 papers between 1969 and 2021.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2021

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle.

Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

2019

Intuitionistic ancestral logic.

Liron Cohen, Robert L. Constable

J. Log. Comput., 2019

Bar Induction is Compatible with Constructive Type Theory.

Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable

J. ACM, 2019

Implementing Euclid's straightedge and compass constructions in type theory.

Ariel Kellison, Mark Bickford, Robert L. Constable

Ann. Math. Artif. Intell., 2019

2018

Computability Beyond Church-Turing via Choice Sequences.

Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems.

Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

Sci. Comput. Program., 2017

Bar induction: The good, the bad, and the ugly.

Vincent Rahli, Mark Bickford, Robert L. Constable

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

2015

Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML.

Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

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

Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language.

Liron Cohen, Robert L. Constable

Proceedings of the Logic, Language, Information, and Computation, 2015

2014

Virtual Evidence: A Constructive Semantics for Classical Logics.

Robert L. Constable

CoRR, 2014

Intuitionistic completeness of first-order logic.

Robert L. Constable, Mark Bickford

Ann. Pure Appl. Log., 2014

Developing Correctly Replicated Databases Using Formal Tools.

Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

Proceedings of the 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2014

2012

Russell's Orders in Kripke's Theory of Truth and Computational Type Theory.

Fairouz Kamareddine, Twan Laan, Robert L. Constable

Proceedings of the Sets and Extensions in the Twentieth Century, 2012

Proof Assistants and the Dynamic Nature of Formal Theories.

Robert L. Constable

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer.

Robert L. Constable

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

A diversified and correct-by-construction broadcast service.

Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable

Proceedings of the 20th IEEE International Conference on Network Protocols, 2012

ShadowDB: A Replicated Database on a Synthesized Consensus Core.

Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

Proceedings of the Eighth Workshop on Hot Topics in System Dependability, HotDep 2012, 2012

2011

Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP

Robert L. Constable

CoRR, 2011

Knowledge-Based Synthesis of Distributed Systems Using Event Structures

Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

Log. Methods Comput. Sci., 2011

2009

Computational type theory.

Robert L. Constable

Scholarpedia, 2009

Extracting the resolution algorithm from a completeness proof for the propositional calculus.

Robert L. Constable, Wojciech Moczydlowski

Ann. Pure Appl. Log., 2009

Building Mathematics-Based Software Systems to Advance Science and Create Knowledge.

Robert L. Constable

Proceedings of the Efficient Algorithms, 2009

2008

Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics.

Robert L. Constable, Wojciech Moczydlowski

Log. Methods Comput. Sci., 2008

2006

Innovations in computational type theory using Nuprl.

Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, E. Moran

J. Appl. Log., 2006

2004

A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.

Lori Lorigo, Jon M. Kleinberg, Richard Eaton, Robert L. Constable

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

2003

MetaPRL - A Modular Logical Environment.

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

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

2001

Protocol Switching: Exploiting Meta-Properties.

Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable

Proceedings of the 21st International Conference on Distributed Computing Systems Workshops (ICDCS 2001 Workshops), 2001

2000

The Nuprl Open Logical Environment.

Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

Proceedings of the Automated Deduction, 2000

Constructively formalizing automata theory.

Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan C. Uribe

Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1999

Metalogical Frameworks II: Developing a Reflected Decision Procedure.

William E. Aitken, Robert L. Constable, Judith L. Underwood

J. Autom. Reason., 1999

Building reliable, high-performance communication systems from components.

Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth P. Birman, Robert L. Constable

Proceedings of the 17th ACM Symposium on Operating System Principles, 1999

Verbalization of High-Level Formal Proofs.

Amanda M. Holland-Minkley, Regina Barzilay, Robert L. Constable

Proceedings of the Sixteenth National Conference on Artificial Intelligence and Eleventh Conference on Innovative Applications of Artificial Intelligence, 1999

1998

A Note on Complexity Measures for Inductive Classes in Constructive Type Theory.

Robert L. Constable

Inf. Comput., 1998

1997

ML Programming in Constructive Type Theory (abstract).

Robert L. Constable

Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997

1995

Single change neighbor designs.

Robert L. Constable, Donald A. Preece, Nicholas C. K. Phillips, Thomas Dale Porter, Walter D. Wallis

Australas. J Comb., 1995

Experience with Type Theory as a Foundation for Computer Science

Robert L. Constable

Proceedings of the Proceedings, 1995

1994

Expressing Computational Complexity in Constructive Type Theory.

Robert L. Constable

Proceedings of the Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, 1994

Exporting and Refecting Abstract Metamathematics.

Robert L. Constable

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

Computational Foundations of Basic Recursive Function Theory.

Robert L. Constable, Scott F. Smith

Theor. Comput. Sci., 1993

1992

Formal Theories and Software Systems: Fundamental Connections between Computer Science and Logic.

Robert L. Constable

Proceedings of the Future Tendencies in Computer Science, 1992

1991

Type Theory as a Foundation for Computer Science.

Robert L. Constable

Proceedings of the Theoretical Aspects of Computer Software, 1991

1990

The Semantics of Reflected Proof

Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William E. Aitken

Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

1987

Partial Objects In Constructive Type Theory

Robert L. Constable, Scott F. Smith

Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

1986

Infinite Objects in Type Theory

Nax Paul Mendler, Prakash Panangaden, Robert L. Constable

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Formalized Metareasoning in Type Theory

Todd B. Knoblock, Robert L. Constable

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Implementing mathematics with the Nuprl proof development system.

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

Prentice Hall, ISBN: 978-0-13-451832-9, 1986

1985

Proofs as Programs.

Joseph L. Bates, Robert L. Constable

ACM Trans. Program. Lang. Syst., 1985

Writing Programs that Construct Proofs.

Robert L. Constable, Todd B. Knoblock, Joseph L. Bates

J. Autom. Reason., 1985

Recursive Definitions in Type Theory.

Robert L. Constable, Nax Paul Mendler

Proceedings of the Logics of Programs, 1985

1984

The Type Theory of PL/CV3.

Robert L. Constable, Daniel R. Zlatin

ACM Trans. Program. Lang. Syst., 1984

1983

Programs as Proofs: A Synopsis.

Robert L. Constable

Inf. Process. Lett., 1983

Partial functions in constructive formal theories.

Robert L. Constable

Proceedings of the Theoretical Computer Science, 1983

Mathematics as Programming.

Robert L. Constable

Proceedings of the Logics of Programs, 1983

Constructive Mathematics as a Programming Logic I: Some Principles of Theory.

Robert L. Constable

Proceedings of the Fundamentals of Computation Theory, 1983

1982

An Introduction to the PL/CV2 Programming Logic

Robert L. Constable, Scott Johnson, C. D. Eichenlaub

Lecture Notes in Computer Science 135, Springer, ISBN: 3-540-11492-0, 1982

1981

VERking in constructive set theory.

Robert L. Constable

ACM SIGSOFT Softw. Eng. Notes, 1981

The Type Theory of PL/CV 3.

Robert L. Constable, Daniel R. Zlatin

Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, 1981

1980

On the Computational Complexity of Program Scheme Equivalence.

Harry B. Hunt III, Robert L. Constable, Sartaj Sahni

SIAM J. Comput., 1980

Programs and Types

Robert L. Constable

Proceedings of the 21st Annual Symposium on Foundations of Computer Science, 1980

1979

A Hierarchial Approach to Formal Semantics With Application to the Definition of PL/CS.

Robert L. Constable, James E. Donahue

ACM Trans. Program. Lang. Syst., 1979

A PL/CV Precis.

Robert L. Constable, Scott Johnson

Proceedings of the Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, 1979

1977

On the Theory of Programming Logics

Robert L. Constable

Proceedings of the 9th Annual ACM Symposium on Theory of Computing, 1977

A Constructive Programming Logic.

Robert L. Constable

Proceedings of the Information Processing, 1977

1976

Computability Concepts for Programming Language Semantics.

Herbert Egli, Robert L. Constable

Theor. Comput. Sci., 1976

1974

Special issue on semantics and program schemas SIAM journal on computing.

Robert L. Constable, David Park

SIGACT News, 1974

1973

Type Two Computational Complexity

Robert L. Constable

Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30, 1973

1972

On Classes of Program Schemata.

Robert L. Constable, David Gries

SIAM J. Comput., 1972

Subrecursive Program Schemata I & II: I. Undecidable Equivalence problems; II. Decidable Equivalence Problems.

Robert L. Constable, Steven S. Muchnick

J. Comput. Syst. Sci., 1972

Subrecursive Programming Languages, Part I: efficiency and program structure.

Robert L. Constable, Allan Borodin

J. ACM, 1972

The Operator Gap.

Robert L. Constable

J. ACM, 1972

Representing Program Schemes in Logic

John C. Cherniavsky, Robert L. Constable

Proceedings of the 13th Annual Symposium on Switching and Automata Theory, 1972

1971

Subrecursive Programming Languages. II. On Program Size.

Robert L. Constable

J. Comput. Syst. Sci., 1971

Complexity of Formal Translations and Speed-Up Results

Robert L. Constable, Juris Hartmanis

Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 1971

Loop Schemata

Robert L. Constable

Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 1971

Constructive Mathematics and Automatic Program Writers.

Robert L. Constable

Proceedings of the Information Processing, Proceedings of IFIP Congress 1971, Volume 1, 1971

1970

On the Size of Programs in Subrecursive Formalisms

Robert L. Constable

Proceedings of the 2nd Annual ACM Symposium on Theory of Computing, 1970

On the Efficiency of Programs in Subrecursive Formalisms (Incomplete Version, Extended Abstract)

Robert L. Constable, Allan Borodin

Proceedings of the 11th Annual Symposium on Switching and Automata Theory, 1970

1969

Dense and Non-Dense Families of Complexity Classes

Allan Borodin, Robert L. Constable, John E. Hopcroft

Proceedings of the 10th Annual Symposium on Switching and Automata Theory, 1969