Robert L. Constable

92 papers A* 21A 4B 4C 1Misc 1Journal 33Unranked 24

Year	Rank	Type	Title / Venue / Authors
2021	B	`conf`	Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. CSL Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
2019	J	`jnl`	Bar Induction is Compatible with Constructive Type Theory. J. ACM Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable
2019	J	`jnl`	Implementing Euclid's straightedge and compass constructions in type theory. Ann. Math. Artif. Intell. Ariel Kellison, Mark Bickford, Robert L. Constable
2019	J	`jnl`	Intuitionistic ancestral logic. J. Log. Comput. Liron Cohen, Robert L. Constable
2018	A*	`conf`	Computability Beyond Church-Turing via Choice Sequences. LICS Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
2017	A*	`conf`	Bar induction: The good, the bad, and the ugly. LICS Vincent Rahli, Mark Bickford, Robert L. Constable
2017	J	`jnl`	EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
2015	J	`jnl`	Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
2015	C	`conf`	Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language. WoLLIC Liron Cohen, Robert L. Constable
2014	A	`conf`	Developing Correctly Replicated Databases Using Formal Tools. DSN Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
2014	J	`jnl`	Intuitionistic completeness of first-order logic. Ann. Pure Appl. Log. Robert L. Constable, Mark Bickford
2014	J	`jnl`	Virtual Evidence: A Constructive Semantics for Classical Logics. CoRR Robert L. Constable
2012	B	`conf`	A diversified and correct-by-construction broadcast service. ICNP Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable
2012	—	`ed.`	Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday Logic and Program Semantics Robert L. Constable, Alexandra Silva
2012	A*	`conf`	On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer. LICS Robert L. Constable
2012	—	`conf`	Proof Assistants and the Dynamic Nature of Formal Theories. ATx/WInG@IJCAR Robert L. Constable
2012	—	`conf`	Proof Assistants and the Dynamic Nature of Formal Theories. PxTP Robert L. Constable
2012	—	`ch.`	Russell's Orders in Kripke's Theory of Truth and Computational Type Theory. Sets and Extensions in the Twentieth Century Fairouz Kamareddine, Twan Laan, Robert L. Constable
2012	—	`conf`	ShadowDB: A Replicated Database on a Synthesized Consensus Core. HotDep Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
2011	J	`jnl`	Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP CoRR Robert L. Constable
2011	J	`jnl`	Intuitionistic Completeness of First-Order Logic CoRR Robert L. Constable, Mark Bickford
2011	J	`jnl`	Knowledge-Based Synthesis of Distributed Systems Using Event Structures Log. Methods Comput. Sci. Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2009	—	`conf`	Building Mathematics-Based Software Systems to Advance Science and Create Knowledge. Efficient Algorithms Robert L. Constable
2009	J	`jnl`	Computational type theory. Scholarpedia Robert L. Constable
2009	J	`jnl`	Extracting the resolution algorithm from a completeness proof for the propositional calculus. Ann. Pure Appl. Log. Robert L. Constable, Wojciech Moczydlowski
2008	J	`jnl`	Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics CoRR Robert L. Constable, Wojciech Moczydlowski
2008	J	`jnl`	Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. Log. Methods Comput. Sci. Robert L. Constable, Wojciech Moczydlowski
2007	Misc	`conf`	Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus. LFCS Robert L. Constable, Wojciech Moczydlowski
2006	A	`conf`	Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics. IJCAR Robert L. Constable, Wojciech Moczydlowski
2006	J	`jnl`	Innovations in computational type theory using Nuprl. J. Appl. Log. Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, E. Moran
2004	—	`conf`	A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. MKM Lori Lorigo, Jon M. Kleinberg, Richard Eaton, Robert L. Constable
2004	B	`conf`	Knowledge-Based Synthesis of Distributed Systems Using Event Structures. LPAR Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2003	—	`conf`	MetaPRL - A Modular Logical Environment. TPHOLs 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
2001	—	`conf`	Protocol Switching: Exploiting Meta-Properties. ICDCS Workshops Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2000	—	`conf`	Constructively formalizing automata theory. Proof, Language, and Interaction Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan C. Uribe
2000	A	`conf`	The Nuprl Open Logical Environment. CADE Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
1999	A*	`conf`	Building reliable, high-performance communication systems from components. SOSP Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth P. Birman, Robert L. Constable
1999	J	`jnl`	Metalogical Frameworks II: Developing a Reflected Decision Procedure. J. Autom. Reason. William E. Aitken, Robert L. Constable, Judith L. Underwood
1999	—	`conf`	Verbalization of High-Level Formal Proofs. AAAI/IAAI Amanda M. Holland-Minkley, Regina Barzilay, Robert L. Constable
1998	J	`jnl`	A Note on Complexity Measures for Inductive Classes in Constructive Type Theory. Inf. Comput. Robert L. Constable
1997	—	`conf`	ML Programming in Constructive Type Theory (abstract). TPHOLs Robert L. Constable
1995	A*	`conf`	Experience with Type Theory as a Foundation for Computer Science LICS Robert L. Constable
1995	J	`jnl`	Single change neighbor designs. Australas. J Comb. Robert L. Constable, Donald A. Preece, Nicholas C. K. Phillips, Thomas Dale Porter, Walter D. Wallis
1994	A	`conf`	Exporting and Refecting Abstract Metamathematics. CADE Robert L. Constable
1994	—	`conf`	Expressing Computational Complexity in Constructive Type Theory. LCC Robert L. Constable
1993	J	`jnl`	Computational Foundations of Basic Recursive Function Theory. Theor. Comput. Sci. Robert L. Constable, Scott F. Smith
1992	—	`conf`	Formal Theories and Software Systems: Fundamental Connections between Computer Science and Logic. 25th Anniversary of INRIA Robert L. Constable
1991	—	`conf`	Type Theory as a Foundation for Computer Science. TACS Robert L. Constable
1990	A*	`conf`	The Semantics of Reflected Proof LICS Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William E. Aitken
1988	A*	`conf`	Computational Foundations of Basic Recursive Function Theory LICS Robert L. Constable, Scott F. Smith
1987	A*	`conf`	Partial Objects In Constructive Type Theory LICS Robert L. Constable, Scott F. Smith
1986	A*	`conf`	Formalized Metareasoning in Type Theory LICS Todd B. Knoblock, Robert L. Constable
1986	—	`book`	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
1986	A*	`conf`	Infinite Objects in Type Theory LICS Nax Paul Mendler, Prakash Panangaden, Robert L. Constable
1985	J	`jnl`	Proofs as Programs. ACM Trans. Program. Lang. Syst. Joseph L. Bates, Robert L. Constable
1985	—	`conf`	Recursive Definitions in Type Theory. Logic of Programs Robert L. Constable, Nax Paul Mendler
1985	J	`jnl`	Writing Programs that Construct Proofs. J. Autom. Reason. Robert L. Constable, Todd B. Knoblock, Joseph L. Bates
1984	J	`jnl`	The Type Theory of PL/CV3. ACM Trans. Program. Lang. Syst. Robert L. Constable, Daniel R. Zlatin
1983	B	`conf`	Constructive Mathematics as a Programming Logic I: Some Principles of Theory. FCT Robert L. Constable
1983	—	`conf`	Mathematics as Programming. Logic of Programs Robert L. Constable
1983	—	`conf`	Partial functions in constructive formal theories. Theoretical Computer Science Robert L. Constable
1983	J	`jnl`	Programs as Proofs: A Synopsis. Inf. Process. Lett. Robert L. Constable
1982	—	`book`	An Introduction to the PL/CV2 Programming Logic Robert L. Constable, Scott Johnson, C. D. Eichenlaub
1981	—	`conf`	The Type Theory of PL/CV 3. Logic of Programs Robert L. Constable, Daniel R. Zlatin
1981	J	`jnl`	VERking in constructive set theory. ACM SIGSOFT Softw. Eng. Notes Robert L. Constable
1980	J	`jnl`	On the Computational Complexity of Program Scheme Equivalence. SIAM J. Comput. Harry B. Hunt III, Robert L. Constable, Sartaj Sahni
1980	A*	`conf`	Programs and Types FOCS Robert L. Constable
1979	J	`jnl`	A Hierarchial Approach to Formal Semantics With Application to the Definition of PL/CS. ACM Trans. Program. Lang. Syst. Robert L. Constable, James E. Donahue
1979	A*	`conf`	A PL/CV Precis. POPL Robert L. Constable, Scott Johnson
1977	—	`conf`	A Constructive Programming Logic. IFIP Congress Robert L. Constable
1977	A*	`conf`	On the Theory of Programming Logics STOC Robert L. Constable
1976	J	`jnl`	Computability Concepts for Programming Language Semantics. Theor. Comput. Sci. Herbert Egli, Robert L. Constable
1975	A*	`conf`	Computability Concepts for Programming Language Semantics STOC Herbert Egli, Robert L. Constable
1974	A*	`ed.`	Proceedings of the 6th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1974, Seattle, Washington, USA STOC Robert L. Constable, Robert W. Ritchie, Jack W. Carlyle, Michael A. Harrison
1974	J	`jnl`	Special issue on semantics and program schemas SIAM journal on computing. SIGACT News Robert L. Constable, David Park
1973	A*	`ed.`	Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA STOC Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, H. Raymond Strong
1973	A*	`conf`	Type Two Computational Complexity STOC Robert L. Constable
1972	J	`jnl`	On Classes of Program Schemata. SIAM J. Comput. Robert L. Constable, David Gries
1972	—	`conf`	Representing Program Schemes in Logic SWAT John C. Cherniavsky, Robert L. Constable
1972	A*	`conf`	Subrecursive Program Schemata I & II: I. Undecidable Equivalence Problems; II. Decidable Equivalence Problems STOC Robert L. Constable, Steven S. Muchnick
1972	J	`jnl`	Subrecursive Program Schemata I & II: I. Undecidable Equivalence problems; II. Decidable Equivalence Problems. J. Comput. Syst. Sci. Robert L. Constable, Steven S. Muchnick
1972	J	`jnl`	Subrecursive Programming Languages, Part I: efficiency and program structure. J. ACM Robert L. Constable, Allan Borodin
1972	J	`jnl`	The Operator Gap. J. ACM Robert L. Constable
1971	A*	`conf`	Complexity of Formal Translations and Speed-Up Results STOC Robert L. Constable, Juris Hartmanis
1971	—	`conf`	Constructive Mathematics and Automatic Program Writers. IFIP Congress (1) Robert L. Constable
1971	A*	`conf`	Loop Schemata STOC Robert L. Constable
1971	—	`conf`	On Classes of Program Schemata SWAT Robert L. Constable, David Gries
1971	J	`jnl`	Subrecursive Programming Languages. II. On Program Size. J. Comput. Syst. Sci. Robert L. Constable
1970	—	`conf`	On the Efficiency of Programs in Subrecursive Formalisms (Incomplete Version, Extended Abstract) SWAT Robert L. Constable, Allan Borodin
1970	A*	`conf`	On the Size of Programs in Subrecursive Formalisms STOC Robert L. Constable
1969	—	`conf`	Dense and Non-Dense Families of Complexity Classes SWAT Allan Borodin, Robert L. Constable, John E. Hopcroft
1969	—	`conf`	The Operator Gap SWAT Robert L. Constable