Robert L. Constable
According to our database^{1},
Robert L. Constable
authored at least 76 papers
between 1969 and 2018.
Collaborative distances:
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 OtherLinks
Homepages:

at id.loc.gov

at isni.org

at dl.acm.org
On csauthors.net:
Bibliography
2018
Computability Beyond ChurchTuring via Choice Sequences.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018
2017
EventML: Specification, verification, and implementation of crashtolerant 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 FaultTolerant 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
Intuitionistic completeness of firstorder 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 correctbyconstruction 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
KnowledgeBased Synthesis of Distributed Systems Using Event Structures
Logical Methods in Computer Science, 2011
2009
Computational type theory.
Scholarpedia, 2009
Building MathematicsBased Software Systems to Advance Science and Create Knowledge.
Proceedings of the Efficient Algorithms, 2009
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 SetTheoretic Semantics.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006
2004
A GraphBased Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.
Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004
KnowledgeBased 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 MetaProperties.
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, highperformance communication systems from components.
Proceedings of the 17th ACM Symposium on Operating System Principles, 1999
Verbalization of HighLevel 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  CADE12, 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: 9780134518329, 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: 3540114920, 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 SpeedUp 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 NonDense Families of Complexity Classes
Proceedings of the 10th Annual Symposium on Switching and Automata Theory, 1969