#
Knowledge Base of

Publications,
Seminars,
& Math Library

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

## List by Subject

Type Theory | Theory | Systems | Special Topics | Semantics | Reflection | Puzzels | Proofs | Programming Languages | Nuprl | Meta-PRL | Logic | Intuitionistic Mathematics | HOL | History | Geometry | EventML | Event Structures | Evaluation | Ensemble | Cubical Type Theory | Arithmetic

688 results

Type Theory

*
A Type Theory with Partial Equivalence Relations as Types *

by Vincent Rahli

September 10, 2014

*
An Extension of OCaml's Type Theory *

by Robert L. Constable

October 23, 2013

*
Bar Induction and the Fan Theorem in Constructive Type Theory *

by Robert L. Constable, Mark Bickford, Abhishek Anand

October 12, 2012

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

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

2019

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

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

2018

*
Impredicative vs Predicative Type Theory *

by Robert L. Constable, Mark Bickford, Richard Eaton

April 13, 2012

*
Introduction to the Fall Seminar Series *

by Robert L. Constable

September 07, 2012

*
Issues in Constructive Type Theory *

by Ross Tate

September 14, 2012

*
Nominal Type Theory *

by Mark Bickford, Vincent Rahli

October 29, 2014

*
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer *
| cite »

by Robert L. Constable

June 29, 2012

*
Order-theoretic Differences Between Two Variants of Type Theory *

by Evan Moran

October 19, 2012

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

by Robert L. Constable

March 19, 2012

*
The power of bar induction in constructive type theory *

by Mark Bickford

September 25, 2013

*
The Type Base and Undecidability in Type Theory *

by Abhishek Anand

September 21, 2012

*
Topics in Type Theory *

by Abhishek Anand, Robert L. Constable, Mark Bickford

October 22, 2014

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

by Karl Crary

1998

Theory

*
A Basis for Constructive, Reflexive Type Theory *

by William Aitken

October 01, 1990

*
Advancing the Type-Theoretic Underpinnings of Practical Programming Languages *

by Karl Crary

1996-1997

*
CZF, Type Theory, and Nuprl-Light *

by Evan Moran

April 01, 1997

*
CZF, Type Theory, and Nuprl-Light (continued) *

by Evan Moran

April 08, 1997

*
Formal Domain Theory *

by Neal Glew

December 05, 1995

*
Formal Objects in Type Theory *

by Jason Hickey

1996-1997

*
Formalizing the Theory Concept in Nuprl *

by Jason Hickey

March 15, 1994

*
Formalizing the Theory Mechanism in NuPRL *

by Jason Hickey

March 15, 1994

*
Mechanizing the Proof of Correction of a Compiler Using Type Theory *

by Yves Bertot

November 17, 1998

*
Program Optimization in Type Theory *

by Brent Knight

October 18, 1994

*
References in Type Theory *

by Pavel Naumov

November 25, 1997

Systems

*
Chain Replication Protocol *

by Mark Bickford

September 27, 2006

*
Collaborative Mathematics Environments *

by Robert L. Constable

November 21, 1996

*
Event Systems *

by Mark Bickford

November 08, 2003

*
General Automata Theory *

by Mark Bickford

January 25, 2003

*
Hybrid Protocols *

by Mark Bickford

February 20, 2002

*
Iterated Binary Operations *

by Stuart F. Allen

August 02, 2004

*
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

*
Simple Imperative Programming *

by Pavel Naumov

February 26, 2002

Special Topics

*
Brouwer's Fan Theorem: An Overview *

by Crystal Cheung

2015

*
Intuitionism - The Philosophy of L. E. J. Brouwer *

by Dirk Schlimm

April 24, 1998

*
L. E. J. Brouwer's Intuitionism: A Revolution in Two Installments *

by Dirk van Dalen

June 26, 1998

Semantics

*
A Semantics for Abstract Atoms in Nuprl *

by Stuart F. Allen

March 31, 2006

*
Adding Intersection Types to Doug Howe's Classical Set-Theoretic Semantics *

by Evan Moran

April 07, 1998

*
Analyzing Access Control Logics Using Evidence Semantics *

by Robert L. Constable

September 23, 2011

*
Connecting Formal Semantics to Constructive Intuitions *

by Michael J. O'Donnell

July 06, 1993

*
Denotational Semantics *

by Nax P. Mendler

1984-1985

*
Imperative Program Semantics *

by Stuart F. Allen

May 02, 1995

*
Intensional Polymorphism in Type-Erasure Semantics *

by Stephanie Weirich

April 28, 1998

*
Presenting Semantics for a Fragment of the Java Programming Language in Nuprl Proof Development System *

by Pavel Naumov

March 10, 1998

*
Semantics *

by Scott D. Stoller

March 30, 1993

*
Semantics and Pragmatics of Reflected Proof *

by Stuart F. Allen, Sergei Artemov, Robert L. Constable

December 01, 1998

*
Semantics of the Nuprl Type Theory *

by Scott D. Stoller

March 16, 1993

*
Term Model Semantics and Tait Computability Method *

by Scott F. Smith

March 11, 1987

Reflection

*
Analysis of reflection in programming languages using Scheme as the main example *

by Eli Barzilay

March 06, 2000

*
Continuation on reflection *

by Mark Bickford

March 13, 2000

*
Latest results about reflection (TENTATIVE) *

by Eli Barzilay

November 20, 2000

*
Metamathematics of Reflection *

by Todd B. Knoblock

April 22, 1987

*
On the Reflection Mechanism in Nuprl *

by Sergei Artemov

November 24, 1998

*
Online Demonstration of Syntactic Reflection. Realizing an Argument about Syntax (Tarski). *

by Regina Barzilay

March 03, 2003

*
Practical Uses of Quotations, Macros and Reflection *

by Eli Barzilay

April 05, 1999

*
Reflection *

by William Aitken

April 06, 1993

*
Reflection 2 *

by William Aitken, William Aitken

March 05, 1992

*
Reflection 2 *

by William Aitken, William Aitken

February 18, 1992

*
Reflection in First-Order Logic *

by Eli Barzilay

February 12, 2001

*
Reflection Mechanisms in Nuprl *

by Stuart F. Allen, Robert L. Constable

November 10, 1998

*
Reflection Part II *

by Eli Barzilay

April 03, 2000

*
Using Reflection to External Automated Theorem Provers *

by Mark Aagaard

March 30, 1993

Puzzels

*
Towers of Hanoi *

by Stuart F. Allen

April 27, 2004

Proofs

*
Adding Shared Memory to the General Process Model *

by Jason Wu

April 20, 2012

*
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

*
Recent work with Coq *

by Mark Reitblatt

May 11, 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 proof assistant *

by Vincent Rahli, Abhishek Anand

October 30, 2013

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

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

*
Automatic FDL Projections *

by Richard Eaton

September 01, 2006

*
HOL Translation (partial) *

by Douglas J. Howe

February 13, 2004

*
Introduction to EventML *

by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari

February 03, 2012

*
Nuprl as a Programming Assistant *

by Robert L. Constable

November 06, 2013

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

by Christoph Kreitz

April 26, 2012

*
Nuprl Basics *

by Stuart F. Allen

September 18, 2003

*
Nuprl Editor and Interface *

by Stuart F. Allen

September 23, 2003

*
Project Overview *

by Robert L. Constable

July 01, 1993

*
Quotient Types in Nuprl *

by Mark Bickford

November 13, 2013

*
Standard Resources *

by Stuart F. Allen

September 23, 2003

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

by Vincent Rahli, Mark Bickford

January 02, 2018

*
Wider Deployment of Nuprl *

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

September 28, 2012

*
Work in Progress *

by Richard Eaton

February 20, 2012

Meta-PRL

*
20BJ as a Meta-logical Framework *

by Andrew Stevens

April 21, 1990

*
A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory *

by Alexei Kopylov, Aleksey Nogin

November 27, 2000

*
A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory (cont) *

by Aleksey Nogin, Alexei Kopylov

December 04, 2000

*
Arithmetic module for MetaPRL: rules and Arith tactic *

by Yegor Bryukhov

March 25, 2002

*
Differences between the MetaPRL type theory and the Nuprl type theory *

by Aleksey Nogin

April 10, 2000

*
Formal Module Systems and Nuprl-Light: A Programmer's Perspective *

by Jason Hickey

February 13, 1996

*
Logical Programming Environments *

by Jason Hickey

March 03, 1998

*
Nuprl-Light *

by Jason Hickey, Jason Hickey

1996-1997

*
Nuprl-Light *

by Jason Hickey, Jason Hickey

1996-1997

*
Some Recent Results in MetaPRL *

by Eric Klavins

April 22, 2002

*
Speeding Up the MetaPRL Refiner *

by Aleksey Nogin

February 08, 1999

*
The Current Projects of the MetaPRL Group *

by Aleksey Nogin, Jason Hickey

April 26, 1999

*
The Status of the Meta-Prl Project *

by Aleksey Nogin

October 04, 1999

Logic

*
A Constructive Programming Logic *

by Robert L. Constable

August 08, 1977

*
Automated Reasoning in Herbrand Structures *

by Liron Cohen, Reuben Rowe, Yoni Zohar

June 03, 2019

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

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 2017

*
Classical Propositional Logic *

by James L. Caldwell

July 28, 2004

*
Finite Automata *

by Robert L. Constable

May 16, 2001

*
Formalizing Moessner's Theorem in Nuprl *

by Mark Bickford, Dexter Kozen, Alexandra Silva

June 08, 2012

*
Intuitionistic Ancestral Logic *

by Liron Cohen

July 12, 2012

*
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

*
Logical Investigations, with the Nuprl Proof Assistant *

by Robert L. Constable, Anne Trostle

July 22, 2014

*
Polymorphic Logic *
| cite »

by Mark Bickford, Robert L. Constable

July 29, 2012

*
Russel's Paradox *

by Stuart F. Allen

December 14, 2004

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

by Robert L. Constable, Fairouz Kamareddine, Twan Laan

2012

*
Turing Machine Basics *

by Pavel Naumov

November 01, 1996

*
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

*
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

*
Intuitionistic Mathematics and Logic *

by Joan Rand Moschovakis, Garyfallia Vafeiadou

January 25, 2020

*
The Continuum *

by Robert L. Constable

February 26, 2020

HOL

*
(Constructive) set-theoretic semantics for (Constructive) higher-order logic *

by Wojciech Moczydlowski

November 04, 2005

*
Developing Set Theory in HOL *

by Paul B. Jackson

February 28, 1995

*
HOL Workshop *

by Mark Aagaard

September 15, 1992

*
Importing HOL Theorems into Nuprl *

by Douglas J. Howe

July 30, 1998

*
On Howe's Importation of HOL into Nuprl *

by Evan Moran

September 29, 1998

History

*
Seminar History and Initial Planning Meeting *

by Robert L. Constable

September 09, 2011

*
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

*
An Intuitionistic Formalization of The Elements of Euclid Book I *

by Ariel Kellison, Mark Bickford

November 26, 2019

*
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

Evaluation

*
HORUS Verification Effort *

by Jason Hickey

1995-1996

Ensemble

*
On Modeling Ensemble *

by Robert L. Constable, Jason Hickey

October 27, 1998

*
Verifying HORUS in Nuprl *

by Jason Hickey

November 28, 1995

Cubical Type Theory

*
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

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

by Mark Bickford

2018

Arithmetic

*
A Fast Algorithm for the Integer Square Root *

by Anne Trostle, Mark Bickford

June 09, 2014

*
An Algorithm for the Greatest Common Divisor *

by Anne Trostle

October 01, 2013

*
Constructive Factorization Theory *

by Paul B. Jackson

August 19, 1999

*
Constructive General Algebra *

by Paul B. Jackson

August 19, 1999

*
Discrete Math Materials *

by Stuart F. Allen

August 02, 2004

*
Elementary Number Theory *

by Stuart F. Allen

September 23, 2003

*
Finding the Maximum Segment Sum *

by Anne Trostle

January 22, 2014

*
Formalizing Constructive Analysis in Nuprl *

by Mark Bickford

September 04, 2012

*
Fundamental Theorem of Arithmetic *

by Stuart F. Allen

August 02, 2004

*
Readability Exercise (num theory) *

by Stuart F. Allen

December 14, 2004

*
Square Root of 2 is Irrational *

by Stuart F. Allen

August 04, 2004

*
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 Formal Exploration of Constructive Geometry *

by Sarah Sernaker, Robert L. Constable

2016

*
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

*
ACL2 Tutorial *

by Mark Reitblatt

March 27, 2014

*
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

*
Coinduction in Coq *

by Abhishek Anand

November 12, 2014

*
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

*
Constructive Reading of Classical Logic *

by Robert L. Constable, Sarah Sernaker

2015

*
Constructive Topology - A Theory of Observation *

by Francisco Mota

October 15, 2014

*
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 Bishop's Constructive Analysis in Constructive Type Theory *

by Mark Bickford, Robert L. Constable

April 10, 2014

*
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

*
From Replicated Databases to Ensembles of Collaborating Robots *

by Abhishek Anand, Mark Bickford

November 19, 2014

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

by Mark Bickford, Robert L. Constable, David Guaspari

2010

*
How far can we go with Induction-Recursion? *

by Abhishek Anand, Vincent Rahli

November 20, 2013

*
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

*
Isabelle Tutorial *

by Steffen Smolka

March 18, 2014

*
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

*
Realizing Bar Induction in Nuprl *

by Mark Bickford

October 26, 2012

*
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

*
Synthesizing Protocols using the Logic of Events and EventML *

by Robert L. Constable, Mark Bickford

September 17, 2014

*
Synthetic Topology in NuPRL *

by Francisco Mota, Mark Bickford

December 03, 2014

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

by Wilfred Z. Chen

1992

*
The Beauty of Nuprl's Uniform Term Representation and How to Reason about those Terms in Coq *

by Abhishek Anand

October 09, 2013

*
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

*
There Are No Discontinuous Real Functions *

by Mark Bickford, Vincent Rahli

October 08, 2014

*
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

*
Transforming Protocols from Shared Memory Models to Message Passing Models Provides a New Source of High Level Synthetic Protocol Diversity *

by Jason Wu

November 09, 2012

*
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

*
(Re-)Introduction to Howe's Framework *

by Evan Moran

September 30, 2005

*
(Re-)Introduction to Howe's Framework, continued *

by Evan Moran

October 14, 2005

*
A (Possibly) New Scheme for Libraries/Proof-Contexts *

by Chetan Murthy

September 03, 1993

*
A Constructive Completeness Proof for Intuitionistic Predicate Calculus *

by Judith Underwood

February 01, 1994

*
A Conversation with Moshe Vardi *

by Moshe Vardi

November 18, 2011

*
A Discussion in Consensus *

by Jason Wu

February 10, 2012

*
A Formal Framework for Modeling Memory *

by Victor Luchangco

February 22, 1999

*
A Linguistic View of Constuctive Type Theory *

by Amanda Holland-Minkley

February 02, 2004

*
A Methodology for Designing Asynchronous Circuits *

by Rajit Manohar

May 10, 1999

*
A Program Transformation System *

by Annie Liu

1993-1994

*
A Programming Environment for Building Reliable High Performance Systems *

by Jason Hickey

February 15, 1999

*
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 Proof-Theoretic Approach to Knowledge Acquisition" *

by Dexter Kozen

January 28, 2002

*
A Reconfigurable Atomic Memory Service for Dynamic Networks *

by Alex Shvartsman

March 24, 2003

*
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

*
A Type Theoretic Interpretation of Doug Howe's Squiggle Relation *

by Stuart F. Allen

April 19, 1988

*
A Uniform Rippling Approach for Instantiating Free Variables *

by Brigitte Pientka

December 02, 1997

*
Abstact Data Structures, Objects and Classes in the Nuprl Type Theory *

by Alexei Kopylov

November 11, 2002

*
Abstract Identifiers in Nuprl 5 *

by Stuart F. Allen

October 21, 1997

*
Abstract Identifiers in Nuprl 5 (continued) *

by Stuart F. Allen

October 28, 1997

*
Abstract Programming in Nuprl *

by Jason Hickey

November 23, 1993

*
Adapting Proofs-as-Programs for the Synthesis of Imperative SML Programs *

by Iman Poernomo

December 08, 2003

*
Adding Communication Primitives to the Nuprl Evaluator *

by Mark Bickford

May 04, 2012

*
An ACL2 Demo *

by J Strother Moore

October 07, 2002

*
An Efficient Refiner for First-order Intuitionistic Logic *

by Stephan Schmitt

February 28, 2000

*
An Efficient Refiner for First-order Intuitionistic Logic (Part II) *

by Stephan Schmitt

May 22, 2000

*
An Introduction to Event Systems *

by Robert L. Constable

September 29, 2003

*
An Introduction to Region Inference *

by David Walker

November 08, 1999

*
An Open Architecture for Nuprl *

by Robert L. Constable

March 01, 1995

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

by Scott D. Stoller

March 29, 1994

*
Anchoring Expository Text in Formal Mathematics *

by Stuart F. Allen

December 06, 2004

*
Anchoring Expository Text in Formal Mathematics -- Part II *

by Stuart F. Allen

April 15, 2005

*
Application of Event Systems and the Logic of Distributed Systems to Leader Election *

by Mark Bickford

September 30, 2002

*
Application of Notational Methods in dy/dx *

by Stuart F. Allen

March 31, 1998

*
Applied Logic as Part of an Effort to Accumulate Precise Knowledge *

by Stuart F. Allen

February 09, 2004

*
Are There Long Reduction Sequences with Short Normal Forms? *

by Helmut Schwichtenberg

September 29, 1992

*
Arithpac *

by Timothy G. Griffin

1984-1985

*
Attaching Context to Objects in the Library *

by Stuart F. Allen

February 04, 1992

*
Automated Complexity Analysis *

by Ralph Benzinger

September 15, 1998

*
Automated Higher-Order Complexity Analysis *

by Ralph Benzinger

February 05, 2001

*
Automated Proofs in Event Logic *

by Mark Bickford

September 16, 2005

*
Automated Reasoning in Category Theory *

by Robert L. Constable

October 04, 2004

*
Automatic Complexity Analysis Revisited *

by Ralph Benzinger

January 31, 2000

*
Automatic Debugging Through Type Inference *

by Ozan Hafizogullari

October 06, 1998

*
Automatic Debugging Through Type Inference, Continued *

by Ozan Hafizogullari

November 03, 1998

*
Automatic generation of texts from Nuprl proofs *

by Amanda Holland-Minkley

February 04, 2002

*
Automating Proofs in Event Logic *

by Mark Bickford, Richard Eaton

August 26, 2005

*
Automating Proofs in Event Logic *

by Mark Bickford, Richard Eaton

March 23, 2006

*
Bar Types *

by Scott F. Smith

March 18, 1987

*
Bar-Type Rules *

by Karl Crary

January 25, 2002

*
Bridges Between Set Theory and Type Theory *

by Evan Moran

September 15, 2003

*
CADE Practice Talk *

by Wilfred Z. Chen

May 12, 1992

*
Caltech Computer Science *

by Jason Hickey

November 06, 2000

*
Can we Compile the Prolog Program to a Type? *

by Jim Lipton

November 12, 1991

*
Categorical Models of Nuprl *

by Michael Schwartzbach

October 21, 1986

*
Category Theory as Basis for Mathematics *

by John Beck

December 02, 1986

*
CFZ From Below *

by Evan Moran

April 12, 2004

*
CFZ From Below (continued) *

by Evan Moran

April 19, 2004

*
Chet Says Good-Bye: Theory; Implementation (System); Methodology; Science *

by Chetan Murthy

February 14, 1995

*
Classes and Objects *

by Robert L. Constable

November 25, 2002

*
Collaborative Mathematics Environments *
| cite »

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

1996

*
Collaborative Problem Solving Environment *

by Robert L. Constable

1988

*
Comparing Aspects of Set Theory and Type Theory *

by Robert L. Constable

February 16, 2004

*
Computability is Ineffable in ZF Set Theory *

by Robert L. Constable

April 01, 1997

*
Computational Content of Math *

by Douglas Bridges

October 19, 1993

*
Computer Algebra, Theorem Proving, and Types *

by Todd Wilson

October 04, 1994

*
Constructive Algorithms in Nuprl *

by Douglas J. Howe

December 01, 1992

*
Constructive Proofs and Program Extraction *

by Christoph Kreitz

February 23, 2004

*
Continuation of A Type Theoretic Interpretation of DougHowe's Squiggle Relation *

by Stuart F. Allen

April 26, 1988

*
Continuation of Categorial Models of Nuprl *

by Michael Schwartzbach

October 28, 1986

*
Continuation of talk on Polymorphic References *

by Ozan Hafizogullari

September 24, 1999

*
Continuing Discussion of Objects *

by Alexei Kopylov, Robert L. Constable

December 02, 2002

*
Continuing Discussion of the NSDL *

by Robert L. Constable

April 14, 2003

*
Continuing on Objects and Classes *

by Alexei Kopylov

November 18, 2002

*
Coq and Nuprl *

by Wojciech Moczydlowski

July 27, 2004

*
Dead Code Elimination *

by Ozan Hafizogullari, Christoph Kreitz

January 27, 1998

*
DEC *

by Rustan Leino

November 19, 1996

*
Decidability of Linear Affine Logic *

by Alexei Kopylov

November 01, 1999

*
Defining Lambda-prl and Its Extensions *

by Scott F. Smith

1984-1985

*
Defining Polynomials in Constructive Type Theory *

by Paul B. Jackson

1992-1993

*
Defining the Polynomial Time Functions over N in Nuprl *

by Robert L. Constable

March 28, 1995

*
Design and Implemention of the Library Component of Nuprl 5 *

by Richard Eaton

October 03, 1995

*
Design of the Nuprl Refiner *

by Roderick Moten

September 26, 1995

*
Designing a Logical Library *

by Stuart F. Allen

February 24, 1997

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

by Paul B. Jackson

1991

*
Discussing the issues surrounding our library of formal algorithmic mathematics *

by Robert L. Constable

November 13, 2000

*
Discussion of Issues in Logic Library Design *

by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton

March 03, 1997

*
Discussion of Methods of Sharing Formal Mathematics *

by Evan Moran

September 22, 2003

*
Distributed Snapshot Algorithms *

by Keshav Pingali

February 17, 2003

*
Domains in Type Theory *

by Scott F. Smith

November 10, 1987

*
Editing *

by Stuart F. Allen

November 16, 1993

*
Editor Demonstration *

by Paul B. Jackson

March 09, 1993

*
Efficient Automated Proof Search and Proof Reconstruction in Intuitionistic Logic *

by Jens Otten, Stephan Schmitt

June 23, 1998

*
Efficient Programming by Extract in Nuprl Type Theory *

by Aleksey Nogin

February 07, 2000

*
Efficient Programming by Extract in Nuprl Type Theory - Continued *

by Aleksey Nogin

February 14, 2000

*
Embedded Ststems *

by Christoph Kreitz, Robert L. Constable

November 05, 2001

*
Empty Types *

by John Mitchell

September 25, 1986

*
Enabling Active Mathematical Documents in the National Science Digital Library *

by Robert L. Constable

March 31, 2003

*
Enhancing Proof Assistant Systems *

by Christoph Kreitz

February 25, 2002

*
Enhancing the search of mathematics & Hot topics in mathematical search *

by Lori Lorigo

May 03, 2004

*
Equality *

by Robert W. Harper

1984-1985

*
Event Systems: Introduction to the Logic of Events *

by Mark Bickford

February 17, 2006

*
Explaining the Formal Digital Library *

by Stuart F. Allen, Robert L. Constable, Richard Eaton

March 11, 2002

*
Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations *

by Matthew Fluet

November 24, 2003

*
Extracting Circuits from Constructive Proofs *
| cite »

by David A. Basin

1991

*
Extracting Readable and Efficient Programs from Nuprl Proofs *

by James L. Caldwell

November 18, 1997

*
Extraction *

by Judith Underwood

March 16, 1993

*
Extraction in IZF *

by Wojciech Moczydlowski

February 25, 2005

*
Extraction of Programs *

by Benjamin Werner

1993-1994

*
Fefprl *

by Douglas J. Howe, Douglas J. Howe

October 20, 1992

*
Fefprl *

by Douglas J. Howe, Douglas J. Howe

October 05, 1992

*
Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages *

by Chung-chieh Shan

December 02, 2011

*
Finding Computational Content from Classical Proofs *
| cite »

by Robert L. Constable, Chetan Murthy

1991

*
Finite Multi-Sets *

by Paul B. Jackson

August 19, 1999

*
Formal Abstract Data Types and Inheritance *

by Jason Hickey

October 31, 1995

*
Formal Continuations and Classical Logic *

by Karl Crary

March 10, 1997

*
Formal Methods & Distributed Systems *

by Mark Hayden

1996-1997

*
Formal Methods Program at NASA Langley Research Center *

by James L. Caldwell

February 07, 1995

*
Formal Models for Nuprl Evaluator *

by Aleksey Nogin

March 24, 1998

*
Formal Modules (Abstract Data Types) and Object Oriented Programming *

by Jason Hickey

1995-1996

*
Formal Reasoning about Communication Systems *

by Christoph Kreitz

1996-1997

*
Formalizing Hamiltonian Dynamics *

by Conal Mannion

November 09, 1993

*
Formalizing Program Synthesis *

by Arnd Poetzsch

April 27, 1993

*
Formally Verified Synthesis of Combinational Circuits *
| cite »

by David A. Basin, Geoffrey Brown, Miriam Leeser

1991

*
Foundations for the Implementation of Higher-Order Subtyping *

by Karl Crary

November 05, 1996

*
Foundations for the Implementation of Higher-Order Subtyping: Part II *

by Karl Crary

November 12, 1996

*
Foundations for the Management of Formal Mathematical Knowledge *

by Robert L. Constable

October 25, 2004

*
From System F to Typed Assembly Language *

by Karl Crary

September 16, 1997

*
GOLEM *

by Ettore Remidde

October 24, 1995

*
Graph Theory *

by Mark Bickford

May 14, 2003

*
Gröbner Basis *

by Thomas Yan

September 20, 1994

*
Group Communication with Functional Languages *

by Mark Hayden

January 28, 1997

*
Hilbert Basis Function *

by Thomas Yan

March 01, 1994

*
HOAS -- Higher Order Abstract Syntax: a Survey *

by Regina Barzilay

October 21, 2002

*
How Nuprl Reasons *

by Robert L. Constable

January 29, 2001

*
How to browse the library *

by Stuart F. Allen

December 14, 2004

*
How to Integrate Set Theory and Computation? *

by Scott D. Stoller

September 14, 1993

*
How to Strengthen the Notion of Obvious Step *

by Wilfred Z. Chen

October 22, 1991

*
Implementing Finite Sets *

by Walter Rance Cleaveland

September 09, 1986

*
Implementing the Logic of Events *

by Mark Bickford

February 24, 2003

*
Important Episodes in the History of Constructive Mathematics--including the frog and mouse wars *

by Robert L. Constable

March 01, 2004

*
Importing Isabelle Formal Mathematics into NuPRL *

by Pavel Naumov

March 08, 1999

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

by Lori Lorigo

2006

*
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs *

by Brigitte Pientka

May 05, 1998

*
Internalizing proofs and provability *

by Aleksey Nogin

February 19, 2001

*
Intersections, Unions and Games *

by Robert L. Constable, Alexei Kopylov, Aleksey Nogin

December 06, 1999

*
Introduction to Event Systems and the Logic of Distributed Systems *

by Mark Bickford, Robert L. Constable

September 16, 2002

*
Introduction to the Fall Seminar Series *

by Robert L. Constable

September 08, 2003

*
Intuitionistic ZF *

by Jim Lipton

January 30, 1990

*
IO-automata and Ensemble *

by Mark Bickford

February 21, 2000

*
iPRL: A General Approach to Interpreting Isabelle Results in NuPRL *

by Pavel Naumov

September 08, 1998

*
Is a type uniquely determined by its equivalence relation? *

by Aleksey Nogin

November 26, 2001

*
IZF and Recursive Realizability *

by Jim Lipton

March 05, 1987

*
Justifying the HOL-Nuprl Connection in the Categorical Framework of General Logics and Type Theory in a Membership Equational Logic Framework *

by Mark-Oliver Stehr

1998-1999

*
KML *

by Karl Crary

April 30, 1996

*
Knowledge-Based Proof Planning *

by Erica Melis

April 19, 1999

*
Kopylov and Nogin CSL Submission *

by Alexei Kopylov

April 02, 2001

*
Lambda Calculus as Basis for Programming Language Design *

by Robert W. Harper

1990-1991

*
Leader Election Protocols *

by Mark Bickford

October 06, 2003

*
Linear Logic *

by Alexei Kopylov

October 18, 1999

*
Listening to Theorem Provers who Talk to Each Other about Computer Systems *

by Robert L. Constable

October 20, 1998

*
Lists *

by Stuart F. Allen

May 15, 2001

*
Logic-Based Knowledge Representation *
| cite »

by Paul B. Jackson

1989

*
Logical Relations *

by Jim Lipton

March 06, 1990

*
M-L Type Theory, Categories, Inductive Types *

by Nax P. Mendler

1990 Summ

*
Marhew's Principle *

by Ryan Stansifer

1984-1985

*
Mark Presentation *

by Mark Bickford

November 29, 2004

*
Markov's Principle for Propositional Type Theory *

by Aleksey Nogin

August 20, 2001

*
Math Vernacular *

by N. G. deBruijn

November 17, 1987

*
Microsoft's Spec# *

by Christoph Kreitz

April 17, 2006

*
ML Execution *

by H. M. Bromley

1984-1985

*
ML-like Type Reconstruction for Nuprl *

by Ozan Hafizogullari

November 26, 1996

*
Modular approach to formalization of the quotient types *

by Aleksey Nogin

April 23, 2001

*
Modular approach to quotient and other types *

by Aleksey Nogin

April 16, 2001

*
Modules and Libraries *

by Jason Hickey

February 18, 1997

*
More on proof automation: Shostak's decision procedure and Nuprl *

by Mark Bickford

September 24, 2001

*
Motivation: Basis of a Set Theory for Nuprl *

by Todd Wilson

February 21, 1995

*
New modular approach to formalizing complex types in type theory *

by Aleksey Nogin

April 09, 2001

*
New Nuprl Editor *

by Stuart F. Allen

November 07, 1995

*
Non-existence of Unions *

by Evan Moran

March 04, 2005

*
Notation and Computer Aided Mathematics *

by Conal Mannion

December 06, 1994

*
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

*
Nuprl 3 vs. Nuprl 4 *

by Paul B. Jackson

November 05, 1991

*
NuPRL Demo *

by Mark Bickford

September 16, 2011

*
Nuprl Execution *

by H. M. Bromley

1984-1985

*
Nuprl Library Annotation *

by Amanda Holland-Minkley

April 05, 2004

*
Nuprl Tutorial *

by Jason Hickey

February 02, 1997

*
Objects *

by Alexei Kopylov

November 19, 2001

*
On continuity of computable real functions *

by Elena Nogina

May 01, 2000

*
On Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis *

by Uwe Egly

September 22, 1998

*
Operational Modal Logic *

by Sergei Artemov

January 29, 1996

*
Optimizing Ext *

by James T. Sasaki

1984-1985

*
Overview of Nuprl 5 *

by Stuart F. Allen

September 19, 1995

*
Partial Objects *

by Scott F. Smith

November 24, 1987

*
Partial Recursive Functions *

by Nax P. Mendler

1984-1985

*
Permutations vol. 1 *

by Paul B. Jackson

August 19, 1999

*
Permutations vol. 2 *

by Paul B. Jackson

August 19, 1999

*
Planning Session for Spring Seminar Series *

by Robert L. Constable

January 26, 2004

*
Plotkin *

by Jim Lipton

March 13, 1990

*
Points of Contact with Girard (Nuprl ∩ Ludics) *

by Robert L. Constable

September 13, 1999

*
Polya/Nuprl *

by Stuart F. Allen

1993-1994

*
Polymorphism Is Not Set Theoretic *

by Nax P. Mendler

February 14, 1990

*
PP-lambda in Nuprl *

by Nax P. Mendler

1984-1985

*
Predicate Calculus Model *

by Stuart F. Allen

1984-1985

*
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

*
Principles of Stepwise Refinement *

by Heiko Mantel

November 22, 1999

*
PRL Library Day *

by Stuart F. Allen

November 19, 1991

*
Processing video streams using event notification systems *

by Robert L. Constable, Mark Bickford

October 15, 2001

*
Program Development for Proof Transformations *

by Helmut Schwichtenberg

October 12, 1994

*
Programs as Specification *

by Rick Hehner

May 06, 1986

*
Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics *

by Stuart F. Allen, Robert L. Constable

December 03, 2001

*
Project Direction and Research Problems *

by Robert L. Constable

February 06, 1996

*
Prolog *

by Ryan Stansifer, Stuart F. Allen

1984-1985

*
Proof Automation in Constructive Type Theory *

by Christoph Kreitz

September 17, 2001

*
Proof Polynomials: Cut Elimination *

by Sergei Artemov

October 07, 1997

*
Proof presentation in the Omega system *

by Erica Melis

October 25, 1999

*
Proof Tools and Correct Program Development *

by Aarong Stump

February 03, 2003

*
Proofs by Structural Induction using Partial Evaluation *

by Julia Lawall

April 13, 1993

*
Properties of the Formal Digital Library *

by Robert L. Constable

May 06, 2002

*
PVS *

by N Shankar

March 24, 1992

*
Randomized Programming and Probabilistic Reasoning in Type Theory *

by James Cheney

April 17, 2000

*
Randomness and Free Choice Sequences *

by Robert L. Constable

February 04, 2005

*
Rational Reconstruction of Boyer and Moore Prover *

by Andrew Stevens

December 01, 1987

*
Reading BAAs and RFPs *

by Robert L. Constable

October 16, 2000

*
Reading BAAs and RFPs (cont.) *

by Robert L. Constable

October 23, 2000

*
Real-time Message Automata *

by Mark Bickford

February 11, 2005

*
Realizabiity for IZF *

by Jim Lipton

March 12, 1987

*
Reasoning about Java Classes in Nuprl *

by Pavel Naumov

September 09, 1997

*
Reasoning about Java Classes in Nuprl (continued) *

by Pavel Naumov

September 16, 1997

*
Reasoning about Scientific Programs *

by Conal Mannion, Stuart F. Allen

1993-1994

*
Recent Results on the PCES Project *

by Mark Bickford

April 01, 2002

*
Record calculus *

by Alexei Kopylov

November 12, 2001

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

by Nax P. Mendler

1987

*
Recursive Types in Coq *

by Christine Paulin-Mohring

September 08, 1994

*
Reflected Lambda Calculus *

by Sergei Artemov

October 02, 2000

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

by Fausto Giunchiglia, Alan Smaill

1989

*
Reflective PRL *

by Todd B. Knoblock

1984-1985

*
Regions, part 2: The Capability Calculus *

by David Walker

November 15, 1999

*
Remarks on Nijmegen trip *

by Robert L. Constable

November 08, 2004

*
Remarks on the FDL (Formal Digital Library) Project *

by Stuart F. Allen

November 17, 2003

*
Remarks on the FDL (Formal Digital Library) Project -- Continuation of talk begun November 17 *

by Stuart F. Allen

December 01, 2003

*
Report on the DARPA PCES PI meeting *

by Robert L. Constable, Lori Lorigo, Mark Bickford

October 29, 2001

*
Report on the Design of the Formal Digital Library *

by Richard Eaton, Robert L. Constable, Stuart F. Allen

April 08, 2002

*
Report on the Edinburgh Conference: 35 Years of Automath *

by Robert L. Constable

2001-2002

*
Representing Computational Complexity in Nuprl *

by Robert L. Constable

November 22, 1994

*
Representing Objects in Nuplr Type Theory *

by Alexei Kopylov

April 29, 2002

*
Representing Red-Black Trees in MetaPRL *

by Alexei Kopylov

March 10, 2003

*
Research Directions *

by Robert L. Constable

September 25, 2000

*
Reversing Howe's Substitution Rule *

by Evan Moran

September 27, 2004

*
Review of Theorem Provers Outside Cornell part 1 *

by Aleksey Nogin

February 11, 2002

*
Review of Theorem Provers Outside Cornell part 2 *

by Aleksey Nogin

February 18, 2002

*
Reviewing Nuprl *

by Robert L. Constable

March 09, 2012

*
Seminar History and Initial Planning Meeting *

by Robert L. Constable, Robert L. Constable

September 09, 2011

*
Separativeness and the Structure of the Singletons *

by Evan Moran

October 18, 2004

*
Set Models *

by Douglas J. Howe

November 03, 1992

*
Set-theoretical models of type theory *

by Wojciech Moczydlowski

September 13, 2004

*
Set-theoretical models of type theory (cont.) *

by Wojciech Moczydlowski

September 20, 2004

*
Sharing Formal Mathematics and Programming *

by Jason Hickey

1996-1997

*
Simple Consensus Algorithm *

by Robert L. Constable, Mark Bickford, Vincent Rahli

October 28, 2011

*
Simple, Efficient Object Encoding using Intersection Types *

by Karl Crary

April 14, 1998

*
Some Recent Results of R. Dyckhoff and A. Pitts *

by Todd Wilson

March 26, 1996

*
Some Uses of the Intersection Type *

by Stuart F. Allen, Robert L. Constable

May 03, 1999

*
Square-Root Verification *

by Jason Hickey

May 10, 1995

*
Stability of intuitionistic systems *

by Sergei Artemov

April 24, 2000

*
Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge *

by Robert L. Constable

October 27, 2003

*
Strong Normalization in Lambda ^{2} *

by Nax P. Mendler

October 02, 1986

*
Stronger Role for Recursive Types Needed for Logic of Events *

by Robert L. Constable

February 24, 2012

*
Structured Concurrent Programming *

by Jaydev Misra

September 15, 2006

*
Structuring Proofs *

by Douglas J. Howe, Paul B. Jackson

October 27, 1992

*
Summer Reports *

by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo

September 04, 2000

*
Summer Reports *

by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo

September 11, 2000

*
Summer Reports *

by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo

September 18, 2000

*
SupInf *

by Tobias Mayr

September 23, 1997

*
Syntactic Abstraction *

by Timothy G. Griffin

September 22, 1987

*
Tactic Trees in eXene *

by Roderick Moten

September 22, 1992

*
TBA *

by David A. Basin, David McAllister, Wilfred Z. Chen

April 08, 1988

*
TBA *

by David A. Basin, David McAllister, Wilfred Z. Chen

October 13, 1987

*
TBA *

by David A. Basin, David McAllister, Wilfred Z. Chen

May 04, 1993

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

by Wojciech Moczydlowski, Alfons Geser

2005

*
The "Interface" Version of Nuprl *

by Stuart F. Allen, Richard Eaton

November 15, 1994

*
The Abstract Term Type *

by Regina Barzilay

March 04, 2002

*
The Calculemus Autumn School *

by Christoph Kreitz, Sabina Petride, Matthew Fluet

October 28, 2002

*
The Engineering Aspects of Proof-Environment Design *

by Chetan Murthy

January 24, 1995

*
The Enigma of Sat Hill Climbing Procedures *

by Ian Gent

November 10, 1992

*
The Expressiveness of lambda Y *

by David A. Basin

April 09, 1987

*
The Lambda Calculus as a Basis for Language Design *

by Robert W. Harper

1989-1990

*
The Logic of Events and Event Structure Patterns *

by Mark Bickford

April 26, 2004

*
The MathBus Term Structure *

by Richard Zippel

1995-1996

*
The MIZAR Project *

by Paul B. Jackson

February 15, 1994

*
The Nuprl 5 Library *

by Richard Eaton

February 09, 1998

*
The Nuprl Proof Development System *
| cite »

by Christian Horn

1988

*
The ONTIC System *

by David McAllister

October 06, 1987

*
The Refiner as the Inference Mechanism of Nuprl Proof Development System *

by Roderick Moten

April 04, 1995

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

by Judith Underwood

1993

*
The Ultimate Programming Machine *

by Jason Hickey

October 25, 1994

*
The Ultimate Programming Machine II: Very Dependent Types *

by Jason Hickey

November 08, 1994

*
Theorem Proving with Real Numbers *

by Robert L. Constable

August 31, 1993

*
Theory of Reals *

by Douglas J. Howe

1984-1985

*
Thesis *

by Douglas J. Howe

1984-1985

*
TLA *

by Scott D. Stoller, Chetan Murthy

November 01, 1994

*
Trip Report *

by Aleksey Nogin

October 22, 2001

*
Type Inference *

by Robert W. Harper

1984-1985

*
Type Methodology for Modern Languages and Compilers *

by Karl Crary

February 24, 1998

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

by Robert L. Constable

1991

*
Type Theory as a Legacy from Logicism *

by Stuart F. Allen

March 08, 2004

*
Typed Assembly Language *

by Neal Glew

March 01, 1999

*
Typed Enumeration-Free External Setting for Computing Theory *

by Robert L. Constable

November 03, 1987

*
Uniform Inhabitants for the Non-Union Blueprints, continued *

by Evan Moran

October 28, 2005

*
Unions and Unboxed Quotients *

by Evan Moran

September 23, 2005

*
Universally Closed Classes *

by Robert L. Constable

1984-1985

*
Urelements in Computational Type Theory *

by Mark Bickford

November 11, 2005

*
Urelements in Type Theory: New Definition of "Inherence" *

by Mark Bickford

November 18, 2005

*
Uri Abraham's Models for Concurrency *

by Robert L. Constable, Sabina Petride

January 27, 2003

*
Using Lemmas *

by Timothy G. Griffin

1984-1985

*
Using Nuprl as a Formal Assistant for Preparing Largely Informal Material *

by Stuart F. Allen

March 29, 1999

*
Using Nuprl to Verify Floating Point Hardware *

by Paul B. Jackson

April 17, 1990

*
Validating a methodology for natural language generation *

by Amanda Holland-Minkley

March 05, 2001

*
Variations on a Proof by Smullyan *

by Matthew Fluet

May 05, 2003

*
Verbalization of High-Level Formal Proofs *

by Amanda Holland-Minkley

February 01, 1999

*
Verified Implementation of Red-Black Trees *

by Alexei Kopylov

November 10, 2003

*
Verifying a Pipelined Circuit *

by Mark Aagaard

April 05, 1994

*
Verifying an Implementation of a Polynomial Algebra ADT *

by Paul B. Jackson

November 29, 1994

*
Verifying Garbage Collection Algorithms using the PVS Theorem Prover *

by Paul B. Jackson

May 07, 1997

*
Verifying the Four Colour Theorem *

by Georges Gonthier

May 20, 2005

*
Very Dependent Function Space *

by Jason Hickey

1994-1995

*
Work in Progress: A Formalization of the SUP-INF Algorithm *

by Todd Wilson

July 11, 1996

*
Zeno *

by Pavel Naumov

January 25, 2002