Robert L. Constable

According to our database1, Robert L. Constable authored at least 82 papers between 1969 and 2018.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 1995, "For fundamental contributions to the field of logic and its computational aspects, especially his work on providing mechanical assistance in problem solving through the software system Nuprl.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2018
Computability Beyond Church-Turing via Choice Sequences.
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.
Sci. Comput. Program., 2017

Bar induction: The good, the bad, and the ugly.
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.
ECEASST, 2015

Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language.
Proceedings of the Logic, Language, Information, and Computation, 2015

2014
Virtual Evidence: A Constructive Semantics for Classical Logics.
CoRR, 2014

Intuitionistic completeness of first-order logic.
Ann. Pure Appl. Logic, 2014

Developing Correctly Replicated Databases Using Formal Tools.
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.
Proceedings of the Sets and Extensions in the Twentieth Century, 2012

On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

A diversified and correct-by-construction broadcast service.
Proceedings of the 20th IEEE International Conference on Network Protocols, 2012

ShadowDB: A Replicated Database on a Synthesized Consensus Core.
Proceedings of the Eighth Workshop on Hot Topics in System Dependability, HotDep 2012, 2012

Proof Assistants and the Dynamic Nature of Formal Theories.
Proceedings of the ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation, 2012

2011
Intuitionistic Completeness of First-Order Logic
CoRR, 2011

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

Knowledge-Based Synthesis of Distributed Systems Using Event Structures
Logical Methods in Computer Science, 2011

2009
Computational type theory.
Scholarpedia, 2009

Extracting the resolution algorithm from a completeness proof for the propositional calculus.
Ann. Pure Appl. Logic, 2009

Building Mathematics-Based Software Systems to Advance Science and Create Knowledge.
Proceedings of the Efficient Algorithms, 2009

2008
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics.
Logical Methods in Computer Science, 2008

Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
CoRR, 2008

2007
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007

2006
Innovations in computational type theory using Nuprl.
J. Applied Logic, 2006

Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2004
A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.
Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

Knowledge-Based Synthesis of Distributed Systems Using Event Structures.
Proceedings of the Logic for Programming, 2004

2003
MetaPRL - A Modular Logical Environment.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

2001
Protocol Switching: Exploiting Meta-Properties.
ICDCS Workshops, 2001

2000
The Nuprl Open Logical Environment.
Proceedings of the Automated Deduction, 2000

Constructively formalizing automata theory.
Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1999
Metalogical Frameworks II: Developing a Reflected Decision Procedure.
J. Autom. Reasoning, 1999

Building reliable, high-performance communication systems from components.
Proceedings of the 17th ACM Symposium on Operating System Principles, 1999

Verbalization of High-Level Formal Proofs.
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.
Inf. Comput., 1998

1997
ML Programming in Constructive Type Theory (abstract).
Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997

1995
Single change neighbor designs.
Australasian J. Combinatorics, 1995

Experience with Type Theory as a Foundation for Computer Science
Proceedings of the Proceedings, 1995

1994
Expressing Computational Complexity in Constructive Type Theory.
Proceedings of the Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, 1994

Exporting and Refecting Abstract Metamathematics.
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.
Theor. Comput. Sci., 1993

1992
Formal Theories and Software Systems: Fundamental Connections between Computer Science and Logic.
Proceedings of the Future Tendencies in Computer Science, 1992

1991
Type Theory as a Foundation for Computer Science.
Proceedings of the Theoretical Aspects of Computer Software, 1991

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

1988
Computational Foundations of Basic Recursive Function Theory
Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

1987
Partial Objects In Constructive Type Theory
Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987

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

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

Implementing mathematics with the Nuprl proof development system.
Prentice Hall, ISBN: 978-0-13-451832-9, 1986

1985
Proofs as Programs.
ACM Trans. Program. Lang. Syst., 1985

Writing Programs that Construct Proofs.
J. Autom. Reasoning, 1985

Recursive Definitions in Type Theory.
Proceedings of the Logics of Programs, 1985

1984
The Type Theory of PL/CV3.
ACM Trans. Program. Lang. Syst., 1984

1983
Programs as Proofs: A Synopsis.
Inf. Process. Lett., 1983

Partial functions in constructive formal theories.
Proceedings of the Theoretical Computer Science, 1983

Mathematics as Programming.
Proceedings of the Logics of Programs, 1983

Constructive Mathematics as a Programming Logic I: Some Principles of Theory.
Proceedings of the Fundamentals of Computation Theory, 1983

1982
An Introduction to the PL/CV2 Programming Logic
Lecture Notes in Computer Science 135, Springer, ISBN: 3-540-11492-0, 1982

1981
The Type Theory of PL/CV 3.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, 1981

1980
On the Computational Complexity of Program Scheme Equivalence.
SIAM J. Comput., 1980

Programs and Types
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.
ACM Trans. Program. Lang. Syst., 1979

A PL/CV Precis.
Proceedings of the Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, 1979

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

A Constructive Programming Logic.
IFIP Congress, 1977

1976
Computability Concepts for Programming Language Semantics.
Theor. Comput. Sci., 1976

1975
Computability Concepts for Programming Language Semantics
Proceedings of the 7th Annual ACM Symposium on Theory of Computing, 1975

1973
Type Two Computational Complexity
Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30, 1973

1972
On Classes of Program Schemata.
SIAM J. Comput., 1972

Subrecursive Program Schemata I & II: I. Undecidable Equivalence problems; II. Decidable Equivalence Problems.
J. Comput. Syst. Sci., 1972

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

The Operator Gap.
J. ACM, 1972

Subrecursive Program Schemata I & II: I. Undecidable Equivalence Problems; II. Decidable Equivalence Problems
Proceedings of the 4th Annual ACM Symposium on Theory of Computing, 1972

Representing Program Schemes in Logic
Proceedings of the 13th Annual Symposium on Switching and Automata Theory, 1972

1971
Subrecursive Programming Languages. II. On Program Size.
J. Comput. Syst. Sci., 1971

Complexity of Formal Translations and Speed-Up Results
Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 1971

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

Constructive Mathematics and Automatic Program Writers.
IFIP Congress (1), 1971

On Classes of Program Schemata
Proceedings of the 12th Annual Symposium on Switching and Automata Theory, 1971

1970
On the Size of Programs in Subrecursive Formalisms
Proceedings of the 2nd Annual ACM Symposium on Theory of Computing, 1970

On the Efficiency of Programs in Subrecursive Formalisms (Incomplete Version, Extended Abstract)
Proceedings of the 11th Annual Symposium on Switching and Automata Theory, 1970

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

Dense and Non-Dense Families of Complexity Classes
Proceedings of the 10th Annual Symposium on Switching and Automata Theory, 1969


  Loading...