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