Knowledge Base of
Publications,
Seminars,
& 
Math Library
PhD theses from the project are accessible at the NCSTRL web site.
Filter for: Robert L. Constable
180 results
The Continuum
by Robert L. Constable
February 26, 2020
Computer Science at the Frontiers of Mathematics
by Robert L. Constable
January 15, 2020
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020
Bar Induction is Compatible with Constructive Type Theory
| cite »
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
2019
Computability Beyond Church-Turing using Choice Sequences
| cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018
Implementing Euclid's Straightedge and Compass Constructions in Type Theory
| cite »
by Ariel Kellison, Mark Bickford, Robert L. Constable
2018
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems
| cite »
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
November 15, 2017
Bar Induction: The Good, the Bad, and the Ugly
| cite »
by Vincent Rahli, Mark Bickford, Robert L. Constable
April 11, 2017
A Formal Exploration of Constructive Geometry
by Sarah Sernaker, Robert L. Constable
2016
A Formal Exploration of Constructive Geometry
by Robert L. Constable, Sarah Sernaker
2016
Intuitionistic Ancestral Logic
by Liron Cohen, Robert L. Constable
October 10, 2015
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
September 01, 2015
Nuprl’s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
September 01, 2015
Constructive Reading of Classical Logic
by Robert L. Constable, Sarah Sernaker
2015
Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014
Synthesizing Protocols using the Logic of Events and EventML
by Robert L. Constable, Mark Bickford
September 17, 2014
Logical Investigations, with the Nuprl Proof Assistant
by Robert L. Constable, Anne Trostle
July 22, 2014
Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014
A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014
Inductive Construction in Nuprl Type Theory Using Bar Induction
by Mark Bickford, Robert L. Constable
May 12, 2014
Formalizing Bishop's Constructive Analysis in Constructive Type Theory
by Mark Bickford, Robert L. Constable
April 10, 2014
Intuitionistic Completeness of First-Order Logic
| cite »
by Robert L. Constable, Mark Bickford
January 01, 2014
Virtual Evidence: A Constructive Semantics for Classical Logics
by Robert L. Constable
2014
Nuprl as a Programming Assistant
by Robert L. Constable
November 06, 2013
An Extension of OCaml's Type Theory
by Robert L. Constable
October 23, 2013
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
March 31, 2013
The Logic of Information Flow and the Foundations of Distributed Computing
by Robert L. Constable
January 10, 2013
Next Generation Proof Technology
by Robert L. Constable
December 27, 2012
A Diversified and Correct-by-Construction Broadcast Service
| cite »
by Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable
October 30, 2012
Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012
ShadowDB: A Replicated Database on a Synthesized Consensus Core
| cite »
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
October 07, 2012
Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012
Introduction to the Fall Seminar Series
by Robert L. Constable
September 07, 2012
Polymorphic Logic
| cite »
by Mark Bickford, Robert L. Constable
July 29, 2012
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer
| cite »
by Robert L. Constable
June 29, 2012
Proof Assistants and the Dynamic Nature of Formal Theories
| cite »
by Robert L. Constable
June 29, 2012
Type Theoretic Semantics for First-Order Logic
by Robert L. Constable
May 24, 2012
Proof Assistants and the Rise of Type Theory Circa 1912-2012
by Robert L. Constable
March 19, 2012
Introduction to EventML
by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
February 03, 2012
Proofs as Process
by Robert L. Constable
2012
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory
| cite »
by Robert L. Constable, Fairouz Kamareddine, Twan Laan
2012
The Logic of Events, a framework to reason about distributed systems
| cite »
by Mark Bickford, Vincent Rahli, Robert L. Constable
2012
Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012
Reviewing Nuprl
by Robert L. Constable
March 09, 2012
Stronger Role for Recursive Types Needed for Logic of Events
by Robert L. Constable
February 24, 2012
Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011
Analyzing Access Control Logics Using Evidence Semantics
by Robert L. Constable
September 23, 2011
Seminar History and Initial Planning Meeting
by Robert L. Constable
September 09, 2011
Seminar History and Initial Planning Meeting
by Robert L. Constable, Robert L. Constable
September 09, 2011
Seminar History and Initial Planning Meeting
by Robert L. Constable, Robert L. Constable
September 09, 2011
Intuitionistic Completeness of First-Order Logic
| cite »
by Robert L. Constable, Mark Bickford
October 07, 2011
Generating Event Logics with Higher-Order Processes as Realizers
| cite »
by Mark Bickford, Robert L. Constable, David Guaspari
2010
Investigating Correct-by-Construction Attack-Tolerant Systems
| cite »
by Robert L. Constable, Mark Bickford, Robbert van Renesse
2010
The Triumph of Types: Principia Mathematica's Impact on Computer Science
| cite »
by Robert L. Constable
2010
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
| cite »
by Robert L. Constable
2009
Computational Type Theory -- Extended Version
| cite »
by Robert L. Constable
2008
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP
| cite »
by Robert L. Constable
2008
Formal Foundations of Computer Security
| cite »
by Mark Bickford, Robert L. Constable
2008
Transforming the Academy: Knowledge Formation in the Age of Digital Information
by Robert L. Constable
January 11, 2007
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus
| cite »
by Wojciech Moczydlowski, Robert L. Constable
2007
Enabling Large Scale Coherency Among Mathematical Texts
| cite »
by Stuart F. Allen, Robert L. Constable
2006
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
| cite »
by Robert L. Constable, Wojciech Moczydlowski
2006
Information-Intensive Proof Technology
| cite »
by Robert L. Constable
2006
Innovations in Computational Type Theory using Nuprl
| cite »
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, Evan Moran
2006
Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts
| cite »
by Stuart F. Allen, Robert L. Constable, Lori Lorigo
2006
A Causal Logic of Events in Formalized Computational Type Theory
| cite »
by Mark Bickford, Robert L. Constable
2005
Knowledge-based synthesis of distributed systems using event structures
| cite »
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2005
Randomness and Free Choice Sequences
by Robert L. Constable
February 04, 2005
Remarks on Nijmegen trip
by Robert L. Constable
November 08, 2004
Foundations for the Management of Formal Mathematical Knowledge
by Robert L. Constable
October 25, 2004
Automated Reasoning in Category Theory
by Robert L. Constable
October 04, 2004
A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.
| cite »
by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable
2004
Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations
| cite »
by Stuart F. Allen, Robert L. Constable, Matthew Fluet
2004
Knowledge-Based Synthesis of Distributed Systems Using Event Structures
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2004
Important Episodes in the History of Constructive Mathematics--including the frog and mouse wars
by Robert L. Constable
March 01, 2004
Comparing Aspects of Set Theory and Type Theory
by Robert L. Constable
February 16, 2004
Planning Session for Spring Seminar Series
by Robert L. Constable
January 26, 2004
Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge
by Robert L. Constable
October 27, 2003
An Introduction to Event Systems
by Robert L. Constable
September 29, 2003
Introduction to the Fall Seminar Series
by Robert L. Constable
September 08, 2003
A Logic of Events
| cite »
by Mark Bickford, Robert L. Constable
2003
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics
| cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003
MetaPRL -- A Modular Logical Environment
| cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003
Practical Reflection in Nuprl
| cite »
by Eli Barzilay, Stuart F. Allen, Robert L. Constable
2003
Recent Results in Type Theory and Their Relationship to Automath
| cite »
by Robert L. Constable
2003
Continuing Discussion of the NSDL
by Robert L. Constable
April 14, 2003
Enabling Active Mathematical Documents in the National Science Digital Library
by Robert L. Constable
March 31, 2003
Uri Abraham's Models for Concurrency
by Robert L. Constable, Sabina Petride
January 27, 2003
Continuing Discussion of Objects
by Alexei Kopylov, Robert L. Constable
December 02, 2002
Classes and Objects
by Robert L. Constable
November 25, 2002
Introduction to Event Systems and the Logic of Distributed Systems
by Mark Bickford, Robert L. Constable
September 16, 2002
Computational Complexity and Induction for Partial Computable Functions in Type Theory
| cite »
by Robert L. Constable, Karl Crary
2002
FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002
Naive Computational Type Theory
| cite »
by Robert L. Constable
2002
Properties of the Formal Digital Library
by Robert L. Constable
May 06, 2002
Report on the Design of the Formal Digital Library
by Richard Eaton, Robert L. Constable, Stuart F. Allen
April 08, 2002
Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002
Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics
by Stuart F. Allen, Robert L. Constable
December 03, 2001
Embedded Ststems
by Christoph Kreitz, Robert L. Constable
November 05, 2001
Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001
Processing video streams using event notification systems
by Robert L. Constable, Mark Bickford
October 15, 2001
Report on the Edinburgh Conference: 35 Years of Automath
by Robert L. Constable
2001-2002
Finite Automata
by Robert L. Constable
May 16, 2001
An Experiment in Formal Design Using Meta-Properties
| cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable
2001
Logical Aspects of Digital Mathematics Libraries (extended abstract)
| cite »
by Stuart F. Allen, James L. Caldwell, Robert L. Constable
2001
Protocol Switching: Exploiting Meta-Properties
| cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001
NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 26, 2001
NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 26, 2001
NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 12, 2001
NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 12, 2001
How Nuprl Reasons
by Robert L. Constable
January 29, 2001
Discussing the issues surrounding our library of formal algorithmic mathematics
by Robert L. Constable
November 13, 2000
Reading BAAs and RFPs (cont.)
by Robert L. Constable
October 23, 2000
Reading BAAs and RFPs
by Robert L. Constable
October 16, 2000
Research Directions
by Robert L. Constable
September 25, 2000
Nuprl's Class Theory and Its Applications
| cite »
by Robert L. Constable, Jason Hickey
2000
The Horus and Ensemble Projects: Accomplishments and Limitations
| cite »
by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels
2000
The Nuprl Open Logical Environment
| cite »
by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2000
Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999
Points of Contact with Girard (Nuprl ∩ Ludics)
by Robert L. Constable
September 13, 1999
Building Reliable, High-Performance Communication Systems from Components
| cite »
by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable
1999
Metalogical Frameworks II: Developing a Reflected Decision Procedure
| cite »
by William Aitken, Robert L. Constable, Judith Underwood
1999
Verbalization of High-Level Formal Proofs
| cite »
by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable
1999
Some Uses of the Intersection Type
by Stuart F. Allen, Robert L. Constable
May 03, 1999
Semantics and Pragmatics of Reflected Proof
by Stuart F. Allen, Sergei Artemov, Robert L. Constable
December 01, 1998
Reflection Mechanisms in Nuprl
by Stuart F. Allen, Robert L. Constable
November 10, 1998
On Modeling Ensemble
by Robert L. Constable, Jason Hickey
October 27, 1998
Listening to Theorem Provers who Talk to Each Other about Computer Systems
by Robert L. Constable
October 20, 1998
The Structure of Nuprl's Type Theory
| cite »
by Robert L. Constable
1997
Computability is Ineffable in ZF Set Theory
by Robert L. Constable
April 01, 1997
Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997
Collaborative Mathematics Environments
by Robert L. Constable
November 21, 1996
Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing
| cite »
by Robert L. Constable
1996
Formalizing Automata II: Decidable Properties
| cite »
by Robert L. Constable, Pavel Naumov
1996
Formalizing Automata Theory I: Finite Automata
| cite »
by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe
1996
The Value of Automated Deduction
| cite »
by Robert L. Constable
1996
Collaborative Mathematics Environments
| cite »
by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel
1996
Project Direction and Research Problems
by Robert L. Constable
February 06, 1996
Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995
| cite »
by Robert L. Constable
1995
Expressing Computational Complexity in Constructive Type Theory
| cite »
by Robert L. Constable
1995
Defining the Polynomial Time Functions over N in Nuprl
by Robert L. Constable
March 28, 1995
An Open Architecture for Nuprl
by Robert L. Constable
March 01, 1995
Representing Computational Complexity in Nuprl
by Robert L. Constable
November 22, 1994
Exporting and Reflecting Abstract Meta-mathematics
| cite »
by Robert L. Constable
1994
Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics
| cite »
by Robert L. Constable, Paul B. Jackson
1994
Using Reflection to Explain and Enhance Type Theory
| cite »
by Robert L. Constable
1994
Theorem Proving with Real Numbers
by Robert L. Constable
August 31, 1993
Project Overview
by Robert L. Constable
July 01, 1993
Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993
Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993
Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993
Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993
Formal Theories and Software Systems: Fundamental Connections Between Computer Science and Logic
| cite »
by Robert L. Constable
1992
Lectures on: Classical Proofs as Programs
| cite »
by Robert L. Constable
1992
Metalevel Programming in Constructive Type Theory
| cite »
by Robert L. Constable
1992
Metalogical Frameworks
| cite »
by David A. Basin, Robert L. Constable
1991
Finding Computational Content from Classical Proofs
| cite »
by Robert L. Constable, Chetan Murthy
1991
Type Theory as a Foundation for Computer Science
| cite »
by Robert L. Constable
1991
Implementing Metamathematics as an Approach to Automatic Theorem Proving
| cite »
by Robert L. Constable, Douglas J. Howe
1990
Nuprl as a General Logic
| cite »
by Robert L. Constable, Douglas J. Howe
1990
Reflecting the Open-Ended Computation System of Constructive Type Theory
| cite »
by Robert L. Constable, Stuart F. Allen, Douglas J. Howe
1990
The Semantics of Reflected Proof
| cite »
by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken
1990
Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments
| cite »
by Robert L. Constable
1989
Computational Foundations of Basic Recursive Function Theory
| cite »
by Robert L. Constable, Scott F. Smith
1988
Collaborative Problem Solving Environment
by Robert L. Constable
1988
Typed Enumeration-Free External Setting for Computing Theory
by Robert L. Constable
November 03, 1987
Partial Objects in Constructive Type Theory
| cite »
by Scott F. Smith, Robert L. Constable
1987
Formalized Metareasoning in Type Theory
| cite »
by Todd B. Knoblock, Robert L. Constable
1986
Implementing Mathematics with the Nuprl Development System
| cite »
by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith
1986
Infinite Objects in Type Theory
| cite »
by Nax P. Mendler, Robert L. Constable, Prakash Panangaden
1986
Constructive Mathematics as a Programming Logic I: Some Principles of Theory
| cite »
by Robert L. Constable
1985
Proofs as Programs
| cite »
by Joseph L. Bates, Robert L. Constable
1985
Recursive Definitions in Type Theory
| cite »
by Robert L. Constable, Nax P. Mendler
1985
Semantics of Evidence
| cite »
by Robert L. Constable
1985
Universally Closed Classes
by Robert L. Constable
1984-1985
Writing Programs That Construct Proofs
| cite »
by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates
1984
A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS
| cite »
by Robert L. Constable, James Donahue
July 01, 1979
A Programming Logic
| cite »
by Robert L. Constable, Michael J. O'Donnell
1978
A Constructive Programming Logic
by Robert L. Constable
August 08, 1977
Constructive Mathematics and Automatic Program Writers
| cite »
by Robert L. Constable
1971