# Knowledge Base list of Publications

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

## List by Year

247 results

2020

*
Cubical type theory with several universes in Nuprl *

by Mark Bickford

May 20, 2020

*
The Continuum *

by Robert L. Constable

February 26, 2020

*
DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics *

by Mark Bickford

February 18, 2020

*
Intuitionistic Mathematics and Logic *

by Joan Rand Moschovakis, Garyfallia Vafeiadou

January 25, 2020

*
Computer Science at the Frontiers of Mathematics *

by Robert L. Constable

January 15, 2020

*
Formalization of Cubical Type Theory in Nuprl *

by Mark Bickford

January 15, 2020

*
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic *

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

2020

2019

*
Automated Reasoning in Herbrand Structures *

by Liron Cohen, Reuben Rowe, Yoni Zohar

June 03, 2019

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

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

2019

2018

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

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

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

by Liron Cohen, Reuben Rowe

July 01, 2018

*
Validating Brouwerâ€™s Continuity Principle for Numbers Using Named Exceptions *
| cite »

by Vincent Rahli, Mark Bickford

January 02, 2018

*
Computability Beyond Church-Turing using Choice Sequences *
| cite »

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

2018

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

by Mark Bickford

2018

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

by Mark Bickford

2018

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

by Ariel Kellison, Mark Bickford, Robert L. Constable

2018

2017

*
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

2016

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

by Mark Bickford

March 02, 2016

*
A Nominal Exploration of Intuitionism *

by Vincent Rahli, Mark Bickford

January 18, 2016

*
A Formal Exploration of Constructive Geometry *

by Robert L. Constable, Sarah Sernaker

2016

2015

*
Intuitionistic Ancestral Logic *

by Liron Cohen, Robert L. Constable

October 10, 2015

*
Coq as a Metatheory for Nuprl with Bar Induction *

by Vincent Rahli, Mark Bickford

September 14, 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

*
Brouwer's Fan Theorem: An Overview *

by Crystal Cheung

2015

2014

*
A Generic Approach to Proofs about Substitution *

by Abhishek Anand, Vincent Rahli

July 17, 2014

*
Towards a Formally Verified Proof Assistant *

by Abhishek Anand, Vincent Rahli

July 14, 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

*
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

2013

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

by Vincent Rahli, Mark Bickford, Abhishek Anand

April 22, 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

2012

*
Next Generation Proof Technology *

by Robert L. Constable

December 27, 2012

*
Byzantine Chain Replication *
| cite »

by Robbert van Renesse, Chi Ho, Nicolas Schiper

December 20, 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

*
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

*
Logic, Construction, Computation *
| cite »

by Ulrich Berger

July 29, 2012

*
Polymorphic Logic *
| cite »

by Mark Bickford, Robert L. Constable

July 29, 2012

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

by Vincent Rahli

July 11, 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

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

by Christoph Kreitz

April 26, 2012

*
Proof Assistants and the Rise of Type Theory Circa 1912-2012 *

by Robert L. Constable

March 19, 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

2011

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

by Robert L. Constable, Mark Bickford

October 07, 2011

*
Introduction to Classic ML *
| cite »

by Christoph Kreitz, Vincent Rahli

2011

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

by Vincent Rahli

2011

2010

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

by Mark Bickford

2010

*
Encoding Pi Calculus *
| cite »

by David Guaspari

2010

*
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

2009

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

by Robert L. Constable

2009

*
Component Specification Using Event Classes *
| cite »

by Mark Bickford

2009

2008

*
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

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

by Mark Bickford

2008

2007

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

by Robert L. Constable

January 11, 2007

*
A Dependent Set Theory *

by Wojciech Moczydlowski

2007

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

by Wojciech Moczydlowski, Robert L. Constable

2007

2006

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

by Wojciech Moczydlowski

2006

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

by Stuart F. Allen

2006

*
Automating Proofs in Category Theory *
| cite »

by Dexter Kozen, Christoph Kreitz, Eva Richter

2006

*
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

*
Formalizing chain replication *

by Mark Bickford, David Guaspari

2006

*
Implementing Reflection in Nuprl *
| cite »

by Eli Barzilay

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

*
Normalization of intuitionistic set theories. *
| cite »

by Wojciech Moczydlowski

2006

*
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

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

by Lori Lorigo

2006

2005

*
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

*
A Programming Logic for Distributed Systems *
| cite »

by Mark Bickford, David Guaspari

2005

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

by Wojciech Moczydlowski, Alfons Geser

2005

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

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

by Stuart F. Allen

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

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

by Alexei Kopylov

2004

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

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

by Alexei Kopylov

2003

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

by Jason Hickey, Aleksey Nogin

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

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

by Christoph Kreitz

2003

2002

*
Abstract Identifiers and Textual Reference *
| cite »

by Stuart F. Allen

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

*
Planning Proof Content for Communicating Induction *
| cite »

by Amanda Holland-Minkley

2002

*
Quotient Types: A Modular Approach *
| cite »

by Aleksey Nogin

2002

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

by Eli Barzilay, Stuart F. Allen

2002

2001

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

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

2001

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

by Ralph Benzinger

2001

*
Automated Computational Complexity Analysis *
| cite »

by Ralph Benzinger

2001

*
Connection-Driven Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2001

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

by Mark Bickford, Christoph Kreitz, Robbert van Renesse

2001

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

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

2001

*
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

*
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

*
The MetaPRL Logical Programming Environment *
| cite »

by Jason Hickey

2001

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

by Aleksey Nogin

2001

2000

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

by Christoph Kreitz, Stephan Schmitt

2000

*
Fast Tactic-Based Theorem Proving *
| cite »

by Jason Hickey, Aleksey Nogin

2000

*
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

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

by Robert L. Constable, Jason Hickey

2000

*
Search Algorithms in Type Theory *
| cite »

by James L. Caldwell, Ian Gent, Judith Underwood

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

1999

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

by Mark Bickford, Jason Hickey

1999

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

by Christoph Kreitz

1999

*
Automating Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

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

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

by Christoph Kreitz, Jens Otten

1999

*
Dependence Analysis Through Type Inference *
| cite »

by Ozan Hafizogullari, Christoph Kreitz

1999

*
Fault-Tolerant Distributed Theorem Proving *
| cite »

by Jason Hickey

1999

*
Intuitionistic Tableau Extracted *
| cite »

by James L. Caldwell

1999

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

by William Aitken, Robert L. Constable, Judith Underwood

1999

*
Specifications and Proofs for Ensemble Layers *
| cite »

by Jason Hickey, Nancy Lynch, Robbert van Renesse

1999

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

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

1999

1998

*
A type annotation scheme for Nuprl *
| cite »

by Douglas J. Howe

October 01, 1998

*
A Matrix Characterization for MELL *
| cite »

by Heiko Mantel, Christoph Kreitz

1998

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

by Christoph Kreitz, Mark Hayden, Jason Hickey

1998

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

by James L. Caldwell

1998

*
Decidability Extracted: Synthesizing *
| cite »

by James L. Caldwell

1998

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

by Christoph Kreitz

1998

*
Formalizing Reference Types in Nuprl *
| cite »

by Pavel Naumov

1998

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

by Stuart F. Allen

1998

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

by Brigitte Pientka, Christoph Kreitz

1998

*
The Ensemble System *
| cite »

by Mark Hayden

1998

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

by Karl Crary

1998

1997

*
Concurrent Refinement in Nuprl *
| cite »

by Roderick Moten

1997

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

by James L. Caldwell

1997

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

by Christoph Kreitz

1997

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

by Karl Crary

1997

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

by James L. Caldwell

1997

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

by Jason Hickey

1997

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

by Robert L. Constable

1997

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

by Jason Hickey

1997

1996

*
Classical Tools for Constructive Proof Search *
| cite »

by James L. Caldwell, Judith Underwood

1996

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

by Robert L. Constable

1996

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

by Jason Hickey

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

*
Importing Mathematics from HOL into Nuprl *
| cite »

by Douglas J. Howe

1996

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

by Douglas J. Howe

1996

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

by Paul B. Jackson

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

1995

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

by Paul B. Jackson

1995

*
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

1994

*
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

*
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

*
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

*
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

1993

*
Formalizing Constructive Real Analysis *
| cite »

by Max B. Forester

1993

*
Reasoning About Functional Programs in Nuprl *
| cite »

by Douglas J. Howe

1993

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

by Mark Aagaard, Miriam Leeser

1993

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

by Judith Underwood

1993

1992

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

by Chetan Murthy

1992

*
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

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

by Christoph Kreitz

1992

*
Metalevel Programming in Constructive Type Theory *
| cite »

by Robert L. Constable

1992

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

by Paul B. Jackson

1992

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

by Wilfred Z. Chen

1992

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

by Miriam Leeser

1992

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

by Douglas J. Howe

1992

1991

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

by Douglas J. Howe

July 15, 1991

*
An Evaluation Semantics for Classical Proofs *
| cite »

by Chetan Murthy

1991

*
Metalogical Frameworks *
| cite »

by David A. Basin, Robert L. Constable

1991

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

by David A. Basin, Douglas J. Howe

1991

*
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

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

by Robert L. Constable

1991

1990

*
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

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

by David A. Basin

1990

*
Extracting Constructive Content from Classical Proofs *
| cite »

by Chetan Murthy

1990

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

1989

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

by Robert L. Constable

1989

*
Building Theories in Nuprl *
| cite »

by David A. Basin

1989

*
Equality in Lazy Computation Systems *
| cite »

by Douglas J. Howe

1989

*
Partial Objects in Type Theory *
| cite »

by Scott F. Smith

1989

*
Verification of Combinational Logic in Nuprl *
| cite »

by David A. Basin, Peter Del Vecchio

1989

*
Logic-Based Knowledge Representation *
| cite »

by Paul B. Jackson

1989

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

by Fausto Giunchiglia, Alan Smaill

1989

1988

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

by David A. Basin

1988

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

by Peter Madden

1988

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

by Douglas J. Howe

1988

*
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

*
Inductive Definition in Type Theory *
| cite »

by Nax P. Mendler

1988

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

by Timothy G. Griffin

1988

*
The Nuprl Proof Development System *
| cite »

by Christian Horn

1988

1987

*
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

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

by Douglas J. Howe

1987

*
Metamathematical Extensibility in Type Theory *
| cite »

by Todd B. Knoblock

1987

*
Partial Objects in Constructive Type Theory *
| cite »

by Scott F. Smith, Robert L. Constable

1987

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

by Douglas J. Howe

1987

*
Type-Theoretic Models of Concurrency *
| cite »

by Walter Rance Cleaveland

1987

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

by Nax P. Mendler

1987

1986

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

by Christoph Kreitz

1986

*
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

1985

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

by Robert W. Harper

1985

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

by Robert L. Constable

1985

*
Extracting Efficient Code from Constructive Proofs *
| cite »

by James T. Sasaki

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

1984

*
Writing Programs That Construct Proofs *
| cite »

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

1984

1981

*
A Logic for Correct Program Development *
| cite »

by Joseph L. Bates

1981

1980

*
Reversal-Bounded Computations *
| cite »

by Tat-hung Chan

1980

1979

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

by Robert L. Constable, James Donahue

July 01, 1979

1978

*
A Programming Logic *
| cite »

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

1978

1977

*
A Constructive Programming Logic *

by Robert L. Constable

August 08, 1977

1971

*
Constructive Mathematics and Automatic Program Writers *
| cite »

by Robert L. Constable

1971