# Knowledge Base list of Publications

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

## List by Subject

Type Theory | Systems | Special Topics | Proofs | Programming Languages | Nuprl | Logic | Intuitionistic Mathematics | History | Geometry | EventML | Cubical Type Theory

239 results

Type Theory

*
Bar Induction is Compatible with Constructive Type Theory *
| cite »

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

*
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 Rise of Type Theory Circa 1912-2012 *

by Robert L. Constable

March 19, 2012

*
Type-Theoretic Methodology for Practical Programming Languages *
| cite »

by Karl Crary

1998

Systems

*
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

Special Topics

*
Brouwer's Fan Theorem: An Overview *

by Crystal Cheung

2015

Proofs

*
Proof Assistants and the Dynamic Nature of Formal Theories *
| cite »

by Robert L. Constable

June 29, 2012

*
Proofs as Process *

by Robert L. Constable

2012

Programming Languages

*
A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS *
| cite »

by Robert L. Constable, James Donahue

July 01, 1979

Nuprl

*
A Verified Theorem Prover Backend Supported by a Monotonic Library *
| cite »

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

*
Nuprl as Logical Framework for Automating Proofs in Category *
| cite »

by Christoph Kreitz

April 26, 2012

*
Validating Brouwer’s Continuity Principle for Numbers Using Named Exceptions *
| cite »

by Vincent Rahli, Mark Bickford

January 02, 2018

Logic

*
A Constructive Programming Logic *

by Robert L. Constable

August 08, 1977

*
Bar Induction: The Good, the Bad, and the Ugly *
| cite »

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 2017

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

October 07, 2011

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

January 01, 2014

*
Logic, Construction, Computation *
| cite »

by Ulrich Berger

July 29, 2012

*
Polymorphic Logic *
| cite »

by Mark Bickford, Robert L. Constable

July 29, 2012

*
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory *
| cite »

by Robert L. Constable, Fairouz Kamareddine, Twan Laan

2012

*
Type Theoretic Semantics for First-Order Logic *

by Robert L. Constable

May 24, 2012

*
Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent *
| cite »

by Liron Cohen, Reuben Rowe

July 01, 2018

*
Virtual Evidence: A Constructive Semantics for Classical Logics *

by Robert L. Constable

2014

Intuitionistic Mathematics

*
Connectedness of the Continuum in Intuitionistic Mathematics *
| cite »

by Mark Bickford

2018

History

*
Transforming the Academy: Knowledge Formation in the Age of Digital Information *

by Robert L. Constable

January 11, 2007

Geometry

*
A Formal Exploration of Constructive Geometry *

by Robert L. Constable, Sarah Sernaker

2016

*
Implementing Euclid's Straightedge and Compass Constructions in Type Theory *
| cite »

by Ariel Kellison, Mark Bickford, Robert L. Constable

2018

EventML

*
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

*
Interfacing with Proof Assistants for Domain Specific Programming Using EventML *
| cite »

by Vincent Rahli

July 11, 2012

Cubical Type Theory

*
Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl *
| cite »

by Mark Bickford

2018

*
A Causal Logic of Events in Formalized Computational Type Theory *
| cite »

by Mark Bickford, Robert L. Constable

2005

*
A Computational Analysis of Girard's Translation and LC *
| cite »

by Chetan Murthy

1992

*
A Constructive Completeness Proof for the Intuitionistic Propositional Calculus *
| cite »

by Judith Underwood

1990

*
A Constructive Proof of Higman's Lemma *
| cite »

by Chetan Murthy, James R. Russell

1990

*
A Dependent Set Theory *

by Wojciech Moczydlowski

2007

*
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

*
A Generic Approach to Proofs about Substitution *

by Abhishek Anand, Vincent Rahli

July 17, 2014

*
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

*
A Logic for Correct Program Development *
| cite »

by Joseph L. Bates

1981

*
A Logic of Events *
| cite »

by Mark Bickford, Robert L. Constable

2003

*
A Matrix Characterization for MELL *
| cite »

by Heiko Mantel, Christoph Kreitz

1998

*
A Nominal Exploration of Intuitionism *

by Vincent Rahli, Mark Bickford

January 18, 2016

*
A Non-Type-Theoretic Definition of Martin-Lof's Types *
| cite »

by Stuart F. Allen

1987

*
A Non-Type-Theoretic Semantics for Type-Theoretic Language *
| cite »

by Stuart F. Allen

1987

*
A Normalizing Intuitionistic Set Theory with Inaccessible Sets *
| cite »

by Wojciech Moczydlowski

2006

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz

2003

*
A Proof Environment for the Development of Group Communication Systems *
| cite »

by Christoph Kreitz, Mark Hayden, Jason Hickey

1998

*
A type annotation scheme for Nuprl *
| cite »

by Douglas J. Howe

October 01, 1998

*
A Type Theory with Partial Equivalence Relations as Types *

by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli

May 12, 2014

*
A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems *
| cite »

by Christoph Kreitz, Stephan Schmitt

2000

*
Abstract Identifiers and Textual Reference *
| cite »

by Stuart F. Allen

2002

*
Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping *
| cite »

by Stuart F. Allen

2004

*
An Abstract Semantics for Atoms in Nuprl *
| cite »

by Stuart F. Allen

2006

*
An Environment for Automated Reasoning About Partial Functions *
| cite »

by David A. Basin

1988

*
An Evaluation Semantics for Classical Proofs *
| cite »

by Chetan Murthy

1991

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable

2001

*
An Object-Oriented Approach to Verifying Group Communication Systems *
| cite »

by Mark Bickford, Jason Hickey

1999

*
An Operational Approach to Combining Classical Set Theory and Functional Programming Languages *
| cite »

by Douglas J. Howe, Scott D. Stoller

1994

*
Aspects of the Computational Content of Proofs *
| cite »

by Judith Underwood

1994

*
Aspects of the Implementation of Type Theory *
| cite »

by Robert W. Harper

1985

*
Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments *
| cite »

by Robert L. Constable

1989

*
Automated Complexity Analysis of Nuprl Extracted Programs *
| cite »

by Ralph Benzinger

2001

*
Automated Computational Complexity Analysis *
| cite »

by Ralph Benzinger

2001

*
Automated Fast-Track Reconfiguration of Group Communication Systems *
| cite »

by Christoph Kreitz

1999

*
Automated Proof of Authentication Protocols in a Logic of Events *
| cite »

by Mark Bickford

2010

*
Automatic Program Optimization Via the Transformation of Nuprl Synthesis Proofs *
| cite »

by Peter Madden

1988

*
Automating Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1999

*
Automating Proofs in Category Theory *
| cite »

by Dexter Kozen, Christoph Kreitz, Eva Richter

2006

*
Automating Reasoning in an Implementation of Constructive Type Theory *
| cite »

by Douglas J. Howe

1988

*
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge *
| cite »

by Robert L. Constable

2009

*
Building Problem Solving Environments in Constructive Type Theory *
| cite »

by David A. Basin

1990

*
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

*
Building Theories in Nuprl *
| cite »

by David A. Basin

1989

*
Byzantine Chain Replication *
| cite »

by Robbert van Renesse, Chi Ho, Nicolas Schiper

December 20, 2012

*
Classical Propositional Decidability via Nuprl Proof Extraction *
| cite »

by James L. Caldwell

1998

*
Classical Tools for Constructive Proof Search *
| cite »

by James L. Caldwell, Judith Underwood

1996

*
Component Specification Using Event Classes *
| cite »

by Mark Bickford

2009

*
Computational Complexity and Induction for Partial Computable Functions in Type Theory *
| cite »

by Robert L. Constable, Karl Crary

2002

*
Computational Foundations of Basic Recursive Function Theory *
| cite »

by Robert L. Constable, Scott F. Smith

1988

*
Computational Metatheory in Nuprl *
| cite »

by Douglas J. Howe

1988

*
Computational Type Theory -- Extended Version *
| cite »

by Robert L. Constable

2008

*
Concurrent Refinement in Nuprl *
| cite »

by Roderick Moten

1997

*
Connection-Based Theorem Proving in Classical and Non-Classical Logics *
| cite »

by Christoph Kreitz, Jens Otten

1999

*
Connection-Driven Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2001

*
Constructive Analysis and Experimental Mathematics using the Nuprl Proof Assistant *

by Mark Bickford

March 02, 2016

*
Constructive Automata Theory Implemented with the Nuprl Proof Development System *
| cite »

by Christoph Kreitz

1986

*
Constructive Mathematics and Automatic Program Writers *
| cite »

by Robert L. Constable

1971

*
Constructive Mathematics as a Programming Logic I: Some Principles of Theory *
| cite »

by Robert L. Constable

1985

*
Coq as a Metatheory for Nuprl with Bar Induction *

by Vincent Rahli, Mark Bickford

September 14, 2015

*
Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing *
| cite »

by Robert L. Constable

1996

*
Decidability Extracted: Synthesizing *
| cite »

by James L. Caldwell

1998

*
Dependence Analysis Through Type Inference *
| cite »

by Ozan Hafizogullari, Christoph Kreitz

1999

*
Dependent Intersection: A New Way of Defining Records in Type Theory *
| cite »

by Alexei Kopylov

2003

*
Developing Correctly Replicated Databases Using Formal Tools *

by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

June 23, 2014

*
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP *
| cite »

by Robert L. Constable

2008

*
Enabling Large Scale Coherency Among Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable

2006

*
Encoding Pi Calculus *
| cite »

by David Guaspari

2010

*
Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra *
| cite »

by Paul B. Jackson

1995

*
Equality in Lazy Computation Systems *
| cite »

by Douglas J. Howe

1989

*
Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995 *
| cite »

by Robert L. Constable

1995

*
Exploring Abstract Algebra in Constructive Type Theory *
| cite »

by Paul B. Jackson

1994

*
Exporting and Reflecting Abstract Meta-mathematics *
| cite »

by Robert L. Constable

1994

*
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

*
Expressing Computational Complexity in Constructive Type Theory *
| cite »

by Robert L. Constable

1995

*
Extracting Constructive Content from Classical Proofs *
| cite »

by Chetan Murthy

1990

*
Extracting Efficient Code from Constructive Proofs *
| cite »

by James T. Sasaki

1985

*
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics *
| cite »

by Robert L. Constable, Wojciech Moczydlowski

2006

*
Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extracted Program *
| cite »

by James L. Caldwell

1997

*
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus *
| cite »

by Wojciech Moczydlowski, Robert L. Constable

2007

*
Fast Tactic-Based Theorem Proving *
| cite »

by Jason Hickey, Aleksey Nogin

2000

*
Fault-Tolerant Distributed Theorem Proving *
| cite »

by Jason Hickey

1999

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Formal Compiler Implementation in a Logical Framework *
| cite »

by Jason Hickey, Aleksey Nogin

2003

*
Formal Foundations of Computer Security *
| cite »

by Mark Bickford, Robert L. Constable

2008

*
Formal Objects in Type Theory Using Very Dependent Types *
| cite »

by Jason Hickey

1996

*
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types *
| cite »

by Vincent Rahli, Mark Bickford, Abhishek Anand

April 22, 2013

*
Formal Reasoning About Communication Systems I: Embedding ML in Type Theory *
| cite »

by Christoph Kreitz

1997

*
Formal Reasoning About Communication Systems II: Automated Fast-Track Reconfiguration *
| cite »

by Christoph Kreitz

1998

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems *

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

March 31, 2013

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML *

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

September 01, 2015

*
Formal Theories and Software Systems: Fundamental Connections Between Computer Science and Logic *
| cite »

by Robert L. Constable

1992

*
Formalized Metareasoning in Type Theory *
| cite »

by Todd B. Knoblock, Robert L. Constable

1986

*
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

*
Formalizing chain replication *

by Mark Bickford, David Guaspari

2006

*
Formalizing Constructive Real Analysis *
| cite »

by Max B. Forester

1993

*
Formalizing Reference Types in Nuprl *
| cite »

by Pavel Naumov

1998

*
Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse

2001

*
Foundations for the Implementation of Higher-Order Subtyping *
| cite »

by Karl Crary

1997

*
From dy/dx to []P: A Matter of Notation *
| cite »

by Stuart F. Allen

1998

*
Generating Event Logics with Higher-Order Processes as Realizers *
| cite »

by Mark Bickford, Robert L. Constable, David Guaspari

2010

*
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

*
Implementing Metamathematics as an Approach to Automatic Theorem Proving *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Implementing Number Theory: An Experiment with Nuprl *
| cite »

by Douglas J. Howe

1987

*
Implementing Reflection in Nuprl *
| cite »

by Eli Barzilay

2006

*
Importing Mathematics from HOL into Nuprl *
| cite »

by Douglas J. Howe

1996

*
Inductive Construction in Nuprl Type Theory Using Bar Induction *

by Mark Bickford, Robert L. Constable

May 12, 2014

*
Inductive Definition in Type Theory *
| cite »

by Nax P. Mendler

1988

*
Infinite Objects in Type Theory *
| cite »

by Nax P. Mendler, Robert L. Constable, Prakash Panangaden

1986

*
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

*
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1998

*
Introduction to Classic ML *
| cite »

by Christoph Kreitz, Vincent Rahli

2011

*
Intuitionistic Ancestral Logic *

by Liron Cohen, Robert L. Constable

October 10, 2015

*
Intuitionistic Tableau Extracted *
| cite »

by James L. Caldwell

1999

*
Investigating Correct-by-Construction Attack-Tolerant Systems *
| cite »

by Robert L. Constable, Mark Bickford, Robbert van Renesse

2010

*
Investigations in intersection types:Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method *
| cite »

by Vincent Rahli

2011

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

2001

*
Knowledge-Based Synthesis of Distributed Systems Using Event Structures *

by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

2004

*
Knowledge-based synthesis of distributed systems using event structures *
| cite »

by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

2005

*
Lectures on: Classical Proofs as Programs *
| cite »

by Robert L. Constable

1992

*
Logical Aspects of Digital Mathematics Libraries (extended abstract) *
| cite »

by Stuart F. Allen, James L. Caldwell, Robert L. Constable

2001

*
Markov's Principle For Propositional Type Theory *
| cite »

by Alexei Kopylov, Aleksey Nogin

2001

*
Matrix-Based Constructive Theorem Proving *
| cite »

by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka

2000

*
Matrix-Based Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2000

*
Meta-Synthesis: Deriving Programs That Develop Programs *
| cite »

by Christoph Kreitz

1992

*
Metalevel Programming in Constructive Type Theory *
| cite »

by Robert L. Constable

1992

*
Metalogical Frameworks *
| cite »

by David A. Basin, Robert L. Constable

1991

*
Metalogical Frameworks II: Developing a Reflected Decision Procedure *
| cite »

by William Aitken, Robert L. Constable, Judith Underwood

1999

*
Metamathematical Extensibility in Type Theory *
| cite »

by Todd B. Knoblock

1987

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
Moving Proofs-as-Programs into Practice *
| cite »

by James L. Caldwell

1997

*
Naive Computational Type Theory *
| cite »

by Robert L. Constable

2002

*
Next Generation Proof Technology *

by Robert L. Constable

December 27, 2012

*
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization *
| cite »

by John O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard

1994

*
Normalization of intuitionistic set theories. *
| cite »

by Wojciech Moczydlowski

2006

*
Notational Definition and Top-down Refinement for Interactive Proof Development Systems *
| cite »

by Timothy G. Griffin

1988

*
Nuprl and Its Use in Circuit Design *
| cite »

by Paul B. Jackson

1992

*
Nuprl as a General Logic *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Nuprl's Class Theory and Its Applications *
| cite »

by Robert L. Constable, Jason Hickey

2000

*
Nuprl-Light: An Implementation Framework for Higher-Order Logics *
| cite »

by Jason Hickey

1997

*
Nuprl’s Inductive Logical Forms *

by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli

September 01, 2015

*
On computational open-endedness in Martin-Lof's type theory *

by Douglas J. Howe

July 15, 1991

*
Partial Objects in Constructive Type Theory *
| cite »

by Scott F. Smith, Robert L. Constable

1987

*
Partial Objects in Type Theory *
| cite »

by Scott F. Smith

1989

*
Planning Proof Content for Communicating Induction *
| cite »

by Amanda Holland-Minkley

2002

*
Practical Reflection in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen, Robert L. Constable

2003

*
Proofs as Programs *
| cite »

by Joseph L. Bates, Robert L. Constable

1985

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable

2001

*
Proving Hybrid Protocols Correct *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu

2001

*
Quotation and Reflection in Nuprl and Scheme *
| cite »

by Eli Barzilay

2001

*
Quotient Types: A Modular Approach *
| cite »

by Aleksey Nogin

2002

*
Reasoning About Functional Programs in Nuprl *
| cite »

by Douglas J. Howe

1993

*
Recent Results in Type Theory and Their Relationship to Automath *
| cite »

by Robert L. Constable

2003

*
Recursive Definitions in Type Theory *
| cite »

by Robert L. Constable, Nax P. Mendler

1985

*
Reflecting Higher-Order Abstract Syntax in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen

2002

*
Reflecting the Open-Ended Computation System of Constructive Type Theory *
| cite »

by Robert L. Constable, Stuart F. Allen, Douglas J. Howe

1990

*
Reversal-Bounded Computations *
| cite »

by Tat-hung Chan

1980

*
Search Algorithms in Type Theory *
| cite »

by James L. Caldwell, Ian Gent, Judith Underwood

2000

*
Semantic Foundations for Embedding HOL in Nuprl *
| cite »

by Douglas J. Howe

1996

*
Semantics of Evidence *
| cite »

by Robert L. Constable

1985

*
Some Normalization Properties of Martin-Lof's Type Theory and Applications *
| cite »

by David A. Basin, Douglas J. Howe

1991

*
Specifications and Proofs for Ensemble Layers *
| cite »

by Jason Hickey, Nancy Lynch, Robbert van Renesse

1999

*
Tactic-Based Theorem Proving and Knowledge-Based Forward Chaining: An Experiment with Nuprl and Ontic *
| cite »

by Wilfred Z. Chen

1992

*
The Computational Behaviour of Girard's Paradox *
| cite »

by Douglas J. Howe

1987

*
The Ensemble System *
| cite »

by Mark Hayden

1998

*
The FDL Navigator: Browsing and Manipulating Formal Content *
| cite »

by Christoph Kreitz

2003

*
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 Logic of Events, a framework to reason about distributed systems *
| cite »

by Mark Bickford, Vincent Rahli, Robert L. Constable

2012

*
The Logic of Information Flow and the Foundations of Distributed Computing *

by Robert L. Constable

January 10, 2013

*
The MetaPRL Logical Programming Environment *
| cite »

by Jason Hickey

2001

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

*
The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide *
| cite »

by Paul B. Jackson

1996

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

*
The Structure of Nuprl's Type Theory *
| cite »

by Robert L. Constable

1997

*
The Triumph of Types: Principia Mathematica's Impact on Computer Science *
| cite »

by Robert L. Constable

2010

*
The Value of Automated Deduction *
| cite »

by Robert L. Constable

1996

*
Towards a Formally Verified Proof Assistant *

by Abhishek Anand, Vincent Rahli

July 14, 2014

*
Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics *
| cite »

by Robert L. Constable, Paul B. Jackson

1994

*
Type Theoretical Foundations for Data Structures, Classes, and Objects *
| cite »

by Alexei Kopylov

2004

*
Type-Theoretic Models of Concurrency *
| cite »

by Walter Rance Cleaveland

1987

*
Unguessable Atoms: A Logical Foundation for Security *
| cite »

by Mark Bickford

2008

*
Unguessable Atoms: A Logical Foundation for Security *
| cite »

by Mark Bickford

2006

*
Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable, Lori Lorigo

2006

*
Using Nuprl for the Verification and Synthesis of Hardware *
| cite »

by Miriam Leeser

1992

*
Using Reflection to Explain and Enhance Type Theory *
| cite »

by Robert L. Constable

1994

*
Verbalization of High-Level Formal Proofs *
| cite »

by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable

1999

*
Verification of Combinational Logic in Nuprl *
| cite »

by David A. Basin, Peter Del Vecchio

1989

*
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification *
| cite »

by Mark Aagaard, Miriam Leeser

1993

*
Writing Constructive Proofs Yielding Efficient Extracted Programs *
| cite »

by Aleksey Nogin

2001

*
Writing Programs That Construct Proofs *
| cite »

by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates

1984

*
A Programming Logic *
| cite »

by Robert L. Constable, Michael J. O'Donnell

1978

*
A Programming Logic for Distributed Systems *
| cite »

by Mark Bickford, David Guaspari

2005

*
A Semantics of Objects in Type Theory *
| cite »

by Jason Hickey

1997

*
A Simple Type Theory for Reasoning About Functional Programs *
| cite »

by Douglas J. Howe

1992

*
Collaborative Mathematics Environments *
| cite »

by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel

1996

*
Developing a Toolkit for Floating-Point Hardware in the Nuprl Proof Development System *
| cite »

by Paul B. Jackson

1991

*
Extracting Circuits from Constructive Proofs *
| cite »

by David A. Basin

1991

*
Finding Computational Content from Classical Proofs *
| cite »

by Robert L. Constable, Chetan Murthy

1991

*
Formally Verified Synthesis of Combinational Circuits *
| cite »

by David A. Basin, Geoffrey Brown, Miriam Leeser

1991

*
Information Management in the Service of Knowledge and Discovery *
| cite »

by Lori Lorigo

2006

*
Logic-Based Knowledge Representation *
| cite »

by Paul B. Jackson

1989

*
Recursive Types and Type Constraints in Second-Order Lambda Calculus *
| cite »

by Nax P. Mendler

1987

*
Reflection in Constructive and Non-Constructive Automated Reasoning *
| cite »

by Fausto Giunchiglia, Alan Smaill

1989

*
Termination of Single-Threaded One-rule Semi-Thue Systems *
| cite »

by Wojciech Moczydlowski, Alfons Geser

2005

*
The Nuprl Proof Development System *
| cite »

by Christian Horn

1988

*
The Tableau Algorithm for Intuitionistic Propositional Calculus as a Constructive Completeness Proof *
| cite »

by Judith Underwood

1993

*
Type Theory as a Foundation for Computer Science *
| cite »

by Robert L. Constable

1991