#
Knowledge Base of

Publications,
Seminars,
& Math Library

PhD theses from the project are accessible at the NCSTRL web site.

## Filter for: Robert L. Constable

177 results

*
Bar Induction is Compatible with Constructive Type Theory *

by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable

2018

*
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 *

by Ariel Kellison, Mark Bickford, Robert L. Constable

2018

*
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

November 15, 2017

*
Bar Induction: The Good, the Bad, and the Ugly *

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