Knowledge Base of
Publications, Seminars, & Math Library

List by Title

690 results

---

(Constructive) set-theoretic semantics for (Constructive) higher-order logic
by Wojciech Moczydlowski
November 04, 2005

(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

20BJ as a Meta-logical Framework
by Andrew Stevens
April 21, 1990

A (Possibly) New Scheme for Libraries/Proof-Contexts
by Chetan Murthy
September 03, 1993

A Basis for Constructive, Reflexive Type Theory
by William Aitken
October 01, 1990

A Causal Logic of Events in Formalized Computational Type Theory | cite »
by Mark Bickford, Robert L. Constable
2005

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

A Computational Analysis of Girard's Translation and LC | cite »
by Chetan Murthy
1992

A Constructive Completeness Proof for Intuitionistic Predicate Calculus
by Judith Underwood
February 01, 1994

A Constructive Completeness Proof for the Intuitionistic Propositional Calculus | cite »
by Judith Underwood
1990

A Constructive Programming Logic
by Robert L. Constable
August 08, 1977

A Constructive Proof of Higman's Lemma | cite »
by Chetan Murthy, James R. Russell
1990

A Conversation with Moshe Vardi
by Moshe Vardi
November 18, 2011

A Dependent Set Theory
by Wojciech Moczydlowski
2007

A Discussion in Consensus
by Jason Wu
February 10, 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

A Fast Algorithm for the Integer Square Root
by Anne Trostle, Mark Bickford
June 09, 2014

A Formal Exploration of Constructive Geometry
by Sarah Sernaker, Robert L. Constable
2016

A Formal Exploration of Constructive Geometry
by Robert L. Constable, Sarah Sernaker
2016

A Formal Framework for Modeling Memory
by Victor Luchangco
February 22, 1999

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 Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS | cite »
by Robert L. Constable, James Donahue
July 01, 1979

A Linguistic View of Constuctive Type Theory
by Amanda Holland-Minkley
February 02, 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 Methodology for Designing Asynchronous Circuits
by Rajit Manohar
May 10, 1999

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 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 Environment for the Development of Group Communication Systems | cite »
by Christoph Kreitz, Mark Hayden, Jason Hickey
1998

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 for Abstract Atoms in Nuprl
by Stuart F. Allen
March 31, 2006

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 annotation scheme for Nuprl | cite »
by Douglas J. Howe
October 01, 1998

A Type Theoretic Interpretation of Doug Howe's Squiggle Relation
by Stuart F. Allen
April 19, 1988

A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014

A Type Theory with Partial Equivalence Relations as Types
by Vincent Rahli
September 10, 2014

A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems | cite »
by Christoph Kreitz, Stephan Schmitt
2000

A Uniform Rippling Approach for Instantiating Free Variables
by Brigitte Pientka
December 02, 1997

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

Abstact Data Structures, Objects and Classes in the Nuprl Type Theory
by Alexei Kopylov
November 11, 2002

Abstract Identifiers and Textual Reference | cite »
by Stuart F. Allen
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 Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping | cite »
by Stuart F. Allen
2004

Abstract Programming in Nuprl
by Jason Hickey
November 23, 1993

ACL2 Tutorial
by Mark Reitblatt
March 27, 2014

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

Adding Intersection Types to Doug Howe's Classical Set-Theoretic Semantics
by Evan Moran
April 07, 1998

Adding Shared Memory to the General Process Model
by Jason Wu
April 20, 2012

Advancing the Type-Theoretic Underpinnings of Practical Programming Languages
by Karl Crary
1996-1997

An Abstract Semantics for Atoms in Nuprl | cite »
by Stuart F. Allen
2006

An ACL2 Demo
by J Strother Moore
October 07, 2002

An Algorithm for the Greatest Common Divisor
by Anne Trostle
October 01, 2013

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 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 Extension of OCaml's Type Theory
by Robert L. Constable
October 23, 2013

An Introduction to Event Systems
by Robert L. Constable
September 29, 2003

An Introduction to Region Inference
by David Walker
November 08, 1999

An Intuitionistic Formalization of The Elements of Euclid Book I
by Ariel Kellison, Mark Bickford
November 26, 2019

An Object-Oriented Approach to Verifying Group Communication Systems | cite »
by Mark Bickford, Jason Hickey
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 | cite »
by Douglas J. Howe, Scott D. Stoller
1994

An Operational Approach to Combining Classical Set Theory and Functional Programming Languages
by Scott D. Stoller
March 29, 1994

Analysis of reflection in programming languages using Scheme as the main example
by Eli Barzilay
March 06, 2000

Analyzing Access Control Logics Using Evidence Semantics
by Robert L. Constable
September 23, 2011

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

Arithmetic module for MetaPRL: rules and Arith tactic
by Yegor Bryukhov
March 25, 2002

Arithpac
by Timothy G. Griffin
1984-1985

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

Attaching Context to Objects in the Library
by Stuart F. Allen
February 04, 1992

Automated Complexity Analysis
by Ralph Benzinger
September 15, 1998

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 Higher-Order Complexity Analysis
by Ralph Benzinger
February 05, 2001

Automated Proof of Authentication Protocols in a Logic of Events | cite »
by Mark Bickford
2010

Automated Proofs in Event Logic
by Mark Bickford
September 16, 2005

Automated Reasoning in Category Theory
by Robert L. Constable
October 04, 2004

Automated Reasoning in Herbrand Structures
by Liron Cohen, Reuben Rowe, Yoni Zohar
June 03, 2019

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 FDL Projections
by Richard Eaton
September 01, 2006

Automatic generation of texts from Nuprl proofs
by Amanda Holland-Minkley
February 04, 2002

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

Automating Reasoning in an Implementation of Constructive Type Theory | cite »
by Douglas J. Howe
1988

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

Bar Induction: The Good, the Bad, and the Ugly | cite »
by Vincent Rahli, Mark Bickford, Robert L. Constable
April 11, 2017

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

Brouwer's Fan Theorem: An Overview
by Crystal Cheung
2015

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

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

Chain Replication Protocol
by Mark Bickford
September 27, 2006

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

Classical Propositional Decidability via Nuprl Proof Extraction | cite »
by James L. Caldwell
1998

Classical Propositional Logic
by James L. Caldwell
July 28, 2004

Classical Tools for Constructive Proof Search | cite »
by James L. Caldwell, Judith Underwood
1996

Coinduction in Coq
by Abhishek Anand
November 12, 2014

Collaborative Mathematics Environments
by Robert L. Constable
November 21, 1996

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

Component Specification Using Event Classes | cite »
by Mark Bickford
2009

Computability Beyond Church-Turing using Choice Sequences | cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018

Computability is Ineffable in ZF Set Theory
by Robert L. Constable
April 01, 1997

Computational Complexity and Induction for Partial Computable Functions in Type Theory | cite »
by Robert L. Constable, Karl Crary
2002

Computational Content of Math
by Douglas Bridges
October 19, 1993

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

Computer Algebra, Theorem Proving, and Types
by Todd Wilson
October 04, 1994

Computer Science at the Frontiers of Mathematics
by Robert L. Constable
January 15, 2020

Concurrent Refinement in Nuprl | cite »
by Roderick Moten
1997

Connectedness of the Continuum in Intuitionistic Mathematics | cite »
by Mark Bickford
2018

Connecting Formal Semantics to Constructive Intuitions
by Michael J. O'Donnell
July 06, 1993

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 Algorithms in Nuprl
by Douglas J. Howe
December 01, 1992

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 Factorization Theory
by Paul B. Jackson
August 19, 1999

Constructive General Algebra
by Paul B. Jackson
August 19, 1999

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 Proofs and Program Extraction
by Christoph Kreitz
February 23, 2004

Constructive Reading of Classical Logic
by Robert L. Constable, Sarah Sernaker
2015

Constructive Topology - A Theory of Observation
by Francisco Mota
October 15, 2014

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

Continuation on reflection
by Mark Bickford
March 13, 2000

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

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

Cubical type theory with several universes in Nuprl
by Mark Bickford
May 20, 2020

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

Dead Code Elimination
by Ozan Hafizogullari, Christoph Kreitz
January 27, 1998

DEC
by Rustan Leino
November 19, 1996

Decidability Extracted: Synthesizing | cite »
by James L. Caldwell
1998

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

Denotational Semantics
by Nax P. Mendler
1984-1985

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

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

Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014

Developing Set Theory in HOL
by Paul B. Jackson
February 28, 1995

Differences between the MetaPRL type theory and the Nuprl type theory
by Aleksey Nogin
April 10, 2000

Discrete Math Materials
by Stuart F. Allen
August 02, 2004

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

DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics
by Mark Bickford
February 18, 2020

Editing
by Stuart F. Allen
November 16, 1993

Editor Demonstration
by Paul B. Jackson
March 09, 1993

Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP | cite »
by Robert L. Constable
2008

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

Elementary Number Theory
by Stuart F. Allen
September 23, 2003

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

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 Proof Assistant Systems
by Christoph Kreitz
February 25, 2002

Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra | cite »
by Paul B. Jackson
1995

Enhancing the search of mathematics & Hot topics in mathematical search
by Lori Lorigo
May 03, 2004

Equality
by Robert W. Harper
1984-1985

Equality in Lazy Computation Systems | cite »
by Douglas J. Howe
1989

Event Systems
by Mark Bickford
November 08, 2003

Event Systems: Introduction to the Logic of Events
by Mark Bickford
February 17, 2006

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

Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995 | cite »
by Robert L. Constable
1995

Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002

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 and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations
by Matthew Fluet
November 24, 2003

Expressing Computational Complexity in Constructive Type Theory | cite »
by Robert L. Constable
1995

Extracting Circuits from Constructive Proofs | cite »
by David A. Basin
1991

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 Readable and Efficient Programs from Nuprl Proofs
by James L. Caldwell
November 18, 1997

Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus | cite »
by Wojciech Moczydlowski, Robert L. Constable
2007

Extraction
by Judith Underwood
March 16, 1993

Extraction in IZF
by Wojciech Moczydlowski
February 25, 2005

Extraction of Programs
by Benjamin Werner
1993-1994

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

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

Finding the Maximum Segment Sum
by Anne Trostle
January 22, 2014

Finite Automata
by Robert L. Constable
May 16, 2001

Finite Multi-Sets
by Paul B. Jackson
August 19, 1999

Formal Abstract Data Types and Inheritance
by Jason Hickey
October 31, 1995

Formal Compiler Implementation in a Logical Framework | cite »
by Jason Hickey, Aleksey Nogin
2003

Formal Continuations and Classical Logic
by Karl Crary
March 10, 1997

Formal Domain Theory
by Neal Glew
December 05, 1995

Formal Foundations of Computer Security | cite »
by Mark Bickford, Robert L. Constable
2008

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 Module Systems and Nuprl-Light: A Programmer's Perspective
by Jason Hickey
February 13, 1996

Formal Modules (Abstract Data Types) and Object Oriented Programming
by Jason Hickey
1995-1996

Formal Objects in Type Theory
by Jason Hickey
1996-1997

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
by Christoph Kreitz
1996-1997

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

Formalization of Cubical Type Theory in Nuprl
by Mark Bickford
January 15, 2020

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 Category Theory and Presheaf Models of Type Theory in Nuprl | cite »
by Mark Bickford
2018

Formalizing chain replication
by Mark Bickford, David Guaspari
2006

Formalizing Constructive Analysis in Nuprl
by Mark Bickford
September 04, 2012

Formalizing Constructive Real Analysis | cite »
by Max B. Forester
1993

Formalizing Hamiltonian Dynamics
by Conal Mannion
November 09, 1993

Formalizing Moessner's Theorem in Nuprl
by Mark Bickford, Dexter Kozen, Alexandra Silva
June 08, 2012

Formalizing Program Synthesis
by Arnd Poetzsch
April 27, 1993

Formalizing Reference Types in Nuprl | cite »
by Pavel Naumov
1998

Formalizing the Theory Concept in Nuprl
by Jason Hickey
March 15, 1994

Formalizing the Theory Mechanism in NuPRL
by Jason Hickey
March 15, 1994

Formally Verified Synthesis of Combinational Circuits | cite »
by David A. Basin, Geoffrey Brown, Miriam Leeser
1991

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

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

From System F to Typed Assembly Language
by Karl Crary
September 16, 1997

Fundamental Theorem of Arithmetic
by Stuart F. Allen
August 02, 2004

General Automata Theory
by Mark Bickford
January 25, 2003

Generating Event Logics with Higher-Order Processes as Realizers | cite »
by Mark Bickford, Robert L. Constable, David Guaspari
2010

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

HOL Translation (partial)
by Douglas J. Howe
February 13, 2004

HOL Workshop
by Mark Aagaard
September 15, 1992

HORUS Verification Effort
by Jason Hickey
1995-1996

How far can we go with Induction-Recursion?
by Abhishek Anand, Vincent Rahli
November 20, 2013

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

Hybrid Protocols
by Mark Bickford
February 20, 2002

Imperative Program Semantics
by Stuart F. Allen
May 02, 1995

Implementing Euclid's Straightedge and Compass Constructions in Type Theory | cite »
by Ariel Kellison, Mark Bickford, Robert L. Constable
2018

Implementing Finite Sets
by Walter Rance Cleaveland
September 09, 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

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

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 HOL Theorems into Nuprl
by Douglas J. Howe
July 30, 1998

Importing Isabelle Formal Mathematics into NuPRL
by Pavel Naumov
March 08, 1999

Importing Mathematics from HOL into Nuprl | cite »
by Douglas J. Howe
1996

Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012

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 Management in the Service of Knowledge and Discovery | cite »
by Lori Lorigo
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

Instantiation of Existentially Quantified Variables in Inductive Specification Proofs | cite »
by Brigitte Pientka, Christoph Kreitz
1998

Instantiation of Existentially Quantified Variables in Inductive Specification Proofs
by Brigitte Pientka
May 05, 1998

Intensional Polymorphism in Type-Erasure Semantics
by Stephanie Weirich
April 28, 1998

Interfacing with Proof Assistants for Domain Specific Programming Using EventML | cite »
by Vincent Rahli
July 11, 2012

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 Classic ML | cite »
by Christoph Kreitz, Vincent Rahli
2011

Introduction to Event Systems and the Logic of Distributed Systems
by Mark Bickford, Robert L. Constable
September 16, 2002

Introduction to EventML
by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
February 03, 2012

Introduction to the Fall Seminar Series
by Robert L. Constable
September 08, 2003

Introduction to the Fall Seminar Series
by Robert L. Constable
September 07, 2012

Intuitionism - The Philosophy of L. E. J. Brouwer
by Dirk Schlimm
April 24, 1998

Intuitionistic Ancestral Logic
by Liron Cohen, Robert L. Constable
October 10, 2015

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

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

Intuitionistic Tableau Extracted | cite »
by James L. Caldwell
1999

Intuitionistic ZF
by Jim Lipton
January 30, 1990

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

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

Isabelle Tutorial
by Steffen Smolka
March 18, 2014

Issues in Constructive Type Theory
by Ross Tate
September 14, 2012

Iterated Binary Operations
by Stuart F. Allen
August 02, 2004

IZF and Recursive Realizability
by Jim Lipton
March 05, 1987

JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants | cite »
by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
2001

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

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

Kopylov and Nogin CSL Submission
by Alexei Kopylov
April 02, 2001

L. E. J. Brouwer's Intuitionism: A Revolution in Two Installments
by Dirk van Dalen
June 26, 1998

Lambda Calculus as Basis for Programming Language Design
by Robert W. Harper
1990-1991

Latest results about reflection (TENTATIVE)
by Eli Barzilay
November 20, 2000

Leader Election Protocols
by Mark Bickford
October 06, 2003

Lectures on: Classical Proofs as Programs | cite »
by Robert L. Constable
1992

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, Construction, Computation | cite »
by Ulrich Berger
July 29, 2012

Logic-Based Knowledge Representation | cite »
by Paul B. Jackson
1989

Logical Aspects of Digital Mathematics Libraries (extended abstract) | cite »
by Stuart F. Allen, James L. Caldwell, Robert L. Constable
2001

Logical Investigations, with the Nuprl Proof Assistant
by Robert L. Constable, Anne Trostle
July 22, 2014

Logical Programming Environments
by Jason Hickey
March 03, 1998

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 | cite »
by Alexei Kopylov, Aleksey Nogin
2001

Markov's Principle for Propositional Type Theory
by Aleksey Nogin
August 20, 2001

Math Vernacular
by N. G. deBruijn
November 17, 1987

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

Mechanizing the Proof of Correction of a Compiler Using Type Theory
by Yves Bertot
November 17, 1998

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

Metamathematics of Reflection
by Todd B. Knoblock
April 22, 1987

MetaPRL -- A Modular Logical Environment | cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003

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

Moving Proofs-as-Programs into Practice | cite »
by James L. Caldwell
1997

Naive Computational Type Theory | cite »
by Robert L. Constable
2002

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

Next Generation Proof Technology
by Robert L. Constable
December 27, 2012

Nominal Type Theory
by Mark Bickford, Vincent Rahli
October 29, 2014

Non-existence of Unions
by Evan Moran
March 04, 2005

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

Notation and Computer Aided Mathematics
by Conal Mannion
December 06, 1994

Notational Definition and Top-down Refinement for Interactive Proof Development Systems | cite »
by Timothy G. Griffin
1988

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 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 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 Demo
by Mark Bickford
September 16, 2011

Nuprl Editor and Interface
by Stuart F. Allen
September 23, 2003

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

Nuprl's Class Theory and Its Applications | cite »
by Robert L. Constable, Jason Hickey
2000

Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997

Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997

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

Objects
by Alexei Kopylov
November 19, 2001

On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer | cite »
by Robert L. Constable
June 29, 2012

On computational open-endedness in Martin-Lof's type theory
by Douglas J. Howe
July 15, 1991

On continuity of computable real functions
by Elena Nogina
May 01, 2000

On Howe's Importation of HOL into Nuprl
by Evan Moran
September 29, 1998

On Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis
by Uwe Egly
September 22, 1998

On Modeling Ensemble
by Robert L. Constable, Jason Hickey
October 27, 1998

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

Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020

Operational Modal Logic
by Sergei Artemov
January 29, 1996

Optimizing Ext
by James T. Sasaki
1984-1985

Order-theoretic Differences Between Two Variants of Type Theory
by Evan Moran
October 19, 2012

Overview of Nuprl 5
by Stuart F. Allen
September 19, 1995

Partial Objects
by Scott F. Smith
November 24, 1987

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

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 Proof Content for Communicating Induction | cite »
by Amanda Holland-Minkley
2002

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

Polymorphic Logic | cite »
by Mark Bickford, Robert L. Constable
July 29, 2012

Polymorphism Is Not Set Theoretic
by Nax P. Mendler
February 14, 1990

PP-lambda in Nuprl
by Nax P. Mendler
1984-1985

Practical Reflection in Nuprl | cite »
by Eli Barzilay, Stuart F. Allen, Robert L. Constable
2003

Practical Uses of Quotations, Macros and Reflection
by Eli Barzilay
April 05, 1999

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

Presenting Semantics for a Fragment of the Java Programming Language in Nuprl Proof Development System
by Pavel Naumov
March 10, 1998

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

Program Optimization in Type Theory
by Brent Knight
October 18, 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

Project Overview
by Robert L. Constable
July 01, 1993

Prolog
by Ryan Stansifer, Stuart F. Allen
1984-1985

Proof Assistants and the Dynamic Nature of Formal Theories | 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

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 as Process
by Robert L. Constable
2012

Proofs as Programs | cite »
by Joseph L. Bates, Robert L. Constable
1985

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

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

PVS
by N Shankar
March 24, 1992

Quotation and Reflection in Nuprl and Scheme | cite »
by Eli Barzilay
2001

Quotient Types in Nuprl
by Mark Bickford
November 13, 2013

Quotient Types: A Modular Approach | cite »
by Aleksey Nogin
2002

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

Readability Exercise (num theory)
by Stuart F. Allen
December 14, 2004

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

Realizing Bar Induction in Nuprl
by Mark Bickford
October 26, 2012

Reasoning About Functional Programs in Nuprl | cite »
by Douglas J. Howe
1993

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 in Type Theory and Their Relationship to Automath | cite »
by Robert L. Constable
2003

Recent Results on the PCES Project
by Mark Bickford
April 01, 2002

Recent work with Coq
by Mark Reitblatt
May 11, 2012

Record calculus
by Alexei Kopylov
November 12, 2001

Recursive Definitions in Type Theory | cite »
by Robert L. Constable, Nax P. Mendler
1985

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

References in Type Theory
by Pavel Naumov
November 25, 1997

Reflected Lambda Calculus
by Sergei Artemov
October 02, 2000

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

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 Constructive and Non-Constructive Automated Reasoning | cite »
by Fausto Giunchiglia, Alan Smaill
1989

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

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

Reversal-Bounded Computations | cite »
by Tat-hung Chan
1980

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

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

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
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 Evidence | cite »
by Robert L. Constable
1985

Semantics of the Nuprl Type Theory
by Scott D. Stoller
March 16, 1993

Seminar History and Initial Planning Meeting
by Robert L. Constable
September 09, 2011

Seminar History and Initial Planning Meeting
by Robert L. Constable, Robert L. Constable
September 09, 2011

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

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

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 Imperative Programming
by Pavel Naumov
February 26, 2002

Simple, Efficient Object Encoding using Intersection Types
by Karl Crary
April 14, 1998

Some Normalization Properties of Martin-Lof's Type Theory and Applications | cite »
by David A. Basin, Douglas J. Howe
1991

Some Recent Results in MetaPRL
by Eric Klavins
April 22, 2002

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

Specifications and Proofs for Ensemble Layers | cite »
by Jason Hickey, Nancy Lynch, Robbert van Renesse
1999

Speeding Up the MetaPRL Refiner
by Aleksey Nogin
February 08, 1999

Square Root of 2 is Irrational
by Stuart F. Allen
August 04, 2004

Square-Root Verification
by Jason Hickey
May 10, 1995

Stability of intuitionistic systems
by Sergei Artemov
April 24, 2000

Standard Resources
by Stuart F. Allen
September 23, 2003

Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge
by Robert L. Constable
October 27, 2003

Strong Normalization in Lambda²
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

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 Trees in eXene
by Roderick Moten
September 22, 1992

Tactic-Based Theorem Proving and Knowledge-Based Forward Chaining: An Experiment with Nuprl and Ontic | cite »
by Wilfred Z. Chen
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

Term Model Semantics and Tait Computability Method
by Scott F. Smith
March 11, 1987

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 Beauty of Nuprl's Uniform Term Representation and How to Reason about those Terms in Coq
by Abhishek Anand
October 09, 2013

The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002

The Computational Behaviour of Girard's Paradox | cite »
by Douglas J. Howe
1987

The Continuum
by Robert L. Constable
February 26, 2020

The Current Projects of the MetaPRL Group
by Aleksey Nogin, Jason Hickey
April 26, 1999

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 Ensemble System | cite »
by Mark Hayden
1998

The Expressiveness of lambda Y
by David A. Basin
April 09, 1987

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 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 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 MathBus Term Structure
by Richard Zippel
1995-1996

The MetaPRL Logical Programming Environment | cite »
by Jason Hickey
2001

The MIZAR Project
by Paul B. Jackson
February 15, 1994

The Nuprl 5 Library
by Richard Eaton
February 09, 1998

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 | cite »
by Christian Horn
1988

The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide | cite »
by Paul B. Jackson
1996

The ONTIC System
by David McAllister
October 06, 1987

The Oyster-Clam System | cite »
by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill
1990

The power of bar induction in constructive type theory
by Mark Bickford
September 25, 2013

The Refiner as the Inference Mechanism of Nuprl Proof Development System
by Roderick Moten
April 04, 1995

The Semantics of Reflected Proof | cite »
by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken
1990

The Status of the Meta-Prl Project
by Aleksey Nogin
October 04, 1999

The Structure of Nuprl's Type Theory | cite »
by Robert L. Constable
1997

The Tableau Algorithm for Intuitionistic Propositional Calculus as a Constructive Completeness Proof | cite »
by Judith Underwood
1993

The Triumph of Types: Principia Mathematica's Impact on Computer Science | cite »
by Robert L. Constable
2010

The Type Base and Undecidability in Type Theory
by Abhishek Anand
September 21, 2012

The Ultimate Programming Machine
by Jason Hickey
October 25, 1994

The Ultimate Programming Machine II: Very Dependent Types
by Jason Hickey
November 08, 1994

The Value of Automated Deduction | cite »
by Robert L. Constable
1996

Theorem Proving with Real Numbers
by Robert L. Constable
August 31, 1993

Theory of Reals
by Douglas J. Howe
1984-1985

There Are No Discontinuous Real Functions
by Mark Bickford, Vincent Rahli
October 08, 2014

Thesis
by Douglas J. Howe
1984-1985

TLA
by Scott D. Stoller, Chetan Murthy
November 01, 1994

Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 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

Towers of Hanoi
by Stuart F. Allen
April 27, 2004

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

Transforming the Academy: Knowledge Formation in the Age of Digital Information
by Robert L. Constable
January 11, 2007

Trip Report
by Aleksey Nogin
October 22, 2001

Turing Machine Basics
by Pavel Naumov
November 01, 1996

Type Inference
by Robert W. Harper
1984-1985

Type Methodology for Modern Languages and Compilers
by Karl Crary
February 24, 1998

Type Theoretic Semantics for First-Order Logic
by Robert L. Constable
May 24, 2012

Type Theoretical Foundations for Data Structures, Classes, and Objects | cite »
by Alexei Kopylov
2004

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

Type-Theoretic Methodology for Practical Programming Languages | cite »
by Karl Crary
1998

Type-Theoretic Models of Concurrency | cite »
by Walter Rance Cleaveland
1987

Typed Assembly Language
by Neal Glew
March 01, 1999

Typed Enumeration-Free External Setting for Computing Theory
by Robert L. Constable
November 03, 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

Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent | cite »
by Liron Cohen, Reuben Rowe
July 01, 2018

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 Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts | cite »
by Stuart F. Allen, Robert L. Constable, Lori Lorigo
2006

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 for the Verification and Synthesis of Hardware | cite »
by Miriam Leeser
1992

Using Nuprl to Verify Floating Point Hardware
by Paul B. Jackson
April 17, 1990

Using Reflection to Explain and Enhance Type Theory | cite »
by Robert L. Constable
1994

Using Reflection to External Automated Theorem Provers
by Mark Aagaard
March 30, 1993

Validating a methodology for natural language generation
by Amanda Holland-Minkley
March 05, 2001

Validating Brouwer’s Continuity Principle for Numbers Using Named Exceptions | cite »
by Vincent Rahli, Mark Bickford
January 02, 2018

Variations on a Proof by Smullyan
by Matthew Fluet
May 05, 2003

Verbalization of High-Level Formal Proofs | cite »
by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable
1999

Verbalization of High-Level Formal Proofs
by Amanda Holland-Minkley
February 01, 1999

Verification of Combinational Logic in Nuprl | cite »
by David A. Basin, Peter Del Vecchio
1989

Verified Implementation of Red-Black Trees
by Alexei Kopylov
November 10, 2003

Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification | cite »
by Mark Aagaard, Miriam Leeser
1993

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 HORUS in Nuprl
by Jason Hickey
November 28, 1995

Verifying the Four Colour Theorem
by Georges Gonthier
May 20, 2005

Very Dependent Function Space
by Jason Hickey
1994-1995

Virtual Evidence: A Constructive Semantics for Classical Logics
by Robert L. Constable
2014

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

Work in Progress: A Formalization of the SUP-INF Algorithm
by Todd Wilson
July 11, 1996

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

Zeno
by Pavel Naumov
January 25, 2002