Knowledge Base of
Publications,
Seminars,
& 
Math Library
PhD theses from the project are accessible at the NCSTRL web site.
List by Year
690 results
2020
Cubical type theory with several universes in Nuprl
by Mark Bickford
May 20, 2020
The Continuum
by Robert L. Constable
February 26, 2020
DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics
by Mark Bickford
February 18, 2020
Intuitionistic Mathematics and Logic
by Joan Rand Moschovakis, Garyfallia Vafeiadou
January 25, 2020
Intuitionistic Mathematics and Logic
by Joan Rand Moschovakis, Garyfallia Vafeiadou
January 25, 2020
Computer Science at the Frontiers of Mathematics
by Robert L. Constable
January 15, 2020
Formalization of Cubical Type Theory in Nuprl
by Mark Bickford
January 15, 2020
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020
2019
An Intuitionistic Formalization of The Elements of Euclid Book I
by Ariel Kellison, Mark Bickford
November 26, 2019
Automated Reasoning in Herbrand Structures
by Liron Cohen, Reuben Rowe, Yoni Zohar
June 03, 2019
Bar Induction is Compatible with Constructive Type Theory
| cite »
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
2019
2018
A Verified Theorem Prover Backend Supported by a Monotonic Library
| cite »
by Vincent Rahli, Liron Cohen, Mark Bickford
November 01, 2018
Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
| cite »
by Liron Cohen, Reuben Rowe
July 01, 2018
Validating Brouwer’s Continuity Principle for Numbers Using Named Exceptions
| cite »
by Vincent Rahli, Mark Bickford
January 02, 2018
Computability Beyond Church-Turing using Choice Sequences
| cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018
Connectedness of the Continuum in Intuitionistic Mathematics
| cite »
by Mark Bickford
2018
Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl
| cite »
by Mark Bickford
2018
Implementing Euclid's Straightedge and Compass Constructions in Type Theory
| cite »
by Ariel Kellison, Mark Bickford, Robert L. Constable
2018
2017
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems
| cite »
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
November 15, 2017
Bar Induction: The Good, the Bad, and the Ugly
| cite »
by Vincent Rahli, Mark Bickford, Robert L. Constable
April 11, 2017
2016
Constructive Analysis and Experimental Mathematics using the Nuprl Proof Assistant
by Mark Bickford
March 02, 2016
A Nominal Exploration of Intuitionism
by Vincent Rahli, Mark Bickford
January 18, 2016
A Formal Exploration of Constructive Geometry
by Sarah Sernaker, Robert L. Constable
2016
A Formal Exploration of Constructive Geometry
by Robert L. Constable, Sarah Sernaker
2016
2015
Intuitionistic Ancestral Logic
by Liron Cohen, Robert L. Constable
October 10, 2015
Coq as a Metatheory for Nuprl with Bar Induction
by Vincent Rahli, Mark Bickford
September 14, 2015
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
September 01, 2015
Nuprl’s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
September 01, 2015
Brouwer's Fan Theorem: An Overview
by Crystal Cheung
2015
Constructive Reading of Classical Logic
by Robert L. Constable, Sarah Sernaker
2015
2014
Synthetic Topology in NuPRL
by Francisco Mota, Mark Bickford
December 03, 2014
From Replicated Databases to Ensembles of Collaborating Robots
by Abhishek Anand, Mark Bickford
November 19, 2014
Coinduction in Coq
by Abhishek Anand
November 12, 2014
Nominal Type Theory
by Mark Bickford, Vincent Rahli
October 29, 2014
Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014
Constructive Topology - A Theory of Observation
by Francisco Mota
October 15, 2014
There Are No Discontinuous Real Functions
by Mark Bickford, Vincent Rahli
October 08, 2014
Synthesizing Protocols using the Logic of Events and EventML
by Robert L. Constable, Mark Bickford
September 17, 2014
A Type Theory with Partial Equivalence Relations as Types
by Vincent Rahli
September 10, 2014
Logical Investigations, with the Nuprl Proof Assistant
by Robert L. Constable, Anne Trostle
July 22, 2014
A Generic Approach to Proofs about Substitution
by Abhishek Anand, Vincent Rahli
July 17, 2014
Towards a Formally Verified Proof Assistant
by Abhishek Anand, Vincent Rahli
July 14, 2014
Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014
A Fast Algorithm for the Integer Square Root
by Anne Trostle, Mark Bickford
June 09, 2014
A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014
Inductive Construction in Nuprl Type Theory Using Bar Induction
by Mark Bickford, Robert L. Constable
May 12, 2014
Formalizing Bishop's Constructive Analysis in Constructive Type Theory
by Mark Bickford, Robert L. Constable
April 10, 2014
ACL2 Tutorial
by Mark Reitblatt
March 27, 2014
Isabelle Tutorial
by Steffen Smolka
March 18, 2014
Finding the Maximum Segment Sum
by Anne Trostle
January 22, 2014
Intuitionistic Completeness of First-Order Logic
| cite »
by Robert L. Constable, Mark Bickford
January 01, 2014
Virtual Evidence: A Constructive Semantics for Classical Logics
by Robert L. Constable
2014
2013
How far can we go with Induction-Recursion?
by Abhishek Anand, Vincent Rahli
November 20, 2013
Quotient Types in Nuprl
by Mark Bickford
November 13, 2013
Nuprl as a Programming Assistant
by Robert L. Constable
November 06, 2013
A verified proof assistant
by Vincent Rahli, Abhishek Anand
October 30, 2013
An Extension of OCaml's Type Theory
by Robert L. Constable
October 23, 2013
The Beauty of Nuprl's Uniform Term Representation and How to Reason about those Terms in Coq
by Abhishek Anand
October 09, 2013
An Algorithm for the Greatest Common Divisor
by Anne Trostle
October 01, 2013
The power of bar induction in constructive type theory
by Mark Bickford
September 25, 2013
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
| cite »
by Vincent Rahli, Mark Bickford, Abhishek Anand
April 22, 2013
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
March 31, 2013
The Logic of Information Flow and the Foundations of Distributed Computing
by Robert L. Constable
January 10, 2013
2012
Next Generation Proof Technology
by Robert L. Constable
December 27, 2012
Byzantine Chain Replication
| cite »
by Robbert van Renesse, Chi Ho, Nicolas Schiper
December 20, 2012
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
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
Realizing Bar Induction in Nuprl
by Mark Bickford
October 26, 2012
Order-theoretic Differences Between Two Variants of Type Theory
by Evan Moran
October 19, 2012
Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012
ShadowDB: A Replicated Database on a Synthesized Consensus Core
| cite »
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
October 07, 2012
Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012
The Type Base and Undecidability in Type Theory
by Abhishek Anand
September 21, 2012
Issues in Constructive Type Theory
by Ross Tate
September 14, 2012
Introduction to the Fall Seminar Series
by Robert L. Constable
September 07, 2012
Formalizing Constructive Analysis in Nuprl
by Mark Bickford
September 04, 2012
Logic, Construction, Computation
| cite »
by Ulrich Berger
July 29, 2012
Polymorphic Logic
| cite »
by Mark Bickford, Robert L. Constable
July 29, 2012
Intuitionistic Ancestral Logic
by Liron Cohen
July 12, 2012
Interfacing with Proof Assistants for Domain Specific Programming Using EventML
| cite »
by Vincent Rahli
July 11, 2012
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer
| cite »
by Robert L. Constable
June 29, 2012
Proof Assistants and the Dynamic Nature of Formal Theories
| cite »
by Robert L. Constable
June 29, 2012
Formalizing Moessner's Theorem in Nuprl
by Mark Bickford, Dexter Kozen, Alexandra Silva
June 08, 2012
Type Theoretic Semantics for First-Order Logic
by Robert L. Constable
May 24, 2012
Nuprl as Logical Framework for Automating Proofs in Category
| cite »
by Christoph Kreitz
April 26, 2012
Proof Assistants and the Rise of Type Theory Circa 1912-2012
by Robert L. Constable
March 19, 2012
Work in Progress
by Richard Eaton
February 20, 2012
Introduction to EventML
by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
February 03, 2012
Proofs as Process
by Robert L. Constable
2012
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory
| cite »
by Robert L. Constable, Fairouz Kamareddine, Twan Laan
2012
The Logic of Events, a framework to reason about distributed systems
| cite »
by Mark Bickford, Vincent Rahli, Robert L. Constable
2012
2011-2012
Recent work with Coq
by Mark Reitblatt
May 11, 2012
Adding Communication Primitives to the Nuprl Evaluator
by Mark Bickford
May 04, 2012
Adding Shared Memory to the General Process Model
by Jason Wu
April 20, 2012
Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012
Reviewing Nuprl
by Robert L. Constable
March 09, 2012
Stronger Role for Recursive Types Needed for Logic of Events
by Robert L. Constable
February 24, 2012
A Discussion in Consensus
by Jason Wu
February 10, 2012
Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
by Chung-chieh Shan
December 02, 2011
A Conversation with Moshe Vardi
by Moshe Vardi
November 18, 2011
Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011
Analyzing Access Control Logics Using Evidence Semantics
by Robert L. Constable
September 23, 2011
NuPRL Demo
by Mark Bickford
September 16, 2011
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
2011
Intuitionistic Completeness of First-Order Logic
| cite »
by Robert L. Constable, Mark Bickford
October 07, 2011
Introduction to Classic ML
| cite »
by Christoph Kreitz, Vincent Rahli
2011
Investigations in intersection types:Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method
| cite »
by Vincent Rahli
2011
2010
Automated Proof of Authentication Protocols in a Logic of Events
| cite »
by Mark Bickford
2010
Encoding Pi Calculus
| cite »
by David Guaspari
2010
Generating Event Logics with Higher-Order Processes as Realizers
| cite »
by Mark Bickford, Robert L. Constable, David Guaspari
2010
Investigating Correct-by-Construction Attack-Tolerant Systems
| cite »
by Robert L. Constable, Mark Bickford, Robbert van Renesse
2010
The Triumph of Types: Principia Mathematica's Impact on Computer Science
| cite »
by Robert L. Constable
2010
2009
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
| cite »
by Robert L. Constable
2009
Component Specification Using Event Classes
| cite »
by Mark Bickford
2009
2008
Computational Type Theory -- Extended Version
| cite »
by Robert L. Constable
2008
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP
| cite »
by Robert L. Constable
2008
Formal Foundations of Computer Security
| cite »
by Mark Bickford, Robert L. Constable
2008
Unguessable Atoms: A Logical Foundation for Security
| cite »
by Mark Bickford
2008
2007
Transforming the Academy: Knowledge Formation in the Age of Digital Information
by Robert L. Constable
January 11, 2007
A Dependent Set Theory
by Wojciech Moczydlowski
2007
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus
| cite »
by Wojciech Moczydlowski, Robert L. Constable
2007
2006-2007
Structured Concurrent Programming
by Jaydev Misra
September 15, 2006
2006
Chain Replication Protocol
by Mark Bickford
September 27, 2006
Automatic FDL Projections
by Richard Eaton
September 01, 2006
A Normalizing Intuitionistic Set Theory with Inaccessible Sets
| cite »
by Wojciech Moczydlowski
2006
An Abstract Semantics for Atoms in Nuprl
| cite »
by Stuart F. Allen
2006
Automating Proofs in Category Theory
| cite »
by Dexter Kozen, Christoph Kreitz, Eva Richter
2006
Enabling Large Scale Coherency Among Mathematical Texts
| cite »
by Stuart F. Allen, Robert L. Constable
2006
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
| cite »
by Robert L. Constable, Wojciech Moczydlowski
2006
Formalizing chain replication
by Mark Bickford, David Guaspari
2006
Implementing Reflection in Nuprl
| cite »
by Eli Barzilay
2006
Information-Intensive Proof Technology
| cite »
by Robert L. Constable
2006
Innovations in Computational Type Theory using Nuprl
| cite »
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, Evan Moran
2006
Normalization of intuitionistic set theories.
| cite »
by Wojciech Moczydlowski
2006
Unguessable Atoms: A Logical Foundation for Security
| cite »
by Mark Bickford
2006
Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts
| cite »
by Stuart F. Allen, Robert L. Constable, Lori Lorigo
2006
Information Management in the Service of Knowledge and Discovery
| cite »
by Lori Lorigo
2006
2005-2006
Microsoft's Spec#
by Christoph Kreitz
April 17, 2006
A Semantics for Abstract Atoms in Nuprl
by Stuart F. Allen
March 31, 2006
Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
March 23, 2006
Event Systems: Introduction to the Logic of Events
by Mark Bickford
February 17, 2006
Urelements in Type Theory: New Definition of "Inherence"
by Mark Bickford
November 18, 2005
Unions and Unboxed Quotients
by Evan Moran
September 23, 2005
Automated Proofs in Event Logic
by Mark Bickford
September 16, 2005
Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
August 26, 2005
2005
A Causal Logic of Events in Formalized Computational Type Theory
| cite »
by Mark Bickford, Robert L. Constable
2005
Knowledge-based synthesis of distributed systems using event structures
| cite »
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2005
A Programming Logic for Distributed Systems
| cite »
by Mark Bickford, David Guaspari
2005
Termination of Single-Threaded One-rule Semi-Thue Systems
| cite »
by Wojciech Moczydlowski, Alfons Geser
2005
2004-2005
Urelements in Computational Type Theory
by Mark Bickford
November 11, 2005
(Constructive) set-theoretic semantics for (Constructive) higher-order logic
by Wojciech Moczydlowski
November 04, 2005
Uniform Inhabitants for the Non-Union Blueprints, continued
by Evan Moran
October 28, 2005
(Re-)Introduction to Howe's Framework, continued
by Evan Moran
October 14, 2005
(Re-)Introduction to Howe's Framework
by Evan Moran
September 30, 2005
Verifying the Four Colour Theorem
by Georges Gonthier
May 20, 2005
Anchoring Expository Text in Formal Mathematics -- Part II
by Stuart F. Allen
April 15, 2005
Non-existence of Unions
by Evan Moran
March 04, 2005
Extraction in IZF
by Wojciech Moczydlowski
February 25, 2005
Real-time Message Automata
by Mark Bickford
February 11, 2005
Randomness and Free Choice Sequences
by Robert L. Constable
February 04, 2005
Anchoring Expository Text in Formal Mathematics
by Stuart F. Allen
December 06, 2004
Mark Presentation
by Mark Bickford
November 29, 2004
Remarks on Nijmegen trip
by Robert L. Constable
November 08, 2004
Foundations for the Management of Formal Mathematical Knowledge
by Robert L. Constable
October 25, 2004
Separativeness and the Structure of the Singletons
by Evan Moran
October 18, 2004
Automated Reasoning in Category Theory
by Robert L. Constable
October 04, 2004
Reversing Howe's Substitution Rule
by Evan Moran
September 27, 2004
Set-theoretical models of type theory (cont.)
by Wojciech Moczydlowski
September 20, 2004
Set-theoretical models of type theory
by Wojciech Moczydlowski
September 13, 2004
2004 Summ
Coq and Nuprl
by Wojciech Moczydlowski
July 27, 2004
2004
How to browse the library
by Stuart F. Allen
December 14, 2004
Readability Exercise (num theory)
by Stuart F. Allen
December 14, 2004
Russel's Paradox
by Stuart F. Allen
December 14, 2004
Square Root of 2 is Irrational
by Stuart F. Allen
August 04, 2004
Discrete Math Materials
by Stuart F. Allen
August 02, 2004
Fundamental Theorem of Arithmetic
by Stuart F. Allen
August 02, 2004
Iterated Binary Operations
by Stuart F. Allen
August 02, 2004
Classical Propositional Logic
by James L. Caldwell
July 28, 2004
Towers of Hanoi
by Stuart F. Allen
April 27, 2004
HOL Translation (partial)
by Douglas J. Howe
February 13, 2004
A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.
| cite »
by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable
2004
Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping
| cite »
by Stuart F. Allen
2004
Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations
| cite »
by Stuart F. Allen, Robert L. Constable, Matthew Fluet
2004
Knowledge-Based Synthesis of Distributed Systems Using Event Structures
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2004
Type Theoretical Foundations for Data Structures, Classes, and Objects
| cite »
by Alexei Kopylov
2004
2003-2004
Enhancing the search of mathematics & Hot topics in mathematical search
by Lori Lorigo
May 03, 2004
The Logic of Events and Event Structure Patterns
by Mark Bickford
April 26, 2004
CFZ From Below (continued)
by Evan Moran
April 19, 2004
CFZ From Below
by Evan Moran
April 12, 2004
Nuprl Library Annotation
by Amanda Holland-Minkley
April 05, 2004
Type Theory as a Legacy from Logicism
by Stuart F. Allen
March 08, 2004
Important Episodes in the History of Constructive Mathematics--including the frog and mouse wars
by Robert L. Constable
March 01, 2004
Constructive Proofs and Program Extraction
by Christoph Kreitz
February 23, 2004
Comparing Aspects of Set Theory and Type Theory
by Robert L. Constable
February 16, 2004
Applied Logic as Part of an Effort to Accumulate Precise Knowledge
by Stuart F. Allen
February 09, 2004
A Linguistic View of Constuctive Type Theory
by Amanda Holland-Minkley
February 02, 2004
Planning Session for Spring Seminar Series
by Robert L. Constable
January 26, 2004
Adapting Proofs-as-Programs for the Synthesis of Imperative SML Programs
by Iman Poernomo
December 08, 2003
Remarks on the FDL (Formal Digital Library) Project -- Continuation of talk begun November 17
by Stuart F. Allen
December 01, 2003
Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations
by Matthew Fluet
November 24, 2003
Remarks on the FDL (Formal Digital Library) Project
by Stuart F. Allen
November 17, 2003
Verified Implementation of Red-Black Trees
by Alexei Kopylov
November 10, 2003
Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge
by Robert L. Constable
October 27, 2003
Leader Election Protocols
by Mark Bickford
October 06, 2003
An Introduction to Event Systems
by Robert L. Constable
September 29, 2003
Discussion of Methods of Sharing Formal Mathematics
by Evan Moran
September 22, 2003
Bridges Between Set Theory and Type Theory
by Evan Moran
September 15, 2003
Introduction to the Fall Seminar Series
by Robert L. Constable
September 08, 2003
2003
Event Systems
by Mark Bickford
November 08, 2003
Elementary Number Theory
by Stuart F. Allen
September 23, 2003
Nuprl Editor and Interface
by Stuart F. Allen
September 23, 2003
Standard Resources
by Stuart F. Allen
September 23, 2003
Nuprl Basics
by Stuart F. Allen
September 18, 2003
Graph Theory
by Mark Bickford
May 14, 2003
General Automata Theory
by Mark Bickford
January 25, 2003
A Logic of Events
| cite »
by Mark Bickford, Robert L. Constable
2003
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics
| cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003
Dependent Intersection: A New Way of Defining Records in Type Theory
| cite »
by Alexei Kopylov
2003
Formal Compiler Implementation in a Logical Framework
| cite »
by Jason Hickey, Aleksey Nogin
2003
MetaPRL -- A Modular Logical Environment
| cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003
Practical Reflection in Nuprl
| cite »
by Eli Barzilay, Stuart F. Allen, Robert L. Constable
2003
Recent Results in Type Theory and Their Relationship to Automath
| cite »
by Robert L. Constable
2003
The FDL Navigator: Browsing and Manipulating Formal Content
| cite »
by Christoph Kreitz
2003
2002-2003
Variations on a Proof by Smullyan
by Matthew Fluet
May 05, 2003
Continuing Discussion of the NSDL
by Robert L. Constable
April 14, 2003
Enabling Active Mathematical Documents in the National Science Digital Library
by Robert L. Constable
March 31, 2003
A Reconfigurable Atomic Memory Service for Dynamic Networks
by Alex Shvartsman
March 24, 2003
Representing Red-Black Trees in MetaPRL
by Alexei Kopylov
March 10, 2003
Online Demonstration of Syntactic Reflection. Realizing an Argument about Syntax (Tarski).
by Regina Barzilay
March 03, 2003
Implementing the Logic of Events
by Mark Bickford
February 24, 2003
Distributed Snapshot Algorithms
by Keshav Pingali
February 17, 2003
Proof Tools and Correct Program Development
by Aarong Stump
February 03, 2003
Uri Abraham's Models for Concurrency
by Robert L. Constable, Sabina Petride
January 27, 2003
Continuing Discussion of Objects
by Alexei Kopylov, Robert L. Constable
December 02, 2002
Classes and Objects
by Robert L. Constable
November 25, 2002
Continuing on Objects and Classes
by Alexei Kopylov
November 18, 2002
Abstact Data Structures, Objects and Classes in the Nuprl Type Theory
by Alexei Kopylov
November 11, 2002
The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002
HOAS -- Higher Order Abstract Syntax: a Survey
by Regina Barzilay
October 21, 2002
An ACL2 Demo
by J Strother Moore
October 07, 2002
Application of Event Systems and the Logic of Distributed Systems to Leader Election
by Mark Bickford
September 30, 2002
Introduction to Event Systems and the Logic of Distributed Systems
by Mark Bickford, Robert L. Constable
September 16, 2002
2002
Simple Imperative Programming
by Pavel Naumov
February 26, 2002
Hybrid Protocols
by Mark Bickford
February 20, 2002
Bar-Type Rules
by Karl Crary
January 25, 2002
Zeno
by Pavel Naumov
January 25, 2002
Abstract Identifiers and Textual Reference
| cite »
by Stuart F. Allen
2002
Computational Complexity and Induction for Partial Computable Functions in Type Theory
| cite »
by Robert L. Constable, Karl Crary
2002
FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002
Naive Computational Type Theory
| cite »
by Robert L. Constable
2002
Planning Proof Content for Communicating Induction
| cite »
by Amanda Holland-Minkley
2002
Quotient Types: A Modular Approach
| cite »
by Aleksey Nogin
2002
Reflecting Higher-Order Abstract Syntax in Nuprl
| cite »
by Eli Barzilay, Stuart F. Allen
2002
2001-2002
Properties of the Formal Digital Library
by Robert L. Constable
May 06, 2002
Representing Objects in Nuplr Type Theory
by Alexei Kopylov
April 29, 2002
Some Recent Results in MetaPRL
by Eric Klavins
April 22, 2002
Report on the Design of the Formal Digital Library
by Richard Eaton, Robert L. Constable, Stuart F. Allen
April 08, 2002
Recent Results on the PCES Project
by Mark Bickford
April 01, 2002
Arithmetic module for MetaPRL: rules and Arith tactic
by Yegor Bryukhov
March 25, 2002
Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002
The Abstract Term Type
by Regina Barzilay
March 04, 2002
Enhancing Proof Assistant Systems
by Christoph Kreitz
February 25, 2002
Review of Theorem Provers Outside Cornell part 2
by Aleksey Nogin
February 18, 2002
Review of Theorem Provers Outside Cornell part 1
by Aleksey Nogin
February 11, 2002
Automatic generation of texts from Nuprl proofs
by Amanda Holland-Minkley
February 04, 2002
A Proof-Theoretic Approach to Knowledge Acquisition"
by Dexter Kozen
January 28, 2002
Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics
by Stuart F. Allen, Robert L. Constable
December 03, 2001
Is a type uniquely determined by its equivalence relation?
by Aleksey Nogin
November 26, 2001
Objects
by Alexei Kopylov
November 19, 2001
Record calculus
by Alexei Kopylov
November 12, 2001
Embedded Ststems
by Christoph Kreitz, Robert L. Constable
November 05, 2001
Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001
Trip Report
by Aleksey Nogin
October 22, 2001
Processing video streams using event notification systems
by Robert L. Constable, Mark Bickford
October 15, 2001
More on proof automation: Shostak's decision procedure and Nuprl
by Mark Bickford
September 24, 2001
Proof Automation in Constructive Type Theory
by Christoph Kreitz
September 17, 2001
Markov's Principle for Propositional Type Theory
by Aleksey Nogin
August 20, 2001
Report on the Edinburgh Conference: 35 Years of Automath
by Robert L. Constable
2001-2002
2001
Finite Automata
by Robert L. Constable
May 16, 2001
Lists
by Stuart F. Allen
May 15, 2001
An Experiment in Formal Design Using Meta-Properties
| cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable
2001
Automated Complexity Analysis of Nuprl Extracted Programs
| cite »
by Ralph Benzinger
2001
Automated Computational Complexity Analysis
| cite »
by Ralph Benzinger
2001
Connection-Driven Inductive Theorem Proving
| cite »
by Christoph Kreitz, Brigitte Pientka
2001
Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment
| cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse
2001
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants
| cite »
by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
2001
Logical Aspects of Digital Mathematics Libraries (extended abstract)
| cite »
by Stuart F. Allen, James L. Caldwell, Robert L. Constable
2001
Markov's Principle For Propositional Type Theory
| cite »
by Alexei Kopylov, Aleksey Nogin
2001
Protocol Switching: Exploiting Meta-Properties
| cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001
Proving Hybrid Protocols Correct
| cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
2001
Quotation and Reflection in Nuprl and Scheme
| cite »
by Eli Barzilay
2001
The MetaPRL Logical Programming Environment
| cite »
by Jason Hickey
2001
Writing Constructive Proofs Yielding Efficient Extracted Programs
| cite »
by Aleksey Nogin
2001
2000-2001
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
New modular approach to formalizing complex types in type theory
by Aleksey Nogin
April 09, 2001
Kopylov and Nogin CSL Submission
by Alexei Kopylov
April 02, 2001
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
Validating a methodology for natural language generation
by Amanda Holland-Minkley
March 05, 2001
Internalizing proofs and provability
by Aleksey Nogin
February 19, 2001
Reflection in First-Order Logic
by Eli Barzilay
February 12, 2001
Automated Higher-Order Complexity Analysis
by Ralph Benzinger
February 05, 2001
How Nuprl Reasons
by Robert L. Constable
January 29, 2001
A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory (cont)
by Aleksey Nogin, Alexei Kopylov
December 04, 2000
A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory
by Alexei Kopylov, Aleksey Nogin
November 27, 2000
Latest results about reflection (TENTATIVE)
by Eli Barzilay
November 20, 2000
Discussing the issues surrounding our library of formal algorithmic mathematics
by Robert L. Constable
November 13, 2000
Caltech Computer Science
by Jason Hickey
November 06, 2000
Reading BAAs and RFPs (cont.)
by Robert L. Constable
October 23, 2000
Reading BAAs and RFPs
by Robert L. Constable
October 16, 2000
Reflected Lambda Calculus
by Sergei Artemov
October 02, 2000
Research Directions
by Robert L. Constable
September 25, 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
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 04, 2000
2000
A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems
| cite »
by Christoph Kreitz, Stephan Schmitt
2000
Fast Tactic-Based Theorem Proving
| cite »
by Jason Hickey, Aleksey Nogin
2000
Matrix-Based Constructive Theorem Proving
| cite »
by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka
2000
Matrix-Based Inductive Theorem Proving
| cite »
by Christoph Kreitz, Brigitte Pientka
2000
Nuprl's Class Theory and Its Applications
| cite »
by Robert L. Constable, Jason Hickey
2000
Search Algorithms in Type Theory
| cite »
by James L. Caldwell, Ian Gent, Judith Underwood
2000
The Horus and Ensemble Projects: Accomplishments and Limitations
| cite »
by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels
2000
The Nuprl Open Logical Environment
| cite »
by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2000
1999-2000
An Efficient Refiner for First-order Intuitionistic Logic (Part II)
by Stephan Schmitt
May 22, 2000
On continuity of computable real functions
by Elena Nogina
May 01, 2000
Stability of intuitionistic systems
by Sergei Artemov
April 24, 2000
Randomized Programming and Probabilistic Reasoning in Type Theory
by James Cheney
April 17, 2000
Differences between the MetaPRL type theory and the Nuprl type theory
by Aleksey Nogin
April 10, 2000
Reflection Part II
by Eli Barzilay
April 03, 2000
Continuation on reflection
by Mark Bickford
March 13, 2000
Analysis of reflection in programming languages using Scheme as the main example
by Eli Barzilay
March 06, 2000
An Efficient Refiner for First-order Intuitionistic Logic
by Stephan Schmitt
February 28, 2000
IO-automata and Ensemble
by Mark Bickford
February 21, 2000
Efficient Programming by Extract in Nuprl Type Theory - Continued
by Aleksey Nogin
February 14, 2000
Efficient Programming by Extract in Nuprl Type Theory
by Aleksey Nogin
February 07, 2000
Automatic Complexity Analysis Revisited
by Ralph Benzinger
January 31, 2000
Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999
Principles of Stepwise Refinement
by Heiko Mantel
November 22, 1999
Regions, part 2: The Capability Calculus
by David Walker
November 15, 1999
An Introduction to Region Inference
by David Walker
November 08, 1999
Decidability of Linear Affine Logic
by Alexei Kopylov
November 01, 1999
Proof presentation in the Omega system
by Erica Melis
October 25, 1999
Linear Logic
by Alexei Kopylov
October 18, 1999
The Status of the Meta-Prl Project
by Aleksey Nogin
October 04, 1999
Continuation of talk on Polymorphic References
by Ozan Hafizogullari
September 24, 1999
Points of Contact with Girard (Nuprl ∩ Ludics)
by Robert L. Constable
September 13, 1999
1999
Constructive Factorization Theory
by Paul B. Jackson
August 19, 1999
Constructive General Algebra
by Paul B. Jackson
August 19, 1999
Finite Multi-Sets
by Paul B. Jackson
August 19, 1999
Permutations vol. 1
by Paul B. Jackson
August 19, 1999
Permutations vol. 2
by Paul B. Jackson
August 19, 1999
An Object-Oriented Approach to Verifying Group Communication Systems
| cite »
by Mark Bickford, Jason Hickey
1999
Automated Fast-Track Reconfiguration of Group Communication Systems
| cite »
by Christoph Kreitz
1999
Automating Inductive Specification Proofs
| cite »
by Brigitte Pientka, Christoph Kreitz
1999
Building Reliable, High-Performance Communication Systems from Components
| cite »
by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable
1999
Connection-Based Theorem Proving in Classical and Non-Classical Logics
| cite »
by Christoph Kreitz, Jens Otten
1999
Dependence Analysis Through Type Inference
| cite »
by Ozan Hafizogullari, Christoph Kreitz
1999
Fault-Tolerant Distributed Theorem Proving
| cite »
by Jason Hickey
1999
Intuitionistic Tableau Extracted
| cite »
by James L. Caldwell
1999
Metalogical Frameworks II: Developing a Reflected Decision Procedure
| cite »
by William Aitken, Robert L. Constable, Judith Underwood
1999
Specifications and Proofs for Ensemble Layers
| cite »
by Jason Hickey, Nancy Lynch, Robbert van Renesse
1999
Verbalization of High-Level Formal Proofs
| cite »
by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable
1999
1998-1999
A Methodology for Designing Asynchronous Circuits
by Rajit Manohar
May 10, 1999
Some Uses of the Intersection Type
by Stuart F. Allen, Robert L. Constable
May 03, 1999
The Current Projects of the MetaPRL Group
by Aleksey Nogin, Jason Hickey
April 26, 1999
Knowledge-Based Proof Planning
by Erica Melis
April 19, 1999
Practical Uses of Quotations, Macros and Reflection
by Eli Barzilay
April 05, 1999
Using Nuprl as a Formal Assistant for Preparing Largely Informal Material
by Stuart F. Allen
March 29, 1999
Importing Isabelle Formal Mathematics into NuPRL
by Pavel Naumov
March 08, 1999
Typed Assembly Language
by Neal Glew
March 01, 1999
A Formal Framework for Modeling Memory
by Victor Luchangco
February 22, 1999
A Programming Environment for Building Reliable High Performance Systems
by Jason Hickey
February 15, 1999
Speeding Up the MetaPRL Refiner
by Aleksey Nogin
February 08, 1999
Verbalization of High-Level Formal Proofs
by Amanda Holland-Minkley
February 01, 1999
Semantics and Pragmatics of Reflected Proof
by Stuart F. Allen, Sergei Artemov, Robert L. Constable
December 01, 1998
On the Reflection Mechanism in Nuprl
by Sergei Artemov
November 24, 1998
Mechanizing the Proof of Correction of a Compiler Using Type Theory
by Yves Bertot
November 17, 1998
Reflection Mechanisms in Nuprl
by Stuart F. Allen, Robert L. Constable
November 10, 1998
Automatic Debugging Through Type Inference, Continued
by Ozan Hafizogullari
November 03, 1998
On Modeling Ensemble
by Robert L. Constable, Jason Hickey
October 27, 1998
Listening to Theorem Provers who Talk to Each Other about Computer Systems
by Robert L. Constable
October 20, 1998
Automatic Debugging Through Type Inference
by Ozan Hafizogullari
October 06, 1998
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
Automated Complexity Analysis
by Ralph Benzinger
September 15, 1998
iPRL: A General Approach to Interpreting Isabelle Results in NuPRL
by Pavel Naumov
September 08, 1998
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
1998 Summ
Importing HOL Theorems into Nuprl
by Douglas J. Howe
July 30, 1998
L. E. J. Brouwer's Intuitionism: A Revolution in Two Installments
by Dirk van Dalen
June 26, 1998
Efficient Automated Proof Search and Proof Reconstruction in Intuitionistic Logic
by Jens Otten, Stephan Schmitt
June 23, 1998
1998
A type annotation scheme for Nuprl
| cite »
by Douglas J. Howe
October 01, 1998
A Matrix Characterization for MELL
| cite »
by Heiko Mantel, Christoph Kreitz
1998
A Proof Environment for the Development of Group Communication Systems
| cite »
by Christoph Kreitz, Mark Hayden, Jason Hickey
1998
Classical Propositional Decidability via Nuprl Proof Extraction
| cite »
by James L. Caldwell
1998
Decidability Extracted: Synthesizing
| cite »
by James L. Caldwell
1998
Formal Reasoning About Communication Systems II: Automated Fast-Track Reconfiguration
| cite »
by Christoph Kreitz
1998
Formalizing Reference Types in Nuprl
| cite »
by Pavel Naumov
1998
From dy/dx to []P: A Matter of Notation
| cite »
by Stuart F. Allen
1998
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs
| cite »
by Brigitte Pientka, Christoph Kreitz
1998
The Ensemble System
| cite »
by Mark Hayden
1998
Type-Theoretic Methodology for Practical Programming Languages
| cite »
by Karl Crary
1998
1997-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
Intuitionism - The Philosophy of L. E. J. Brouwer
by Dirk Schlimm
April 24, 1998
Simple, Efficient Object Encoding using Intersection Types
by Karl Crary
April 14, 1998
Adding Intersection Types to Doug Howe's Classical Set-Theoretic Semantics
by Evan Moran
April 07, 1998
Application of Notational Methods in dy/dx
by Stuart F. Allen
March 31, 1998
Formal Models for Nuprl Evaluator
by Aleksey Nogin
March 24, 1998
Presenting Semantics for a Fragment of the Java Programming Language in Nuprl Proof Development System
by Pavel Naumov
March 10, 1998
Logical Programming Environments
by Jason Hickey
March 03, 1998
Type Methodology for Modern Languages and Compilers
by Karl Crary
February 24, 1998
The Nuprl 5 Library
by Richard Eaton
February 09, 1998
Dead Code Elimination
by Ozan Hafizogullari, Christoph Kreitz
January 27, 1998
A Uniform Rippling Approach for Instantiating Free Variables
by Brigitte Pientka
December 02, 1997
References in Type Theory
by Pavel Naumov
November 25, 1997
Extracting Readable and Efficient Programs from Nuprl Proofs
by James L. Caldwell
November 18, 1997
Abstract Identifiers in Nuprl 5 (continued)
by Stuart F. Allen
October 28, 1997
Abstract Identifiers in Nuprl 5
by Stuart F. Allen
October 21, 1997
Proof Polynomials: Cut Elimination
by Sergei Artemov
October 07, 1997
SupInf
by Tobias Mayr
September 23, 1997
From System F to Typed Assembly Language
by Karl Crary
September 16, 1997
Reasoning about Java Classes in Nuprl (continued)
by Pavel Naumov
September 16, 1997
Reasoning about Java Classes in Nuprl
by Pavel Naumov
September 09, 1997
1997
Concurrent Refinement in Nuprl
| cite »
by Roderick Moten
1997
Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extracted Program
| cite »
by James L. Caldwell
1997
Formal Reasoning About Communication Systems I: Embedding ML in Type Theory
| cite »
by Christoph Kreitz
1997
Foundations for the Implementation of Higher-Order Subtyping
| cite »
by Karl Crary
1997
Moving Proofs-as-Programs into Practice
| cite »
by James L. Caldwell
1997
Nuprl-Light: An Implementation Framework for Higher-Order Logics
| cite »
by Jason Hickey
1997
The Structure of Nuprl's Type Theory
| cite »
by Robert L. Constable
1997
A Semantics of Objects in Type Theory
| cite »
by Jason Hickey
1997
1996-1997
Verifying Garbage Collection Algorithms using the PVS Theorem Prover
by Paul B. Jackson
May 07, 1997
CZF, Type Theory, and Nuprl-Light (continued)
by Evan Moran
April 08, 1997
Computability is Ineffable in ZF Set Theory
by Robert L. Constable
April 01, 1997
CZF, Type Theory, and Nuprl-Light
by Evan Moran
April 01, 1997
Formal Continuations and Classical Logic
by Karl Crary
March 10, 1997
Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997
Designing a Logical Library
by Stuart F. Allen
February 24, 1997
Modules and Libraries
by Jason Hickey
February 18, 1997
Nuprl Tutorial
by Jason Hickey
February 02, 1997
Group Communication with Functional Languages
by Mark Hayden
January 28, 1997
ML-like Type Reconstruction for Nuprl
by Ozan Hafizogullari
November 26, 1996
DEC
by Rustan Leino
November 19, 1996
Foundations for the Implementation of Higher-Order Subtyping: Part II
by Karl Crary
November 12, 1996
Foundations for the Implementation of Higher-Order Subtyping
by Karl Crary
November 05, 1996
Advancing the Type-Theoretic Underpinnings of Practical Programming Languages
by Karl Crary
1996-1997
Formal Methods & Distributed Systems
by Mark Hayden
1996-1997
Formal Objects in Type Theory
by Jason Hickey
1996-1997
Formal Reasoning about Communication Systems
by Christoph Kreitz
1996-1997
Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997
Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997
Sharing Formal Mathematics and Programming
by Jason Hickey
1996-1997
1996 Summ
Work in Progress: A Formalization of the SUP-INF Algorithm
by Todd Wilson
July 11, 1996
1996
Collaborative Mathematics Environments
by Robert L. Constable
November 21, 1996
Turing Machine Basics
by Pavel Naumov
November 01, 1996
Classical Tools for Constructive Proof Search
| cite »
by James L. Caldwell, Judith Underwood
1996
Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing
| cite »
by Robert L. Constable
1996
Formal Objects in Type Theory Using Very Dependent Types
| cite »
by Jason Hickey
1996
Formalizing Automata II: Decidable Properties
| cite »
by Robert L. Constable, Pavel Naumov
1996
Formalizing Automata Theory I: Finite Automata
| cite »
by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe
1996
Importing Mathematics from HOL into Nuprl
| cite »
by Douglas J. Howe
1996
Semantic Foundations for Embedding HOL in Nuprl
| cite »
by Douglas J. Howe
1996
The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide
| cite »
by Paul B. Jackson
1996
The Value of Automated Deduction
| cite »
by Robert L. Constable
1996
Collaborative Mathematics Environments
| cite »
by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel
1996
1995-1996
KML
by Karl Crary
April 30, 1996
Some Recent Results of R. Dyckhoff and A. Pitts
by Todd Wilson
March 26, 1996
Formal Module Systems and Nuprl-Light: A Programmer's Perspective
by Jason Hickey
February 13, 1996
Project Direction and Research Problems
by Robert L. Constable
February 06, 1996
Operational Modal Logic
by Sergei Artemov
January 29, 1996
Formal Domain Theory
by Neal Glew
December 05, 1995
Verifying HORUS in Nuprl
by Jason Hickey
November 28, 1995
New Nuprl Editor
by Stuart F. Allen
November 07, 1995
Formal Abstract Data Types and Inheritance
by Jason Hickey
October 31, 1995
GOLEM
by Ettore Remidde
October 24, 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
Overview of Nuprl 5
by Stuart F. Allen
September 19, 1995
Formal Modules (Abstract Data Types) and Object Oriented Programming
by Jason Hickey
1995-1996
HORUS Verification Effort
by Jason Hickey
1995-1996
The MathBus Term Structure
by Richard Zippel
1995-1996
1995
Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra
| cite »
by Paul B. Jackson
1995
Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995
| cite »
by Robert L. Constable
1995
Expressing Computational Complexity in Constructive Type Theory
| cite »
by Robert L. Constable
1995
1994-1995
Square-Root Verification
by Jason Hickey
May 10, 1995
Imperative Program Semantics
by Stuart F. Allen
May 02, 1995
The Refiner as the Inference Mechanism of Nuprl Proof Development System
by Roderick Moten
April 04, 1995
Defining the Polynomial Time Functions over N in Nuprl
by Robert L. Constable
March 28, 1995
An Open Architecture for Nuprl
by Robert L. Constable
March 01, 1995
Developing Set Theory in HOL
by Paul B. Jackson
February 28, 1995
Motivation: Basis of a Set Theory for Nuprl
by Todd Wilson
February 21, 1995
Chet Says Good-Bye: Theory; Implementation (System); Methodology; Science
by Chetan Murthy
February 14, 1995
Formal Methods Program at NASA Langley Research Center
by James L. Caldwell
February 07, 1995
The Engineering Aspects of Proof-Environment Design
by Chetan Murthy
January 24, 1995
Notation and Computer Aided Mathematics
by Conal Mannion
December 06, 1994
Verifying an Implementation of a Polynomial Algebra ADT
by Paul B. Jackson
November 29, 1994
Representing Computational Complexity in Nuprl
by Robert L. Constable
November 22, 1994
The "Interface" Version of Nuprl
by Stuart F. Allen, Richard Eaton
November 15, 1994
The Ultimate Programming Machine II: Very Dependent Types
by Jason Hickey
November 08, 1994
TLA
by Scott D. Stoller, Chetan Murthy
November 01, 1994
The Ultimate Programming Machine
by Jason Hickey
October 25, 1994
Program Optimization in Type Theory
by Brent Knight
October 18, 1994
Program Development for Proof Transformations
by Helmut Schwichtenberg
October 12, 1994
Computer Algebra, Theorem Proving, and Types
by Todd Wilson
October 04, 1994
Gröbner Basis
by Thomas Yan
September 20, 1994
Recursive Types in Coq
by Christine Paulin-Mohring
September 08, 1994
Very Dependent Function Space
by Jason Hickey
1994-1995
1994
An Operational Approach to Combining Classical Set Theory and Functional Programming Languages
| cite »
by Douglas J. Howe, Scott D. Stoller
1994
Aspects of the Computational Content of Proofs
| cite »
by Judith Underwood
1994
Exploring Abstract Algebra in Constructive Type Theory
| cite »
by Paul B. Jackson
1994
Exporting and Reflecting Abstract Meta-mathematics
| cite »
by Robert L. Constable
1994
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization
| cite »
by John O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard
1994
Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics
| cite »
by Robert L. Constable, Paul B. Jackson
1994
Using Reflection to Explain and Enhance Type Theory
| cite »
by Robert L. Constable
1994
1993-1994
Verifying a Pipelined Circuit
by Mark Aagaard
April 05, 1994
An Operational Approach to Combining Classical Set Theory and Functional Programming Languages
by Scott D. Stoller
March 29, 1994
Formalizing the Theory Concept in Nuprl
by Jason Hickey
March 15, 1994
Formalizing the Theory Mechanism in NuPRL
by Jason Hickey
March 15, 1994
Hilbert Basis Function
by Thomas Yan
March 01, 1994
The MIZAR Project
by Paul B. Jackson
February 15, 1994
A Constructive Completeness Proof for Intuitionistic Predicate Calculus
by Judith Underwood
February 01, 1994
Abstract Programming in Nuprl
by Jason Hickey
November 23, 1993
Editing
by Stuart F. Allen
November 16, 1993
Formalizing Hamiltonian Dynamics
by Conal Mannion
November 09, 1993
Computational Content of Math
by Douglas Bridges
October 19, 1993
How to Integrate Set Theory and Computation?
by Scott D. Stoller
September 14, 1993
A (Possibly) New Scheme for Libraries/Proof-Contexts
by Chetan Murthy
September 03, 1993
Semantics
by Scott D. Stoller
March 30, 1993
A Program Transformation System
by Annie Liu
1993-1994
Extraction of Programs
by Benjamin Werner
1993-1994
Polya/Nuprl
by Stuart F. Allen
1993-1994
Reasoning about Scientific Programs
by Conal Mannion, Stuart F. Allen
1993-1994
1993 Summ
Theorem Proving with Real Numbers
by Robert L. Constable
August 31, 1993
Connecting Formal Semantics to Constructive Intuitions
by Michael J. O'Donnell
July 06, 1993
Project Overview
by Robert L. Constable
July 01, 1993
1993
Formalizing Constructive Real Analysis
| cite »
by Max B. Forester
1993
Reasoning About Functional Programs in Nuprl
| cite »
by Douglas J. Howe
1993
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification
| cite »
by Mark Aagaard, Miriam Leeser
1993
The Tableau Algorithm for Intuitionistic Propositional Calculus as a Constructive Completeness Proof
| cite »
by Judith Underwood
1993
1992-1993
TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
May 04, 1993
Formalizing Program Synthesis
by Arnd Poetzsch
April 27, 1993
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
Proofs by Structural Induction using Partial Evaluation
by Julia Lawall
April 13, 1993
Reflection
by William Aitken
April 06, 1993
Using Reflection to External Automated Theorem Provers
by Mark Aagaard
March 30, 1993
Extraction
by Judith Underwood
March 16, 1993
Semantics of the Nuprl Type Theory
by Scott D. Stoller
March 16, 1993
Editor Demonstration
by Paul B. Jackson
March 09, 1993
Constructive Algorithms in Nuprl
by Douglas J. Howe
December 01, 1992
The Enigma of Sat Hill Climbing Procedures
by Ian Gent
November 10, 1992
Set Models
by Douglas J. Howe
November 03, 1992
Structuring Proofs
by Douglas J. Howe, Paul B. Jackson
October 27, 1992
Fefprl
by Douglas J. Howe, Douglas J. Howe
October 20, 1992
Fefprl
by Douglas J. Howe, Douglas J. Howe
October 05, 1992
Are There Long Reduction Sequences with Short Normal Forms?
by Helmut Schwichtenberg
September 29, 1992
Tactic Trees in eXene
by Roderick Moten
September 22, 1992
HOL Workshop
by Mark Aagaard
September 15, 1992
Defining Polynomials in Constructive Type Theory
by Paul B. Jackson
1992-1993
1992
A Computational Analysis of Girard's Translation and LC
| cite »
by Chetan Murthy
1992
Formal Theories and Software Systems: Fundamental Connections Between Computer Science and Logic
| cite »
by Robert L. Constable
1992
Lectures on: Classical Proofs as Programs
| cite »
by Robert L. Constable
1992
Meta-Synthesis: Deriving Programs That Develop Programs
| cite »
by Christoph Kreitz
1992
Metalevel Programming in Constructive Type Theory
| cite »
by Robert L. Constable
1992
Nuprl and Its Use in Circuit Design
| cite »
by Paul B. Jackson
1992
Tactic-Based Theorem Proving and Knowledge-Based Forward Chaining: An Experiment with Nuprl and Ontic
| cite »
by Wilfred Z. Chen
1992
Using Nuprl for the Verification and Synthesis of Hardware
| cite »
by Miriam Leeser
1992
A Simple Type Theory for Reasoning About Functional Programs
| cite »
by Douglas J. Howe
1992
1991-1992
CADE Practice Talk
by Wilfred Z. Chen
May 12, 1992
PVS
by N Shankar
March 24, 1992
Reflection 2
by William Aitken, William Aitken
March 05, 1992
Reflection 2
by William Aitken, William Aitken
February 18, 1992
Attaching Context to Objects in the Library
by Stuart F. Allen
February 04, 1992
PRL Library Day
by Stuart F. Allen
November 19, 1991
Can we Compile the Prolog Program to a Type?
by Jim Lipton
November 12, 1991
Nuprl 3 vs. Nuprl 4
by Paul B. Jackson
November 05, 1991
How to Strengthen the Notion of Obvious Step
by Wilfred Z. Chen
October 22, 1991
1991
On computational open-endedness in Martin-Lof's type theory
by Douglas J. Howe
July 15, 1991
An Evaluation Semantics for Classical Proofs
| cite »
by Chetan Murthy
1991
Metalogical Frameworks
| cite »
by David A. Basin, Robert L. Constable
1991
Some Normalization Properties of Martin-Lof's Type Theory and Applications
| cite »
by David A. Basin, Douglas J. Howe
1991
Developing a Toolkit for Floating-Point Hardware in the Nuprl Proof Development System
| cite »
by Paul B. Jackson
1991
Extracting Circuits from Constructive Proofs
| cite »
by David A. Basin
1991
Finding Computational Content from Classical Proofs
| cite »
by Robert L. Constable, Chetan Murthy
1991
Formally Verified Synthesis of Combinational Circuits
| cite »
by David A. Basin, Geoffrey Brown, Miriam Leeser
1991
Type Theory as a Foundation for Computer Science
| cite »
by Robert L. Constable
1991
1990-1991
A Basis for Constructive, Reflexive Type Theory
by William Aitken
October 01, 1990
Lambda Calculus as Basis for Programming Language Design
by Robert W. Harper
1990-1991
1990 Summ
M-L Type Theory, Categories, Inductive Types
by Nax P. Mendler
1990 Summ
1990
A Constructive Completeness Proof for the Intuitionistic Propositional Calculus
| cite »
by Judith Underwood
1990
A Constructive Proof of Higman's Lemma
| cite »
by Chetan Murthy, James R. Russell
1990
Building Problem Solving Environments in Constructive Type Theory
| cite »
by David A. Basin
1990
Extracting Constructive Content from Classical Proofs
| cite »
by Chetan Murthy
1990
Implementing Metamathematics as an Approach to Automatic Theorem Proving
| cite »
by Robert L. Constable, Douglas J. Howe
1990
Nuprl as a General Logic
| cite »
by Robert L. Constable, Douglas J. Howe
1990
Reflecting the Open-Ended Computation System of Constructive Type Theory
| cite »
by Robert L. Constable, Stuart F. Allen, Douglas J. Howe
1990
The Oyster-Clam System
| cite »
by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill
1990
The Semantics of Reflected Proof
| cite »
by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken
1990
1989-1990
20BJ as a Meta-logical Framework
by Andrew Stevens
April 21, 1990
Using Nuprl to Verify Floating Point Hardware
by Paul B. Jackson
April 17, 1990
Plotkin
by Jim Lipton
March 13, 1990
Logical Relations
by Jim Lipton
March 06, 1990
Polymorphism Is Not Set Theoretic
by Nax P. Mendler
February 14, 1990
Intuitionistic ZF
by Jim Lipton
January 30, 1990
The Lambda Calculus as a Basis for Language Design
by Robert W. Harper
1989-1990
1989
Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments
| cite »
by Robert L. Constable
1989
Building Theories in Nuprl
| cite »
by David A. Basin
1989
Equality in Lazy Computation Systems
| cite »
by Douglas J. Howe
1989
Partial Objects in Type Theory
| cite »
by Scott F. Smith
1989
Verification of Combinational Logic in Nuprl
| cite »
by David A. Basin, Peter Del Vecchio
1989
Logic-Based Knowledge Representation
| cite »
by Paul B. Jackson
1989
Reflection in Constructive and Non-Constructive Automated Reasoning
| cite »
by Fausto Giunchiglia, Alan Smaill
1989
1988
An Environment for Automated Reasoning About Partial Functions
| cite »
by David A. Basin
1988
Automatic Program Optimization Via the Transformation of Nuprl Synthesis Proofs
| cite »
by Peter Madden
1988
Automating Reasoning in an Implementation of Constructive Type Theory
| cite »
by Douglas J. Howe
1988
Computational Foundations of Basic Recursive Function Theory
| cite »
by Robert L. Constable, Scott F. Smith
1988
Computational Metatheory in Nuprl
| cite »
by Douglas J. Howe
1988
Inductive Definition in Type Theory
| cite »
by Nax P. Mendler
1988
Notational Definition and Top-down Refinement for Interactive Proof Development Systems
| cite »
by Timothy G. Griffin
1988
Collaborative Problem Solving Environment
by Robert L. Constable
1988
The Nuprl Proof Development System
| cite »
by Christian Horn
1988
1987-1988
Continuation of A Type Theoretic Interpretation of DougHowe's Squiggle Relation
by Stuart F. Allen
April 26, 1988
A Type Theoretic Interpretation of Doug Howe's Squiggle Relation
by Stuart F. Allen
April 19, 1988
TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
April 08, 1988
Rational Reconstruction of Boyer and Moore Prover
by Andrew Stevens
December 01, 1987
Partial Objects
by Scott F. Smith
November 24, 1987
Math Vernacular
by N. G. deBruijn
November 17, 1987
Domains in Type Theory
by Scott F. Smith
November 10, 1987
Typed Enumeration-Free External Setting for Computing Theory
by Robert L. Constable
November 03, 1987
TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
October 13, 1987
The ONTIC System
by David McAllister
October 06, 1987
Syntactic Abstraction
by Timothy G. Griffin
September 22, 1987
1987
A Non-Type-Theoretic Definition of Martin-Lof's Types
| cite »
by Stuart F. Allen
1987
A Non-Type-Theoretic Semantics for Type-Theoretic Language
| cite »
by Stuart F. Allen
1987
Implementing Number Theory: An Experiment with Nuprl
| cite »
by Douglas J. Howe
1987
Metamathematical Extensibility in Type Theory
| cite »
by Todd B. Knoblock
1987
Partial Objects in Constructive Type Theory
| cite »
by Scott F. Smith, Robert L. Constable
1987
The Computational Behaviour of Girard's Paradox
| cite »
by Douglas J. Howe
1987
Type-Theoretic Models of Concurrency
| cite »
by Walter Rance Cleaveland
1987
Recursive Types and Type Constraints in Second-Order Lambda Calculus
| cite »
by Nax P. Mendler
1987
1986-1987
Metamathematics of Reflection
by Todd B. Knoblock
April 22, 1987
The Expressiveness of lambda Y
by David A. Basin
April 09, 1987
Bar Types
by Scott F. Smith
March 18, 1987
Realizabiity for IZF
by Jim Lipton
March 12, 1987
Term Model Semantics and Tait Computability Method
by Scott F. Smith
March 11, 1987
IZF and Recursive Realizability
by Jim Lipton
March 05, 1987
Category Theory as Basis for Mathematics
by John Beck
December 02, 1986
Continuation of Categorial Models of Nuprl
by Michael Schwartzbach
October 28, 1986
Categorical Models of Nuprl
by Michael Schwartzbach
October 21, 1986
Strong Normalization in Lambda2
by Nax P. Mendler
October 02, 1986
Empty Types
by John Mitchell
September 25, 1986
Implementing Finite Sets
by Walter Rance Cleaveland
September 09, 1986
1986
Constructive Automata Theory Implemented with the Nuprl Proof Development System
| cite »
by Christoph Kreitz
1986
Formalized Metareasoning in Type Theory
| cite »
by Todd B. Knoblock, Robert L. Constable
1986
Implementing Mathematics with the Nuprl Development System
| cite »
by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith
1986
Infinite Objects in Type Theory
| cite »
by Nax P. Mendler, Robert L. Constable, Prakash Panangaden
1986
1985-1986
Programs as Specification
by Rick Hehner
May 06, 1986
1985
Aspects of the Implementation of Type Theory
| cite »
by Robert W. Harper
1985
Constructive Mathematics as a Programming Logic I: Some Principles of Theory
| cite »
by Robert L. Constable
1985
Extracting Efficient Code from Constructive Proofs
| cite »
by James T. Sasaki
1985
Proofs as Programs
| cite »
by Joseph L. Bates, Robert L. Constable
1985
Recursive Definitions in Type Theory
| cite »
by Robert L. Constable, Nax P. Mendler
1985
Semantics of Evidence
| cite »
by Robert L. Constable
1985
1984-1985
Arithpac
by Timothy G. Griffin
1984-1985
Defining Lambda-prl and Its Extensions
by Scott F. Smith
1984-1985
Denotational Semantics
by Nax P. Mendler
1984-1985
Equality
by Robert W. Harper
1984-1985
Marhew's Principle
by Ryan Stansifer
1984-1985
ML Execution
by H. M. Bromley
1984-1985
Nuprl Execution
by H. M. Bromley
1984-1985
Optimizing Ext
by James T. Sasaki
1984-1985
Partial Recursive Functions
by Nax P. Mendler
1984-1985
PP-lambda in Nuprl
by Nax P. Mendler
1984-1985
Predicate Calculus Model
by Stuart F. Allen
1984-1985
Prolog
by Ryan Stansifer, Stuart F. Allen
1984-1985
Reflective PRL
by Todd B. Knoblock
1984-1985
Theory of Reals
by Douglas J. Howe
1984-1985
Thesis
by Douglas J. Howe
1984-1985
Type Inference
by Robert W. Harper
1984-1985
Universally Closed Classes
by Robert L. Constable
1984-1985
Using Lemmas
by Timothy G. Griffin
1984-1985
1984
Writing Programs That Construct Proofs
| cite »
by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates
1984
1981
A Logic for Correct Program Development
| cite »
by Joseph L. Bates
1981
1980
Reversal-Bounded Computations
| cite »
by Tat-hung Chan
1980
1979
A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS
| cite »
by Robert L. Constable, James Donahue
July 01, 1979
1978
A Programming Logic
| cite »
by Robert L. Constable, Michael J. O'Donnell
1978
1977
A Constructive Programming Logic
by Robert L. Constable
August 08, 1977
1971
Constructive Mathematics and Automatic Program Writers
| cite »
by Robert L. Constable
1971