Dense and Non-Dense Families of Complexity Classes - Allan Borodin; Robert L. Constable; John E. Hopcroft (SWAT, 1969)

On the Efficiency of Programs in Subrecursive Formalisms (Incomplete Version, Extended Abstract) - Robert L. Constable; Allan Borodin (SWAT, 1970)

On the Size of Programs in Subrecursive Formalisms - Robert L. Constable (STOC, 1970)

Constructive Mathematics and Automatic Program Writers. - Robert L. Constable (IFIP Congress (1), 1971)

Loop Schemata - Robert L. Constable (STOC, 1971)

Complexity of Formal Translations and Speed-Up Results - Robert L. Constable; Juris Hartmanis (STOC, 1971)

Subrecursive Programming Languages. II. On Program Size. - Robert L. Constable (J. Comput. Syst. Sci., 1971)

Representing Program Schemes in Logic - John C. Cherniavsky; Robert L. Constable (SWAT, 1972)

The Operator Gap. - Robert L. Constable (J. ACM, 1972)

Subrecursive Programming Languages, Part I: efficiency and program structure. - Robert L. Constable; Allan Borodin (J. ACM, 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)

On Classes of Program Schemata. - Robert L. Constable; David Gries (SIAM J. Comput., 1972)

Type Two Computational Complexity - Robert L. Constable (STOC, 1973)

Special issue on semantics and program schemas SIAM journal on computing. - Robert L. Constable; David Park (SIGACT News, 1974)

Computability Concepts for Programming Language Semantics. - Herbert Egli; Robert L. Constable (Theor. Comput. Sci., 1976)

A Constructive Programming Logic. - Robert L. Constable (IFIP Congress, 1977)

On the Theory of Programming Logics - Robert L. Constable (STOC, 1977)

A PL/CV Precis. - Robert L. Constable; Scott Johnson (POPL, 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)

Programs and Types - Robert L. Constable (FOCS, 1980)

On the Computational Complexity of Program Scheme Equivalence. - Harry B. Hunt III; Robert L. Constable; Sartaj Sahni (SIAM J. Comput., 1980)

The Type Theory of PL/CV 3. - Robert L. Constable; Daniel R. Zlatin (Logic of Programs, 1981)

VERking in constructive set theory. - Robert L. Constable (ACM SIGSOFT Softw. Eng. Notes, 1981)

An Introduction to the PL/CV2 Programming Logic - Robert L. Constable; Scott Johnson; C. D. Eichenlaub (Springer, 1982)

Constructive Mathematics as a Programming Logic I: Some Principles of Theory. - Robert L. Constable (FCT, 1983)

Mathematics as Programming. - Robert L. Constable (Logic of Programs, 1983)

Partial functions in constructive formal theories. - Robert L. Constable (Theoretical Computer Science, 1983)

Programs as Proofs: A Synopsis. - Robert L. Constable (Inf. Process. Lett., 1983)

The Type Theory of PL/CV3. - Robert L. Constable; Daniel R. Zlatin (ACM Trans. Program. Lang. Syst., 1984)

Recursive Definitions in Type Theory. - Robert L. Constable; Nax Paul Mendler (Logic of Programs, 1985)

Writing Programs that Construct Proofs. - Robert L. Constable; Todd B. Knoblock; Joseph L. Bates (J. Autom. Reason., 1985)

Proofs as Programs. - Joseph L. Bates; Robert L. Constable (ACM Trans. Program. Lang. Syst., 1985)

Implementing mathematics with the Nuprl proof development system. - Robert L. Constable; Stuart F. Allen; Mark Bromley; Rance Cleaveland; J. F. Cremer; Robert Harper 001; Douglas J. Howe; Todd B. Knoblock; Nax Paul Mendler; Prakash Panangaden; James T. Sasaki; Scott F. Smith 001 (Prentice Hall, 1986)

Formalized Metareasoning in Type Theory - Todd B. Knoblock; Robert L. Constable (LICS, 1986)

Infinite Objects in Type Theory - Nax Paul Mendler; Prakash Panangaden; Robert L. Constable (LICS, 1986)

Partial Objects In Constructive Type Theory - Robert L. Constable; Scott F. Smith 001 (LICS, 1987)

The Semantics of Reflected Proof - Stuart F. Allen; Robert L. Constable; Douglas J. Howe; William E. Aitken (LICS, 1990)

Type Theory as a Foundation for Computer Science. - Robert L. Constable (TACS, 1991)

Formal Theories and Software Systems: Fundamental Connections between Computer Science and Logic. - Robert L. Constable (25th Anniversary of INRIA, 1992)

Computational Foundations of Basic Recursive Function Theory. - Robert L. Constable; Scott F. Smith 001 (Theor. Comput. Sci., 1993)

Exporting and Refecting Abstract Metamathematics. - Robert L. Constable (CADE, 1994)

Expressing Computational Complexity in Constructive Type Theory. - Robert L. Constable (LCC, 1994)

Experience with Type Theory as a Foundation for Computer Science - Robert L. Constable (LICS, 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)

ML Programming in Constructive Type Theory (abstract). - Robert L. Constable (TPHOLs, 1997)

A Note on Complexity Measures for Inductive Classes in Constructive Type Theory. - Robert L. Constable (Inf. Comput., 1998)

Verbalization of High-Level Formal Proofs. - Amanda M. Holland-Minkley; Regina Barzilay; Robert L. Constable (AAAI/IAAI, 1999)

Building reliable, high-performance communication systems from components. - Xiaoming Liu 003; Christoph Kreitz; Robbert van Renesse; Jason Hickey; Mark Hayden; Kenneth P. Birman; Robert L. Constable (SOSP, 1999)

Metalogical Frameworks II: Developing a Reflected Decision Procedure. - William E. Aitken; Robert L. Constable; Judith L. Underwood (J. Autom. Reason., 1999)

Constructively formalizing automata theory. - Robert L. Constable; Paul B. Jackson; Pavel Naumov; Juan C. Uribe (Proof, Language, and Interaction, 2000)

The Nuprl Open Logical Environment. - Stuart F. Allen; Robert L. Constable; Richard Eaton; Christoph Kreitz; Lori Lorigo (CADE, 2000)

Protocol Switching: Exploiting Meta-Properties. - Xiaoming Liu 003; Robbert van Renesse; Mark Bickford; Christoph Kreitz; Robert L. Constable (ICDCS Workshops, 2001)

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; et al. (TPHOLs, 2003)

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 (MKM, 2004)

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)

Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. - Robert L. Constable; Wojciech Moczydlowski (Log. Methods Comput. Sci., 2008)

Building Mathematics-Based Software Systems to Advance Science and Create Knowledge. - Robert L. Constable (Efficient Algorithms, 2009)

Extracting the resolution algorithm from a completeness proof for the propositional calculus. - Robert L. Constable; Wojciech Moczydlowski (Ann. Pure Appl. Log., 2009)

Computational type theory. - Robert L. Constable (Scholarpedia, 2009)

Knowledge-Based Synthesis of Distributed Systems Using Event Structures - Mark Bickford; Robert L. Constable; Joseph Y. Halpern; Sabina Petride (Log. Methods Comput. Sci., 2011)

Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP - Robert L. Constable (CoRR, 2011)

ShadowDB: A Replicated Database on a Synthesized Consensus Core. - Nicolas Schiper; Vincent Rahli; Robbert van Renesse; Mark Bickford; Robert L. Constable (HotDep, 2012)

A diversified and correct-by-construction broadcast service. - Vincent Rahli; Nicolas Schiper; Robbert van Renesse; Mark Bickford; Robert L. Constable (ICNP, 2012)

On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer. - Robert L. Constable (LICS, 2012)

Proof Assistants and the Dynamic Nature of Formal Theories. - Robert L. Constable (PxTP, 2012)

Russell's Orders in Kripke's Theory of Truth and Computational Type Theory. - Fairouz Kamareddine; Twan Laan; Robert L. Constable (Sets and Extensions in the Twentieth Century, 2012)

Developing Correctly Replicated Databases Using Formal Tools. - Nicolas Schiper; Vincent Rahli; Robbert van Renesse; Mark Bickford; Robert L. Constable (DSN, 2014)

Intuitionistic completeness of first-order logic. - Robert L. Constable; Mark Bickford (Ann. Pure Appl. Log., 2014)

Virtual Evidence: A Constructive Semantics for Classical Logics. - Robert L. Constable (CoRR, 2014)

Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language. - Liron Cohen 001; Robert L. Constable (WoLLIC, 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)

Bar induction: The good, the bad, and the ugly. - Vincent Rahli; Mark Bickford; Robert L. Constable (LICS, 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)

Computability Beyond Church-Turing via Choice Sequences. - Mark Bickford; Liron Cohen 001; Robert L. Constable; Vincent Rahli (LICS, 2018)

Implementing Euclid's straightedge and compass constructions in type theory. - Ariel Kellison; Mark Bickford; Robert L. Constable (Ann. Math. Artif. Intell., 2019)

Bar Induction is Compatible with Constructive Type Theory. - Vincent Rahli; Mark Bickford; Liron Cohen 001; Robert L. Constable (J. ACM, 2019)

Intuitionistic ancestral logic. - Liron Cohen 001; Robert L. Constable (J. Log. Comput., 2019)

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. - Mark Bickford; Liron Cohen 001; Robert L. Constable; Vincent Rahli (CSL, 2021)