#
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 Lambda ^{2} *

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