#
Knowledge Base of

Publications,
Seminars,
& Math Library

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

## List by Author

1025 results

Aagaard, Mark

*
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

*
Verifying a Pipelined Circuit *

by Mark Aagaard

April 05, 1994

*
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification *
| cite »

by Mark Aagaard, Miriam Leeser

1993

*
Using Reflection to External Automated Theorem Provers *

by Mark Aagaard

March 30, 1993

*
HOL Workshop *

by Mark Aagaard

September 15, 1992

Aitken, William

*
Metalogical Frameworks II: Developing a Reflected Decision Procedure *
| cite »

by William Aitken, Robert L. Constable, Judith Underwood

1999

*
Reflection *

by William Aitken

April 06, 1993

*
Reflection 2 *

by William Aitken, William Aitken

March 05, 1992

*
Reflection 2 *

by William Aitken, William Aitken

March 05, 1992

*
Reflection 2 *

by William Aitken, William Aitken

February 18, 1992

*
Reflection 2 *

by William Aitken, William Aitken

February 18, 1992

*
A Basis for Constructive, Reflexive Type Theory *

by William Aitken

October 01, 1990

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

Allen, Stuart F.

*
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

*
Enabling Large Scale Coherency Among Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable

2006

*
Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable, Lori Lorigo

2006

*
An Abstract Semantics for Atoms in Nuprl *
| cite »

by Stuart F. Allen

2006

*
A Semantics for Abstract Atoms in Nuprl *

by Stuart F. Allen

March 31, 2006

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

by Stuart F. Allen

April 15, 2005

*
Anchoring Expository Text in Formal Mathematics *

by Stuart F. Allen

December 06, 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

*
Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping *
| cite »

by Stuart F. Allen

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

*
Russel's Paradox *

by Stuart F. Allen

December 14, 2004

*
How to browse the library *

by Stuart F. Allen

December 14, 2004

*
Towers of Hanoi *

by Stuart F. Allen

April 27, 2004

*
Readability Exercise (num theory) *

by Stuart F. Allen

December 14, 2004

*
Type Theory as a Legacy from Logicism *

by Stuart F. Allen

March 08, 2004

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

by Stuart F. Allen

February 09, 2004

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

by Stuart F. Allen

December 01, 2003

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

by Stuart F. Allen

November 17, 2003

*
Practical Reflection in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen, Robert L. Constable

2003

*
Nuprl Basics *

by Stuart F. Allen

September 18, 2003

*
Standard Resources *

by Stuart F. Allen

September 23, 2003

*
Elementary Number Theory *

by Stuart F. Allen

September 23, 2003

*
Nuprl Editor and Interface *

by Stuart F. Allen

September 23, 2003

*
Abstract Identifiers and Textual Reference *
| cite »

by Stuart F. Allen

2002

*
Reflecting Higher-Order Abstract Syntax in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen

2002

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Report on the Design of the Formal Digital Library *

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

April 08, 2002

*
Explaining the Formal Digital Library *

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

March 11, 2002

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

by Stuart F. Allen, Robert L. Constable

December 03, 2001

*
Logical Aspects of Digital Mathematics Libraries (extended abstract) *
| cite »

by Stuart F. Allen, James L. Caldwell, Robert L. Constable

2001

*
Lists *

by Stuart F. Allen

May 15, 2001

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

*
Semantics and Pragmatics of Reflected Proof *

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

December 01, 1998

*
Some Uses of the Intersection Type *

by Stuart F. Allen, Robert L. Constable

May 03, 1999

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

by Stuart F. Allen

March 29, 1999

*
Reflection Mechanisms in Nuprl *

by Stuart F. Allen, Robert L. Constable

November 10, 1998

*
From dy/dx to []P: A Matter of Notation *
| cite »

by Stuart F. Allen

1998

*
Application of Notational Methods in dy/dx *

by Stuart F. Allen

March 31, 1998

*
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

*
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

*
New Nuprl Editor *

by Stuart F. Allen

November 07, 1995

*
Overview of Nuprl 5 *

by Stuart F. Allen

September 19, 1995

*
Imperative Program Semantics *

by Stuart F. Allen

May 02, 1995

*
The "Interface" Version of Nuprl *

by Stuart F. Allen, Richard Eaton

November 15, 1994

*
Reasoning about Scientific Programs *

by Conal Mannion, Stuart F. Allen

1993-1994

*
Polya/Nuprl *

by Stuart F. Allen

1993-1994

*
Editing *

by Stuart F. Allen

November 16, 1993

*
Attaching Context to Objects in the Library *

by Stuart F. Allen

February 04, 1992

*
PRL Library Day *

by Stuart F. Allen

November 19, 1991

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

*
Reflecting the Open-Ended Computation System of Constructive Type Theory *
| cite »

by Robert L. Constable, Stuart F. Allen, Douglas J. Howe

1990

*
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

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

*
Prolog *

by Ryan Stansifer, Stuart F. Allen

1984-1985

*
Predicate Calculus Model *

by Stuart F. Allen

1984-1985

Anand, Abhishek

*
A Type Theory with Partial Equivalence Relations as Types *

by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli

May 12, 2014

*
Towards a Formally Verified Proof Assistant *

by Abhishek Anand, Vincent Rahli

July 14, 2014

*
A Generic Approach to Proofs about Substitution *

by Abhishek Anand, Vincent Rahli

July 17, 2014

*
Topics in Type Theory *

by Abhishek Anand, Robert L. Constable, Mark Bickford

October 22, 2014

*
Coinduction in Coq *

by Abhishek Anand

November 12, 2014

*
From Replicated Databases to Ensembles of Collaborating Robots *

by Abhishek Anand, Mark Bickford

November 19, 2014

*
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types *
| cite »

by Vincent Rahli, Mark Bickford, Abhishek Anand

April 22, 2013

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

by Abhishek Anand

October 09, 2013

*
A verified proof assistant *

by Vincent Rahli, Abhishek Anand

October 30, 2013

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

by Abhishek Anand, Vincent Rahli

November 20, 2013

*
The Type Base and Undecidability in Type Theory *

by Abhishek Anand

September 21, 2012

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

by Robert L. Constable, Mark Bickford, Abhishek Anand

October 12, 2012

Artemov, Sergei

*
Reflected Lambda Calculus *

by Sergei Artemov

October 02, 2000

*
Stability of intuitionistic systems *

by Sergei Artemov

April 24, 2000

*
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

*
Proof Polynomials: Cut Elimination *

by Sergei Artemov

October 07, 1997

*
Operational Modal Logic *

by Sergei Artemov

January 29, 1996

Aydemir, Brian

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

Barzilay, Eli

*
Implementing Reflection in Nuprl *
| cite »

by Eli Barzilay

2006

*
Practical Reflection in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen, Robert L. Constable

2003

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
Reflecting Higher-Order Abstract Syntax in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen

2002

*
Quotation and Reflection in Nuprl and Scheme *
| cite »

by Eli Barzilay

2001

*
Reflection in First-Order Logic *

by Eli Barzilay

February 12, 2001

*
Latest results about reflection (TENTATIVE) *

by Eli Barzilay

November 20, 2000

*
Reflection Part II *

by Eli Barzilay

April 03, 2000

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

by Eli Barzilay

March 06, 2000

*
Practical Uses of Quotations, Macros and Reflection *

by Eli Barzilay

April 05, 1999

Barzilay, Regina

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

by Regina Barzilay

March 03, 2003

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

by Regina Barzilay

October 21, 2002

*
The Abstract Term Type *

by Regina Barzilay

March 04, 2002

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

*
Verbalization of High-Level Formal Proofs *
| cite »

by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable

1999

Basin, David A.

*
TBA *

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

May 04, 1993

*
Extracting Circuits from Constructive Proofs *
| cite »

by David A. Basin

1991

*
Formally Verified Synthesis of Combinational Circuits *
| cite »

by David A. Basin, Geoffrey Brown, Miriam Leeser

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

*
Building Problem Solving Environments in Constructive Type Theory *
| cite »

by David A. Basin

1990

*
Building Theories in Nuprl *
| cite »

by David A. Basin

1989

*
Verification of Combinational Logic in Nuprl *
| cite »

by David A. Basin, Peter Del Vecchio

1989

*
An Environment for Automated Reasoning About Partial Functions *
| cite »

by David A. Basin

1988

*
TBA *

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

April 08, 1988

*
TBA *

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

October 13, 1987

*
The Expressiveness of lambda Y *

by David A. Basin

April 09, 1987

Bates, Joseph L.

*
Proofs as Programs *
| cite »

by Joseph L. Bates, Robert L. Constable

1985

*
Writing Programs That Construct Proofs *
| cite »

by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates

1984

*
A Logic for Correct Program Development *
| cite »

by Joseph L. Bates

1981

Beck, John

*
Category Theory as Basis for Mathematics *

by John Beck

December 02, 1986

Benzinger, Ralph

*
Automated Complexity Analysis of Nuprl Extracted Programs *
| cite »

by Ralph Benzinger

2001

*
Automated Computational Complexity Analysis *
| cite »

by Ralph Benzinger

2001

*
Automated Higher-Order Complexity Analysis *

by Ralph Benzinger

February 05, 2001

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

*
Automatic Complexity Analysis Revisited *

by Ralph Benzinger

January 31, 2000

*
Automated Complexity Analysis *

by Ralph Benzinger

September 15, 1998

Berger, Ulrich

*
Logic, Construction, Computation *
| cite »

by Ulrich Berger

July 29, 2012

Bertot, Yves

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

by Yves Bertot

November 17, 1998

Bickford, Mark

*
Formalization of Cubical Type Theory in Nuprl *

by Mark Bickford

January 15, 2020

*
DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics *

by Mark Bickford

February 18, 2020

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

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

2019

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

by Ariel Kellison, Mark Bickford

November 26, 2019

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

by Vincent Rahli, Mark Bickford

January 02, 2018

*
Connectedness of the Continuum in Intuitionistic Mathematics *
| cite »

by Mark Bickford

2018

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

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

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

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

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

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

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 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

*
A Nominal Exploration of Intuitionism *

by Vincent Rahli, Mark Bickford

January 18, 2016

*
Constructive Analysis and Experimental Mathematics using the Nuprl Proof Assistant *

by Mark Bickford

March 02, 2016

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

September 01, 2015

*
Coq as a Metatheory for Nuprl with Bar Induction *

by Vincent Rahli, Mark Bickford

September 14, 2015

*
Nuprl’s Inductive Logical Forms *

by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli

September 01, 2015

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

January 01, 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 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

*
A Fast Algorithm for the Integer Square Root *

by Anne Trostle, Mark Bickford

June 09, 2014

*
Synthesizing Protocols using the Logic of Events and EventML *

by Robert L. Constable, Mark Bickford

September 17, 2014

*
There Are No Discontinuous Real Functions *

by Mark Bickford, Vincent Rahli

October 08, 2014

*
Topics in Type Theory *

by Abhishek Anand, Robert L. Constable, Mark Bickford

October 22, 2014

*
Nominal Type Theory *

by Mark Bickford, Vincent Rahli

October 29, 2014

*
From Replicated Databases to Ensembles of Collaborating Robots *

by Abhishek Anand, Mark Bickford

November 19, 2014

*
Synthetic Topology in NuPRL *

by Francisco Mota, Mark Bickford

December 03, 2014

*
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 power of bar induction in constructive type theory *

by Mark Bickford

September 25, 2013

*
Quotient Types in Nuprl *

by Mark Bickford

November 13, 2013

*
The Logic of Events, a framework to reason about distributed systems *
| cite »

by Mark Bickford, Vincent Rahli, Robert L. Constable

2012

*
Introduction to EventML *

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

February 03, 2012

*
Formalizing Moessner's Theorem in Nuprl *

by Mark Bickford, Dexter Kozen, Alexandra Silva

June 08, 2012

*
Polymorphic Logic *
| cite »

by Mark Bickford, Robert L. Constable

July 29, 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

*
Formalizing Constructive Analysis in Nuprl *

by Mark Bickford

September 04, 2012

*
Wider Deployment of Nuprl *

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

September 28, 2012

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

by Robert L. Constable, Mark Bickford, Abhishek Anand

October 12, 2012

*
Realizing Bar Induction in Nuprl *

by Mark Bickford

October 26, 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

*
NuPRL Demo *

by Mark Bickford

September 16, 2011

*
Simple Consensus Algorithm *

by Robert L. Constable, Mark Bickford, Vincent Rahli

October 28, 2011

*
Impredicative vs Predicative Type Theory *

by Robert L. Constable, Mark Bickford, Richard Eaton

April 13, 2012

*
Adding Communication Primitives to the Nuprl Evaluator *

by Mark Bickford

May 04, 2012

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

October 07, 2011

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

by Mark Bickford, Robert L. Constable, David Guaspari

2010

*
Automated Proof of Authentication Protocols in a Logic of Events *
| cite »

by Mark Bickford

2010

*
Investigating Correct-by-Construction Attack-Tolerant Systems *
| cite »

by Robert L. Constable, Mark Bickford, Robbert van Renesse

2010

*
Component Specification Using Event Classes *
| cite »

by Mark Bickford

2009

*
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

*
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

*
Formalizing chain replication *

by Mark Bickford, David Guaspari

2006

*
Unguessable Atoms: A Logical Foundation for Security *
| cite »

by Mark Bickford

2006

*
Chain Replication Protocol *

by Mark Bickford

September 27, 2006

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

by Mark Bickford

November 18, 2005

*
Automating Proofs in Event Logic *

by Mark Bickford, Richard Eaton

August 26, 2005

*
Automated Proofs in Event Logic *

by Mark Bickford

September 16, 2005

*
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

*
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

*
Real-time Message Automata *

by Mark Bickford

February 11, 2005

*
Mark Presentation *

by Mark Bickford

November 29, 2004

*
Urelements in Computational Type Theory *

by Mark Bickford

November 11, 2005

*
Knowledge-Based Synthesis of Distributed Systems Using Event Structures *

by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

2004

*
The Logic of Events and Event Structure Patterns *

by Mark Bickford

April 26, 2004

*
Leader Election Protocols *

by Mark Bickford

October 06, 2003

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

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

2003

*
A Logic of Events *
| cite »

by Mark Bickford, Robert L. Constable

2003

*
Event Systems *

by Mark Bickford

November 08, 2003

*
Graph Theory *

by Mark Bickford

May 14, 2003

*
General Automata Theory *

by Mark Bickford

January 25, 2003

*
Implementing the Logic of Events *

by Mark Bickford

February 24, 2003

*
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

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Hybrid Protocols *

by Mark Bickford

February 20, 2002

*
Recent Results on the PCES Project *

by Mark Bickford

April 01, 2002

*
Report on the DARPA PCES PI meeting *

by Robert L. Constable, Lori Lorigo, Mark Bickford

October 29, 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

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable

2001

*
Proving Hybrid Protocols Correct *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu

2001

*
Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse

2001

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable

2001

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

*
Continuation on reflection *

by Mark Bickford

March 13, 2000

*
IO-automata and Ensemble *

by Mark Bickford

February 21, 2000

*
An Object-Oriented Approach to Verifying Group Communication Systems *
| cite »

by Mark Bickford, Jason Hickey

1999

Birman, Kenneth

*
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

*
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

Bridges, Douglas

*
Computational Content of Math *

by Douglas Bridges

October 19, 1993

Bromley, H. M.

*
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

*
ML Execution *

by H. M. Bromley

1984-1985

*
Nuprl Execution *

by H. M. Bromley

1984-1985

Brown, Geoffrey

*
Formally Verified Synthesis of Combinational Circuits *
| cite »

by David A. Basin, Geoffrey Brown, Miriam Leeser

1991

Bryukhov, Yegor

*
Arithmetic module for MetaPRL: rules and Arith tactic *

by Yegor Bryukhov

March 25, 2002

Bundy, Alan

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

Caldwell, James L.

*
Classical Propositional Logic *

by James L. Caldwell

July 28, 2004

*
Logical Aspects of Digital Mathematics Libraries (extended abstract) *
| cite »

by Stuart F. Allen, James L. Caldwell, Robert L. Constable

2001

*
Search Algorithms in Type Theory *
| cite »

by James L. Caldwell, Ian Gent, Judith Underwood

2000

*
Intuitionistic Tableau Extracted *
| cite »

by James L. Caldwell

1999

*
Classical Propositional Decidability via Nuprl Proof Extraction *
| cite »

by James L. Caldwell

1998

*
Decidability Extracted: Synthesizing *
| cite »

by James L. Caldwell

1998

*
Extracting Readable and Efficient Programs from Nuprl Proofs *

by James L. Caldwell

November 18, 1997

*
Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extracted Program *
| cite »

by James L. Caldwell

1997

*
Moving Proofs-as-Programs into Practice *
| cite »

by James L. Caldwell

1997

*
Classical Tools for Constructive Proof Search *
| cite »

by James L. Caldwell, Judith Underwood

1996

*
Formal Methods Program at NASA Langley Research Center *

by James L. Caldwell

February 07, 1995

Chan, Tat-hung

*
Reversal-Bounded Computations *
| cite »

by Tat-hung Chan

1980

Chen, Wilfred Z.

*
TBA *

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

May 04, 1993

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

by Wilfred Z. Chen

1992

*
CADE Practice Talk *

by Wilfred Z. Chen

May 12, 1992

*
How to Strengthen the Notion of Obvious Step *

by Wilfred Z. Chen

October 22, 1991

*
TBA *

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

April 08, 1988

*
TBA *

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

October 13, 1987

Cheney, James

*
Randomized Programming and Probabilistic Reasoning in Type Theory *

by James Cheney

April 17, 2000

Cheung, Crystal

*
Brouwer's Fan Theorem: An Overview *

by Crystal Cheung

2015

Chew, Paul

*
Collaborative Mathematics Environments *
| cite »

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

1996

Cleaveland, Walter Rance

*
Type-Theoretic Models of Concurrency *
| cite »

by Walter Rance Cleaveland

1987

*
Implementing Finite Sets *

by Walter Rance Cleaveland

September 09, 1986

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

Cohen, Liron

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

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

2019

*
Automated Reasoning in Herbrand Structures *

by Liron Cohen, Reuben Rowe, Yoni Zohar

June 03, 2019

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

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

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

*
Intuitionistic Ancestral Logic *

by Liron Cohen, Robert L. Constable

October 10, 2015

*
Intuitionistic Ancestral Logic *

by Liron Cohen

July 12, 2012

Constable, Robert L.

*
Computer Science at the Frontiers of Mathematics *

by Robert L. Constable

January 15, 2020

*
The Continuum *

by Robert L. Constable

February 26, 2020

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

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

2019

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

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

2018

*
Implementing Euclid's Straightedge and Compass Constructions in Type Theory *
| cite »

by Ariel Kellison, Mark Bickford, Robert L. Constable

2018

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

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 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

*
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

*
Intuitionistic Ancestral Logic *

by Liron Cohen, Robert L. Constable

October 10, 2015

*
Constructive Reading of Classical Logic *

by Robert L. Constable, Sarah Sernaker

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

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

January 01, 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 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

*
Logical Investigations, with the Nuprl Proof Assistant *

by Robert L. Constable, Anne Trostle

July 22, 2014

*
Synthesizing Protocols using the Logic of Events and EventML *

by Robert L. Constable, Mark Bickford

September 17, 2014

*
Topics in Type Theory *

by Abhishek Anand, Robert L. Constable, Mark Bickford

October 22, 2014

*
Virtual Evidence: A Constructive Semantics for Classical Logics *

by Robert L. Constable

2014

*
The Logic of Information Flow and the Foundations of Distributed Computing *

by Robert L. Constable

January 10, 2013

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

March 31, 2013

*
An Extension of OCaml's Type Theory *

by Robert L. Constable

October 23, 2013

*
Nuprl as a Programming Assistant *

by Robert L. Constable

November 06, 2013

*
The Logic of Events, a framework to reason about distributed systems *
| cite »

by Mark Bickford, Vincent Rahli, Robert L. Constable

2012

*
Introduction to EventML *

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

February 03, 2012

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

by Robert L. Constable

March 19, 2012

*
Type Theoretic Semantics for First-Order Logic *

by Robert L. Constable

May 24, 2012

*
Proof Assistants and the Dynamic Nature of Formal Theories *
| cite »

by Robert L. Constable

June 29, 2012

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

by Robert L. Constable

June 29, 2012

*
Introduction to the Fall Seminar Series *

by Robert L. Constable

September 07, 2012

*
Polymorphic Logic *
| cite »

by Mark Bickford, Robert L. Constable

July 29, 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

*
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

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

by Robert L. Constable, Mark Bickford, Abhishek Anand

October 12, 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

*
Next Generation Proof Technology *

by Robert L. Constable

December 27, 2012

*
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

*
Seminar History and Initial Planning Meeting *

by Robert L. Constable, Robert L. Constable

September 09, 2011

*
Analyzing Access Control Logics Using Evidence Semantics *

by Robert L. Constable

September 23, 2011

*
Simple Consensus Algorithm *

by Robert L. Constable, Mark Bickford, Vincent Rahli

October 28, 2011

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

by Robert L. Constable

February 24, 2012

*
Reviewing Nuprl *

by Robert L. Constable

March 09, 2012

*
Impredicative vs Predicative Type Theory *

by Robert L. Constable, Mark Bickford, Richard Eaton

April 13, 2012

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

October 07, 2011

*
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

*
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge *
| cite »

by Robert L. Constable

2009

*
Formal Foundations of Computer Security *
| cite »

by Mark Bickford, Robert L. Constable

2008

*
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP *
| cite »

by Robert L. Constable

2008

*
Computational Type Theory -- Extended Version *
| cite »

by Robert L. Constable

2008

*
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus *
| cite »

by Wojciech Moczydlowski, Robert L. Constable

2007

*
Transforming the Academy: Knowledge Formation in the Age of Digital Information *

by Robert L. Constable

January 11, 2007

*
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

*
Enabling Large Scale Coherency Among Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable

2006

*
Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable, Lori Lorigo

2006

*
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics *
| cite »

by Robert L. Constable, Wojciech Moczydlowski

2006

*
Information-Intensive Proof Technology *
| cite »

by Robert L. Constable

2006

*
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

*
Randomness and Free Choice Sequences *

by Robert L. Constable

February 04, 2005

*
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

*
Automated Reasoning in Category Theory *

by Robert L. Constable

October 04, 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

*
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

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

by Robert L. Constable

March 01, 2004

*
Comparing Aspects of Set Theory and Type Theory *

by Robert L. Constable

February 16, 2004

*
Planning Session for Spring Seminar Series *

by Robert L. Constable

January 26, 2004

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

by Robert L. Constable

October 27, 2003

*
An Introduction to Event Systems *

by Robert L. Constable

September 29, 2003

*
Introduction to the Fall Seminar Series *

by Robert L. Constable

September 08, 2003

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

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

2003

*
Practical Reflection in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen, Robert L. Constable

2003

*
A Logic of Events *
| cite »

by Mark Bickford, Robert L. Constable

2003

*
Recent Results in Type Theory and Their Relationship to Automath *
| cite »

by Robert L. Constable

2003

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

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

*
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

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

by Mark Bickford, Robert L. Constable

September 16, 2002

*
Computational Complexity and Induction for Partial Computable Functions in Type Theory *
| cite »

by Robert L. Constable, Karl Crary

2002

*
Naive Computational Type Theory *
| cite »

by Robert L. Constable

2002

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Properties of the Formal Digital Library *

by Robert L. Constable

May 06, 2002

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

by Robert L. Constable

2001-2002

*
Report on the Design of the Formal Digital Library *

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

April 08, 2002

*
Explaining the Formal Digital Library *

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

March 11, 2002

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

by Stuart F. Allen, Robert L. Constable

December 03, 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

*
Processing video streams using event notification systems *

by Robert L. Constable, Mark Bickford

October 15, 2001

*
Logical Aspects of Digital Mathematics Libraries (extended abstract) *
| cite »

by Stuart F. Allen, James L. Caldwell, Robert L. Constable

2001

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable

2001

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable

2001

*
Finite Automata *

by Robert L. Constable

May 16, 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 26, 2001

*
NSF ITR proposal *

by Robert L. Constable, Robert L. Constable

March 12, 2001

*
NSF ITR proposal *

by Robert L. Constable, Robert L. Constable

March 12, 2001

*
How Nuprl Reasons *

by Robert L. Constable

January 29, 2001

*
Research Directions *

by Robert L. Constable

September 25, 2000

*
Reading BAAs and RFPs *

by Robert L. Constable

October 16, 2000

*
Reading BAAs and RFPs (cont.) *

by Robert L. Constable

October 23, 2000

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

by Robert L. Constable

November 13, 2000

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

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

*
Nuprl's Class Theory and Its Applications *
| cite »

by Robert L. Constable, Jason Hickey

2000

*
Intersections, Unions and Games *

by Robert L. Constable, Alexei Kopylov, Aleksey Nogin

December 06, 1999

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

by Robert L. Constable

September 13, 1999

*
Verbalization of High-Level Formal Proofs *
| cite »

by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable

1999

*
Metalogical Frameworks II: Developing a Reflected Decision Procedure *
| cite »

by William Aitken, Robert L. Constable, Judith Underwood

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

*
Semantics and Pragmatics of Reflected Proof *

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

December 01, 1998

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

by Robert L. Constable

October 20, 1998

*
Some Uses of the Intersection Type *

by Stuart F. Allen, Robert L. Constable

May 03, 1999

*
Reflection Mechanisms in Nuprl *

by Stuart F. Allen, Robert L. Constable

November 10, 1998

*
On Modeling Ensemble *

by Robert L. Constable, Jason Hickey

October 27, 1998

*
The Structure of Nuprl's Type Theory *
| cite »

by Robert L. Constable

1997

*
Computability is Ineffable in ZF Set Theory *

by Robert L. Constable

April 01, 1997

*
Discussion of Issues in Logic Library Design *

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

March 03, 1997

*
Formalizing Automata Theory I: Finite Automata *
| cite »

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe

1996

*
Formalizing Automata II: Decidable Properties *
| cite »

by Robert L. Constable, Pavel Naumov

1996

*
The Value of Automated Deduction *
| cite »

by Robert L. Constable

1996

*
Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing *
| cite »

by Robert L. Constable

1996

*
Collaborative Mathematics Environments *
| cite »

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

1996

*
Collaborative Mathematics Environments *

by Robert L. Constable

November 21, 1996

*
Project Direction and Research Problems *

by Robert L. Constable

February 06, 1996

*
Expressing Computational Complexity in Constructive Type Theory *
| cite »

by Robert L. Constable

1995

*
Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995 *
| cite »

by Robert L. Constable

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

*
Representing Computational Complexity in Nuprl *

by Robert L. Constable

November 22, 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

*
Exporting and Reflecting Abstract Meta-mathematics *
| cite »

by Robert L. Constable

1994

*
Theorem Proving with Real Numbers *

by Robert L. Constable

August 31, 1993

*
Project Overview *

by Robert L. Constable

July 01, 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

*
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

*
Lectures on: Classical Proofs as Programs *
| cite »

by Robert L. Constable

1992

*
Metalevel Programming in Constructive Type Theory *
| cite »

by Robert L. Constable

1992

*
Formal Theories and Software Systems: Fundamental Connections Between Computer Science and Logic *
| cite »

by Robert L. Constable

1992

*
Metalogical Frameworks *
| cite »

by David A. Basin, Robert L. Constable

1991

*
Finding Computational Content from Classical Proofs *
| cite »

by Robert L. Constable, Chetan Murthy

1991

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

by Robert L. Constable

1991

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

*
Reflecting the Open-Ended Computation System of Constructive Type Theory *
| cite »

by Robert L. Constable, Stuart F. Allen, Douglas J. Howe

1990

*
Nuprl as a General Logic *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Implementing Metamathematics as an Approach to Automatic Theorem Proving *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments *
| cite »

by Robert L. Constable

1989

*
Collaborative Problem Solving Environment *

by Robert L. Constable

1988

*
Computational Foundations of Basic Recursive Function Theory *
| cite »

by Robert L. Constable, Scott F. Smith

1988

*
Typed Enumeration-Free External Setting for Computing Theory *

by Robert L. Constable

November 03, 1987

*
Partial Objects in Constructive Type Theory *
| cite »

by Scott F. Smith, Robert L. Constable

1987

*
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

*
Formalized Metareasoning in Type Theory *
| cite »

by Todd B. Knoblock, Robert L. Constable

1986

*
Infinite Objects in Type Theory *
| cite »

by Nax P. Mendler, Robert L. Constable, Prakash Panangaden

1986

*
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

*
Constructive Mathematics as a Programming Logic I: Some Principles of Theory *
| cite »

by Robert L. Constable

1985

*
Semantics of Evidence *
| cite »

by Robert L. Constable

1985

*
Universally Closed Classes *

by Robert L. Constable

1984-1985

*
Writing Programs That Construct Proofs *
| cite »

by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates

1984

*
A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS *
| cite »

by Robert L. Constable, James Donahue

July 01, 1979

*
A Programming Logic *
| cite »

by Robert L. Constable, Michael J. O'Donnell

1978

*
A Constructive Programming Logic *

by Robert L. Constable

August 08, 1977

*
Constructive Mathematics and Automatic Program Writers *
| cite »

by Robert L. Constable

1971

Crary, Karl

*
Computational Complexity and Induction for Partial Computable Functions in Type Theory *
| cite »

by Robert L. Constable, Karl Crary

2002

*
Bar-Type Rules *

by Karl Crary

January 25, 2002

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

by Karl Crary

1998

*
Simple, Efficient Object Encoding using Intersection Types *

by Karl Crary

April 14, 1998

*
Type Methodology for Modern Languages and Compilers *

by Karl Crary

February 24, 1998

*
From System F to Typed Assembly Language *

by Karl Crary

September 16, 1997

*
Foundations for the Implementation of Higher-Order Subtyping *
| cite »

by Karl Crary

1997

*
Formal Continuations and Classical Logic *

by Karl Crary

March 10, 1997

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

by Karl Crary

1996-1997

*
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

*
KML *

by Karl Crary

April 30, 1996

Cremer, J. F.

*
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

deBruijn, N. G.

*
Math Vernacular *

by N. G. deBruijn

November 17, 1987

Del Vecchio, Peter

*
Verification of Combinational Logic in Nuprl *
| cite »

by David A. Basin, Peter Del Vecchio

1989

Donahue, James

*
A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS *
| cite »

by Robert L. Constable, James Donahue

July 01, 1979

Eaton, Richard

*
Nuprl’s Inductive Logical Forms *

by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli

September 01, 2015

*
Introduction to EventML *

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

February 03, 2012

*
Work in Progress *

by Richard Eaton

February 20, 2012

*
Wider Deployment of Nuprl *

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

September 28, 2012

*
Impredicative vs Predicative Type Theory *

by Robert L. Constable, Mark Bickford, Richard Eaton

April 13, 2012

*
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

*
Automatic FDL Projections *

by Richard Eaton

September 01, 2006

*
Automating Proofs in Event Logic *

by Mark Bickford, Richard Eaton

August 26, 2005

*
Automating Proofs in Event Logic *

by Mark Bickford, Richard Eaton

March 23, 2006

*
A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. *
| cite »

by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable

2004

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

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

2003

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Report on the Design of the Formal Digital Library *

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

April 08, 2002

*
Explaining the Formal Digital Library *

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

March 11, 2002

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

*
The Nuprl 5 Library *

by Richard Eaton

February 09, 1998

*
Discussion of Issues in Logic Library Design *

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

March 03, 1997

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

by Richard Eaton

October 03, 1995

*
The "Interface" Version of Nuprl *

by Stuart F. Allen, Richard Eaton

November 15, 1994

Egly, Uwe

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

by Uwe Egly

September 22, 1998

Evfimievski, Sasha

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

Fluet, Matthew

*
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

by Matthew Fluet

November 24, 2003

*
Variations on a Proof by Smullyan *

by Matthew Fluet

May 05, 2003

*
The Calculemus Autumn School *

by Christoph Kreitz, Sabina Petride, Matthew Fluet

October 28, 2002

Forester, Max B.

*
Formalizing Constructive Real Analysis *
| cite »

by Max B. Forester

1993

Gent, Ian

*
Search Algorithms in Type Theory *
| cite »

by James L. Caldwell, Ian Gent, Judith Underwood

2000

*
The Enigma of Sat Hill Climbing Procedures *

by Ian Gent

November 10, 1992

Geser, Alfons

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

by Wojciech Moczydlowski, Alfons Geser

2005

Giunchiglia, Fausto

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

by Fausto Giunchiglia, Alan Smaill

1989

Glew, Neal

*
Typed Assembly Language *

by Neal Glew

March 01, 1999

*
Formal Domain Theory *

by Neal Glew

December 05, 1995

Gonthier, Georges

*
Verifying the Four Colour Theorem *

by Georges Gonthier

May 20, 2005

Griffin, Timothy G.

*
Notational Definition and Top-down Refinement for Interactive Proof Development Systems *
| cite »

by Timothy G. Griffin

1988

*
Syntactic Abstraction *

by Timothy G. Griffin

September 22, 1987

*
Using Lemmas *

by Timothy G. Griffin

1984-1985

*
Arithpac *

by Timothy G. Griffin

1984-1985

Guaspari, David

*
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

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

September 01, 2015

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

March 31, 2013

*
Introduction to EventML *

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

February 03, 2012

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

by Mark Bickford, Robert L. Constable, David Guaspari

2010

*
Encoding Pi Calculus *
| cite »

by David Guaspari

2010

*
Formalizing chain replication *

by Mark Bickford, David Guaspari

2006

*
A Programming Logic for Distributed Systems *
| cite »

by Mark Bickford, David Guaspari

2005

Hafizogullari, Ozan

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

*
Continuation of talk on Polymorphic References *

by Ozan Hafizogullari

September 24, 1999

*
Dependence Analysis Through Type Inference *
| cite »

by Ozan Hafizogullari, Christoph Kreitz

1999

*
Automatic Debugging Through Type Inference, Continued *

by Ozan Hafizogullari

November 03, 1998

*
Automatic Debugging Through Type Inference *

by Ozan Hafizogullari

October 06, 1998

*
Dead Code Elimination *

by Ozan Hafizogullari, Christoph Kreitz

January 27, 1998

*
ML-like Type Reconstruction for Nuprl *

by Ozan Hafizogullari

November 26, 1996

Halpern, Joseph Y.

*
Knowledge-based synthesis of distributed systems using event structures *
| cite »

by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

2005

*
Knowledge-Based Synthesis of Distributed Systems Using Event Structures *

by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

2004

Harmelen, Frank Van

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

Harper, Robert W.

*
Lambda Calculus as Basis for Programming Language Design *

by Robert W. Harper

1990-1991

*
The Lambda Calculus as a Basis for Language Design *

by Robert W. Harper

1989-1990

*
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

*
Aspects of the Implementation of Type Theory *
| cite »

by Robert W. Harper

1985

*
Equality *

by Robert W. Harper

1984-1985

*
Type Inference *

by Robert W. Harper

1984-1985

Hayden, Mark

*
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

*
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

*
The Ensemble System *
| cite »

by Mark Hayden

1998

*
A Proof Environment for the Development of Group Communication Systems *
| cite »

by Christoph Kreitz, Mark Hayden, Jason Hickey

1998

*
Formal Methods & Distributed Systems *

by Mark Hayden

1996-1997

*
Group Communication with Functional Languages *

by Mark Hayden

January 28, 1997

Hehner, Rick

*
Programs as Specification *

by Rick Hehner

May 06, 1986

Hickey, Jason

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
Formal Compiler Implementation in a Logical Framework *
| cite »

by Jason Hickey, Aleksey Nogin

2003

*
The MetaPRL Logical Programming Environment *
| cite »

by Jason Hickey

2001

*
Caltech Computer Science *

by Jason Hickey

November 06, 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

*
Nuprl's Class Theory and Its Applications *
| cite »

by Robert L. Constable, Jason Hickey

2000

*
Fast Tactic-Based Theorem Proving *
| cite »

by Jason Hickey, Aleksey Nogin

2000

*
An Object-Oriented Approach to Verifying Group Communication Systems *
| cite »

by Mark Bickford, Jason Hickey

1999

*
Fault-Tolerant Distributed Theorem Proving *
| cite »

by Jason Hickey

1999

*
Specifications and Proofs for Ensemble Layers *
| cite »

by Jason Hickey, Nancy Lynch, Robbert van Renesse

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

*
The Current Projects of the MetaPRL Group *

by Aleksey Nogin, Jason Hickey

April 26, 1999

*
A Programming Environment for Building Reliable High Performance Systems *

by Jason Hickey

February 15, 1999

*
On Modeling Ensemble *

by Robert L. Constable, Jason Hickey

October 27, 1998

*
A Proof Environment for the Development of Group Communication Systems *
| cite »

by Christoph Kreitz, Mark Hayden, Jason Hickey

1998

*
Logical Programming Environments *

by Jason Hickey

March 03, 1998

*
Nuprl-Light: An Implementation Framework for Higher-Order Logics *
| cite »

by Jason Hickey

1997

*
A Semantics of Objects in Type Theory *
| cite »

by Jason Hickey

1997

*
Discussion of Issues in Logic Library Design *

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

March 03, 1997

*
Modules and Libraries *

by Jason Hickey

February 18, 1997

*
Sharing Formal Mathematics and Programming *

by Jason Hickey

1996-1997

*
Nuprl Tutorial *

by Jason Hickey

February 02, 1997

*
Nuprl-Light *

by Jason Hickey, Jason Hickey

1996-1997

*
Nuprl-Light *

by Jason Hickey, Jason Hickey

1996-1997

*
Nuprl-Light *

by Jason Hickey, Jason Hickey

1996-1997

*
Nuprl-Light *

by Jason Hickey, Jason Hickey

1996-1997

*
Formal Objects in Type Theory *

by Jason Hickey

1996-1997

*
Formal Objects in Type Theory Using Very Dependent Types *
| cite »

by Jason Hickey

1996

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

by Jason Hickey

February 13, 1996

*
Verifying HORUS in Nuprl *

by Jason Hickey

November 28, 1995

*
Formal Abstract Data Types and Inheritance *

by Jason Hickey

October 31, 1995

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

by Jason Hickey

1995-1996

*
HORUS Verification Effort *

by Jason Hickey

1995-1996

*
Square-Root Verification *

by Jason Hickey

May 10, 1995

*
Very Dependent Function Space *

by Jason Hickey

1994-1995

*
The Ultimate Programming Machine II: Very Dependent Types *

by Jason Hickey

November 08, 1994

*
The Ultimate Programming Machine *

by Jason Hickey

October 25, 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

*
Formalizing the Theory Concept in Nuprl *

by Jason Hickey

March 15, 1994

*
Formalizing the Theory Mechanism in NuPRL *

by Jason Hickey

March 15, 1994

*
Abstract Programming in Nuprl *

by Jason Hickey

November 23, 1993

Ho, Chi

*
Byzantine Chain Replication *
| cite »

by Robbert van Renesse, Chi Ho, Nicolas Schiper

December 20, 2012

Holland-Minkley, Amanda

*
Nuprl Library Annotation *

by Amanda Holland-Minkley

April 05, 2004

*
A Linguistic View of Constuctive Type Theory *

by Amanda Holland-Minkley

February 02, 2004

*
Planning Proof Content for Communicating Induction *
| cite »

by Amanda Holland-Minkley

2002

*
Automatic generation of texts from Nuprl proofs *

by Amanda Holland-Minkley

February 04, 2002

*
Validating a methodology for natural language generation *

by Amanda Holland-Minkley

March 05, 2001

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

*
Verbalization of High-Level Formal Proofs *
| cite »

by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable

1999

*
Verbalization of High-Level Formal Proofs *

by Amanda Holland-Minkley

February 01, 1999

Horn, Christian

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

*
The Nuprl Proof Development System *
| cite »

by Christian Horn

1988

Howe, Douglas J.

*
HOL Translation (partial) *

by Douglas J. Howe

February 13, 2004

*
Importing HOL Theorems into Nuprl *

by Douglas J. Howe

July 30, 1998

*
A type annotation scheme for Nuprl *
| cite »

by Douglas J. Howe

October 01, 1998

*
Semantic Foundations for Embedding HOL in Nuprl *
| cite »

by Douglas J. Howe

1996

*
Importing Mathematics from HOL into Nuprl *
| cite »

by Douglas J. Howe

1996

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

by Douglas J. Howe, Scott D. Stoller

1994

*
Reasoning About Functional Programs in Nuprl *
| cite »

by Douglas J. Howe

1993

*
Constructive Algorithms in Nuprl *

by Douglas J. Howe

December 01, 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 20, 1992

*
Fefprl *

by Douglas J. Howe, Douglas J. Howe

October 05, 1992

*
Fefprl *

by Douglas J. Howe, Douglas J. Howe

October 05, 1992

*
A Simple Type Theory for Reasoning About Functional Programs *
| cite »

by Douglas J. Howe

1992

*
Some Normalization Properties of Martin-Lof's Type Theory and Applications *
| cite »

by David A. Basin, Douglas J. Howe

1991

*
On computational open-endedness in Martin-Lof's type theory *

by Douglas J. Howe

July 15, 1991

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

*
Reflecting the Open-Ended Computation System of Constructive Type Theory *
| cite »

by Robert L. Constable, Stuart F. Allen, Douglas J. Howe

1990

*
Nuprl as a General Logic *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Implementing Metamathematics as an Approach to Automatic Theorem Proving *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Equality in Lazy Computation Systems *
| cite »

by Douglas J. Howe

1989

*
Automating Reasoning in an Implementation of Constructive Type Theory *
| cite »

by Douglas J. Howe

1988

*
Computational Metatheory in Nuprl *
| cite »

by Douglas J. Howe

1988

*
The Computational Behaviour of Girard's Paradox *
| cite »

by Douglas J. Howe

1987

*
Implementing Number Theory: An Experiment with Nuprl *
| cite »

by Douglas J. Howe

1987

*
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

*
Thesis *

by Douglas J. Howe

1984-1985

*
Theory of Reals *

by Douglas J. Howe

1984-1985

Jackson, Paul B.

*
Constructive General Algebra *

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

*
Finite Multi-Sets *

by Paul B. Jackson

August 19, 1999

*
Constructive Factorization Theory *

by Paul B. Jackson

August 19, 1999

*
Verifying Garbage Collection Algorithms using the PVS Theorem Prover *

by Paul B. Jackson

May 07, 1997

*
Formalizing Automata Theory I: Finite Automata *
| cite »

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe

1996

*
The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide *
| cite »

by Paul B. Jackson

1996

*
Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra *
| cite »

by Paul B. Jackson

1995

*
Developing Set Theory in HOL *

by Paul B. Jackson

February 28, 1995

*
Verifying an Implementation of a Polynomial Algebra ADT *

by Paul B. Jackson

November 29, 1994

*
Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics *
| cite »

by Robert L. Constable, Paul B. Jackson

1994

*
Exploring Abstract Algebra in Constructive Type Theory *
| cite »

by Paul B. Jackson

1994

*
The MIZAR Project *

by Paul B. Jackson

February 15, 1994

*
Defining Polynomials in Constructive Type Theory *

by Paul B. Jackson

1992-1993

*
Editor Demonstration *

by Paul B. Jackson

March 09, 1993

*
Structuring Proofs *

by Douglas J. Howe, Paul B. Jackson

October 27, 1992

*
Nuprl and Its Use in Circuit Design *
| cite »

by Paul B. Jackson

1992

*
Nuprl 3 vs. Nuprl 4 *

by Paul B. Jackson

November 05, 1991

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

by Paul B. Jackson

1991

*
Using Nuprl to Verify Floating Point Hardware *

by Paul B. Jackson

April 17, 1990

*
Logic-Based Knowledge Representation *
| cite »

by Paul B. Jackson

1989

Kamareddine, Fairouz

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

by Robert L. Constable, Fairouz Kamareddine, Twan Laan

2012

Kellison, Ariel

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

by Ariel Kellison, Mark Bickford

November 26, 2019

*
Implementing Euclid's Straightedge and Compass Constructions in Type Theory *
| cite »

by Ariel Kellison, Mark Bickford, Robert L. Constable

2018

Klavins, Eric

*
Some Recent Results in MetaPRL *

by Eric Klavins

April 22, 2002

Kleinberg, Jon

*
A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. *
| cite »

by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable

2004

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

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

2003

Knight, Brent

*
Program Optimization in Type Theory *

by Brent Knight

October 18, 1994

Knoblock, Todd B.

*
Metamathematical Extensibility in Type Theory *
| cite »

by Todd B. Knoblock

1987

*
Metamathematics of Reflection *

by Todd B. Knoblock

April 22, 1987

*
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

*
Formalized Metareasoning in Type Theory *
| cite »

by Todd B. Knoblock, Robert L. Constable

1986

*
Reflective PRL *

by Todd B. Knoblock

1984-1985

*
Writing Programs That Construct Proofs *
| cite »

by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates

1984

Kopylov, Alexei

*
Type Theoretical Foundations for Data Structures, Classes, and Objects *
| cite »

by Alexei Kopylov

2004

*
Verified Implementation of Red-Black Trees *

by Alexei Kopylov

November 10, 2003

*
Dependent Intersection: A New Way of Defining Records in Type Theory *
| cite »

by Alexei Kopylov

2003

*
Representing Red-Black Trees in MetaPRL *

by Alexei Kopylov

March 10, 2003

*
Continuing Discussion of Objects *

by Alexei Kopylov, Robert L. Constable

December 02, 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

*
Representing Objects in Nuplr Type Theory *

by Alexei Kopylov

April 29, 2002

*
Objects *

by Alexei Kopylov

November 19, 2001

*
Record calculus *

by Alexei Kopylov

November 12, 2001

*
Markov's Principle For Propositional Type Theory *
| cite »

by Alexei Kopylov, Aleksey Nogin

2001

*
Kopylov and Nogin CSL Submission *

by Alexei Kopylov

April 02, 2001

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

by Alexei Kopylov, Aleksey Nogin

November 27, 2000

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

by Aleksey Nogin, Alexei Kopylov

December 04, 2000

*
Intersections, Unions and Games *

by Robert L. Constable, Alexei Kopylov, Aleksey Nogin

December 06, 1999

*
Decidability of Linear Affine Logic *

by Alexei Kopylov

November 01, 1999

*
Linear Logic *

by Alexei Kopylov

October 18, 1999

Kozen, Dexter

*
Formalizing Moessner's Theorem in Nuprl *

by Mark Bickford, Dexter Kozen, Alexandra Silva

June 08, 2012

*
Automating Proofs in Category Theory *
| cite »

by Dexter Kozen, Christoph Kreitz, Eva Richter

2006

*
A Proof-Theoretic Approach to Knowledge Acquisition" *

by Dexter Kozen

January 28, 2002

Kreitz, Christoph

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

by Christoph Kreitz

April 26, 2012

*
Wider Deployment of Nuprl *

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

September 28, 2012

*
Introduction to Classic ML *
| cite »

by Christoph Kreitz, Vincent Rahli

2011

*
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

*
Automating Proofs in Category Theory *
| cite »

by Dexter Kozen, Christoph Kreitz, Eva Richter

2006

*
Microsoft's Spec# *

by Christoph Kreitz

April 17, 2006

*
Constructive Proofs and Program Extraction *

by Christoph Kreitz

February 23, 2004

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

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

2003

*
The FDL Navigator: Browsing and Manipulating Formal Content *
| cite »

by Christoph Kreitz

2003

*
The Calculemus Autumn School *

by Christoph Kreitz, Sabina Petride, Matthew Fluet

October 28, 2002

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Enhancing Proof Assistant Systems *

by Christoph Kreitz

February 25, 2002

*
Embedded Ststems *

by Christoph Kreitz, Robert L. Constable

November 05, 2001

*
Proof Automation in Constructive Type Theory *

by Christoph Kreitz

September 17, 2001

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable

2001

*
Proving Hybrid Protocols Correct *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu

2001

*
Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse

2001

*
Connection-Driven Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2001

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable

2001

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

2001

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

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

*
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

*
A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems *
| cite »

by Christoph Kreitz, Stephan Schmitt

2000

*
Dependence Analysis Through Type Inference *
| cite »

by Ozan Hafizogullari, Christoph Kreitz

1999

*
Connection-Based Theorem Proving in Classical and Non-Classical Logics *
| cite »

by Christoph Kreitz, Jens Otten

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

*
A Proof Environment for the Development of Group Communication Systems *
| cite »

by Christoph Kreitz, Mark Hayden, Jason Hickey

1998

*
Formal Reasoning About Communication Systems II: Automated Fast-Track Reconfiguration *
| cite »

by Christoph Kreitz

1998

*
A Matrix Characterization for MELL *
| cite »

by Heiko Mantel, Christoph Kreitz

1998

*
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1998

*
Dead Code Elimination *

by Ozan Hafizogullari, Christoph Kreitz

January 27, 1998

*
Formal Reasoning About Communication Systems I: Embedding ML in Type Theory *
| cite »

by Christoph Kreitz

1997

*
Formal Reasoning about Communication Systems *

by Christoph Kreitz

1996-1997

*
Meta-Synthesis: Deriving Programs That Develop Programs *
| cite »

by Christoph Kreitz

1992

*
Constructive Automata Theory Implemented with the Nuprl Proof Development System *
| cite »

by Christoph Kreitz

1986

Laan, Twan

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

by Robert L. Constable, Fairouz Kamareddine, Twan Laan

2012

Lawall, Julia

*
Proofs by Structural Induction using Partial Evaluation *

by Julia Lawall

April 13, 1993

Leeser, Miriam

*
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

*
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification *
| cite »

by Mark Aagaard, Miriam Leeser

1993

*
Using Nuprl for the Verification and Synthesis of Hardware *
| cite »

by Miriam Leeser

1992

*
Formally Verified Synthesis of Combinational Circuits *
| cite »

by David A. Basin, Geoffrey Brown, Miriam Leeser

1991

Leino, Rustan

*
DEC *

by Rustan Leino

November 19, 1996

Lipton, Jim

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

by Jim Lipton

November 12, 1991

*
Plotkin *

by Jim Lipton

March 13, 1990

*
Logical Relations *

by Jim Lipton

March 06, 1990

*
Intuitionistic ZF *

by Jim Lipton

January 30, 1990

*
Realizabiity for IZF *

by Jim Lipton

March 12, 1987

*
IZF and Recursive Realizability *

by Jim Lipton

March 05, 1987

Liu, Annie

*
A Program Transformation System *

by Annie Liu

1993-1994

Liu, Xiaoming

*
Proving Hybrid Protocols Correct *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu

2001

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable

2001

*
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

Lorigo, Lori

*
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

*
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

by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable

2004

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

by Lori Lorigo

May 03, 2004

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Report on the DARPA PCES PI meeting *

by Robert L. Constable, Lori Lorigo, Mark Bickford

October 29, 2001

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

2001

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

Luchangco, Victor

*
A Formal Framework for Modeling Memory *

by Victor Luchangco

February 22, 1999

Lynch, Nancy

*
Specifications and Proofs for Ensemble Layers *
| cite »

by Jason Hickey, Nancy Lynch, Robbert van Renesse

1999

Madden, Peter

*
Automatic Program Optimization Via the Transformation of Nuprl Synthesis Proofs *
| cite »

by Peter Madden

1988

Mannion, Conal

*
Notation and Computer Aided Mathematics *

by Conal Mannion

December 06, 1994

*
Reasoning about Scientific Programs *

by Conal Mannion, Stuart F. Allen

1993-1994

*
Formalizing Hamiltonian Dynamics *

by Conal Mannion

November 09, 1993

Manohar, Rajit

*
A Methodology for Designing Asynchronous Circuits *

by Rajit Manohar

May 10, 1999

Mantel, Heiko

*
Principles of Stepwise Refinement *

by Heiko Mantel

November 22, 1999

*
A Matrix Characterization for MELL *
| cite »

by Heiko Mantel, Christoph Kreitz

1998

Mayr, Tobias

*
SupInf *

by Tobias Mayr

September 23, 1997

McAllister, David

*
TBA *

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

May 04, 1993

*
TBA *

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

April 08, 1988

*
TBA *

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

October 13, 1987

*
The ONTIC System *

by David McAllister

October 06, 1987

Melis, Erica

*
Proof presentation in the Omega system *

by Erica Melis

October 25, 1999

*
Knowledge-Based Proof Planning *

by Erica Melis

April 19, 1999

Mendler, Nax P.

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

by Nax P. Mendler

1990 Summ

*
Polymorphism Is Not Set Theoretic *

by Nax P. Mendler

February 14, 1990

*
Inductive Definition in Type Theory *
| cite »

by Nax P. Mendler

1988

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

by Nax P. Mendler

1987

*
Strong Normalization in Lambda ^{2} *

by Nax P. Mendler

October 02, 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

*
Recursive Definitions in Type Theory *
| cite »

by Robert L. Constable, Nax P. Mendler

1985

*
PP-lambda in Nuprl *

by Nax P. Mendler

1984-1985

*
Denotational Semantics *

by Nax P. Mendler

1984-1985

*
Partial Recursive Functions *

by Nax P. Mendler

1984-1985

Misra, Jaydev

*
Structured Concurrent Programming *

by Jaydev Misra

September 15, 2006

Mitchell, John

*
Empty Types *

by John Mitchell

September 25, 1986

Moczydlowski, Wojciech

*
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus *
| cite »

by Wojciech Moczydlowski, Robert L. Constable

2007

*
A Dependent Set Theory *

by Wojciech Moczydlowski

2007

*
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics *
| cite »

by Robert L. Constable, Wojciech Moczydlowski

2006

*
A Normalizing Intuitionistic Set Theory with Inaccessible Sets *
| cite »

by Wojciech Moczydlowski

2006

*
Normalization of intuitionistic set theories. *
| cite »

by Wojciech Moczydlowski

2006

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

by Wojciech Moczydlowski, Alfons Geser

2005

*
Extraction in IZF *

by Wojciech Moczydlowski

February 25, 2005

*
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

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

by Wojciech Moczydlowski

November 04, 2005

*
Coq and Nuprl *

by Wojciech Moczydlowski

July 27, 2004

Moore, J Strother

*
An ACL2 Demo *

by J Strother Moore

October 07, 2002

Moran, Evan

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

by Evan Moran

October 19, 2012

*
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

*
Unions and Unboxed Quotients *

by Evan Moran

September 23, 2005

*
Non-existence of Unions *

by Evan Moran

March 04, 2005

*
Separativeness and the Structure of the Singletons *

by Evan Moran

October 18, 2004

*
Reversing Howe's Substitution Rule *

by Evan Moran

September 27, 2004

*
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

*
CFZ From Below (continued) *

by Evan Moran

April 19, 2004

*
CFZ From Below *

by Evan Moran

April 12, 2004

*
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

*
On Howe's Importation of HOL into Nuprl *

by Evan Moran

September 29, 1998

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

by Evan Moran

April 07, 1998

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

by Evan Moran

April 08, 1997

*
CZF, Type Theory, and Nuprl-Light *

by Evan Moran

April 01, 1997

Moschovakis, Joan Rand

*
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

Mota, Francisco

*
Constructive Topology - A Theory of Observation *

by Francisco Mota

October 15, 2014

*
Synthetic Topology in NuPRL *

by Francisco Mota, Mark Bickford

December 03, 2014

Moten, Roderick

*
Concurrent Refinement in Nuprl *
| cite »

by Roderick Moten

1997

*
Design of the Nuprl Refiner *

by Roderick Moten

September 26, 1995

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

by Roderick Moten

April 04, 1995

*
Tactic Trees in eXene *

by Roderick Moten

September 22, 1992

Murthy, Chetan

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

by Chetan Murthy

February 14, 1995

*
The Engineering Aspects of Proof-Environment Design *

by Chetan Murthy

January 24, 1995

*
TLA *

by Scott D. Stoller, Chetan Murthy

November 01, 1994

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

by Chetan Murthy

September 03, 1993

*
A Computational Analysis of Girard's Translation and LC *
| cite »

by Chetan Murthy

1992

*
Finding Computational Content from Classical Proofs *
| cite »

by Robert L. Constable, Chetan Murthy

1991

*
An Evaluation Semantics for Classical Proofs *
| cite »

by Chetan Murthy

1991

*
A Constructive Proof of Higman's Lemma *
| cite »

by Chetan Murthy, James R. Russell

1990

*
Extracting Constructive Content from Classical Proofs *
| cite »

by Chetan Murthy

1990

Naumov, Pavel

*
Zeno *

by Pavel Naumov

January 25, 2002

*
Simple Imperative Programming *

by Pavel Naumov

February 26, 2002

*
Importing Isabelle Formal Mathematics into NuPRL *

by Pavel Naumov

March 08, 1999

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

by Pavel Naumov

September 08, 1998

*
Formalizing Reference Types in Nuprl *
| cite »

by Pavel Naumov

1998

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

by Pavel Naumov

March 10, 1998

*
References in Type Theory *

by Pavel Naumov

November 25, 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

*
Formalizing Automata Theory I: Finite Automata *
| cite »

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe

1996

*
Formalizing Automata II: Decidable Properties *
| cite »

by Robert L. Constable, Pavel Naumov

1996

*
Turing Machine Basics *

by Pavel Naumov

November 01, 1996

Nogin, Aleksey

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
Formal Compiler Implementation in a Logical Framework *
| cite »

by Jason Hickey, Aleksey Nogin

2003

*
Quotient Types: A Modular Approach *
| cite »

by Aleksey Nogin

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

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

by Aleksey Nogin

November 26, 2001

*
Trip Report *

by Aleksey Nogin

October 22, 2001

*
Markov's Principle for Propositional Type Theory *

by Aleksey Nogin

August 20, 2001

*
Markov's Principle For Propositional Type Theory *
| cite »

by Alexei Kopylov, Aleksey Nogin

2001

*
Writing Constructive Proofs Yielding Efficient Extracted Programs *
| cite »

by Aleksey Nogin

2001

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

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

*
Internalizing proofs and provability *

by Aleksey Nogin

February 19, 2001

*
Summer Reports *

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

September 04, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 18, 2000

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

by Alexei Kopylov, Aleksey Nogin

November 27, 2000

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

by Aleksey Nogin, Alexei Kopylov

December 04, 2000

*
Fast Tactic-Based Theorem Proving *
| cite »

by Jason Hickey, Aleksey Nogin

2000

*
Intersections, Unions and Games *

by Robert L. Constable, Alexei Kopylov, Aleksey Nogin

December 06, 1999

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

by Aleksey Nogin

April 10, 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

*
The Status of the Meta-Prl Project *

by Aleksey Nogin

October 04, 1999

*
The Current Projects of the MetaPRL Group *

by Aleksey Nogin, Jason Hickey

April 26, 1999

*
Speeding Up the MetaPRL Refiner *

by Aleksey Nogin

February 08, 1999

*
Formal Models for Nuprl Evaluator *

by Aleksey Nogin

March 24, 1998

Nogina, Elena

*
On continuity of computable real functions *

by Elena Nogina

May 01, 2000

O'Donnell, Michael J.

*
Connecting Formal Semantics to Constructive Intuitions *

by Michael J. O'Donnell

July 06, 1993

*
A Programming Logic *
| cite »

by Robert L. Constable, Michael J. O'Donnell

1978

O'Leary, John

*
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

Otten, Jens

*
Matrix-Based Constructive Theorem Proving *
| cite »

by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka

2000

*
Connection-Based Theorem Proving in Classical and Non-Classical Logics *
| cite »

by Christoph Kreitz, Jens Otten

1999

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

by Jens Otten, Stephan Schmitt

June 23, 1998

Panangaden, Prakash

*
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

Paulin-Mohring, Christine

*
Recursive Types in Coq *

by Christine Paulin-Mohring

September 08, 1994

Petride, Sabina

*
Knowledge-based synthesis of distributed systems using event structures *
| cite »

by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

2005

*
Knowledge-Based Synthesis of Distributed Systems Using Event Structures *

by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

2004

*
Uri Abraham's Models for Concurrency *

by Robert L. Constable, Sabina Petride

January 27, 2003

*
The Calculemus Autumn School *

by Christoph Kreitz, Sabina Petride, Matthew Fluet

October 28, 2002

Pientka, Brigitte

*
Connection-Driven Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2001

*
Matrix-Based Constructive Theorem Proving *
| cite »

by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka

2000

*
Matrix-Based Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2000

*
Automating Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1999

*
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1998

*
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs *

by Brigitte Pientka

May 05, 1998

*
A Uniform Rippling Approach for Instantiating Free Variables *

by Brigitte Pientka

December 02, 1997

Pingali, Keshav

*
Distributed Snapshot Algorithms *

by Keshav Pingali

February 17, 2003

*
Collaborative Mathematics Environments *
| cite »

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

1996

Poernomo, Iman

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

by Iman Poernomo

December 08, 2003

Poetzsch, Arnd

*
Formalizing Program Synthesis *

by Arnd Poetzsch

April 27, 1993

Rahli, Vincent

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

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

2019

*
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

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

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

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

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 2017

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

November 15, 2017

*
A Nominal Exploration of Intuitionism *

by Vincent Rahli, Mark Bickford

January 18, 2016

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

September 01, 2015

*
Coq as a Metatheory for Nuprl with Bar Induction *

by Vincent Rahli, Mark Bickford

September 14, 2015

*
Nuprl’s Inductive Logical Forms *

by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli

September 01, 2015

*
Developing Correctly Replicated Databases Using Formal Tools *

by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

June 23, 2014

*
A Type Theory with Partial Equivalence Relations as Types *

by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli

May 12, 2014

*
Towards a Formally Verified Proof Assistant *

by Abhishek Anand, Vincent Rahli

July 14, 2014

*
A Generic Approach to Proofs about Substitution *

by Abhishek Anand, Vincent Rahli

July 17, 2014

*
A Type Theory with Partial Equivalence Relations as Types *

by Vincent Rahli

September 10, 2014

*
There Are No Discontinuous Real Functions *

by Mark Bickford, Vincent Rahli

October 08, 2014

*
Nominal Type Theory *

by Mark Bickford, Vincent Rahli

October 29, 2014

*
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

*
A verified proof assistant *

by Vincent Rahli, Abhishek Anand

October 30, 2013

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

by Abhishek Anand, Vincent Rahli

November 20, 2013

*
The Logic of Events, a framework to reason about distributed systems *
| cite »

by Mark Bickford, Vincent Rahli, Robert L. Constable

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

*
Interfacing with Proof Assistants for Domain Specific Programming Using EventML *
| cite »

by Vincent Rahli

July 11, 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

*
Simple Consensus Algorithm *

by Robert L. Constable, Mark Bickford, Vincent Rahli

October 28, 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

*
Introduction to Classic ML *
| cite »

by Christoph Kreitz, Vincent Rahli

2011

Reitblatt, Mark

*
ACL2 Tutorial *

by Mark Reitblatt

March 27, 2014

*
Recent work with Coq *

by Mark Reitblatt

May 11, 2012

Remidde, Ettore

*
GOLEM *

by Ettore Remidde

October 24, 1995

Richter, Eva

*
Automating Proofs in Category Theory *
| cite »

by Dexter Kozen, Christoph Kreitz, Eva Richter

2006

Rodeh, Ohad

*
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

Rowe, Reuben

*
Automated Reasoning in Herbrand Structures *

by Liron Cohen, Reuben Rowe, Yoni Zohar

June 03, 2019

*
Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent *
| cite »

by Liron Cohen, Reuben Rowe

July 01, 2018

Russell, James R.

*
A Constructive Proof of Higman's Lemma *
| cite »

by Chetan Murthy, James R. Russell

1990

Sasaki, James T.

*
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

*
Extracting Efficient Code from Constructive Proofs *
| cite »

by James T. Sasaki

1985

*
Optimizing Ext *

by James T. Sasaki

1984-1985

Schiper, Nicolas

*
Developing Correctly Replicated Databases Using Formal Tools *

by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

June 23, 2014

*
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

*
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

*
Byzantine Chain Replication *
| cite »

by Robbert van Renesse, Chi Ho, Nicolas Schiper

December 20, 2012

Schlimm, Dirk

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

by Dirk Schlimm

April 24, 1998

Schmitt, Stephan

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

2001

*
Matrix-Based Constructive Theorem Proving *
| cite »

by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka

2000

*
A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems *
| cite »

by Christoph Kreitz, Stephan Schmitt

2000

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

by Stephan Schmitt

May 22, 2000

*
An Efficient Refiner for First-order Intuitionistic Logic *

by Stephan Schmitt

February 28, 2000

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

by Jens Otten, Stephan Schmitt

June 23, 1998

Schwartzbach, Michael

*
Continuation of Categorial Models of Nuprl *

by Michael Schwartzbach

October 28, 1986

*
Categorical Models of Nuprl *

by Michael Schwartzbach

October 21, 1986

Schwichtenberg, Helmut

*
Program Development for Proof Transformations *

by Helmut Schwichtenberg

October 12, 1994

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

by Helmut Schwichtenberg

September 29, 1992

Sernaker, Sarah

*
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

*
Constructive Reading of Classical Logic *

by Robert L. Constable, Sarah Sernaker

2015

Shan, Chung-chieh

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

by Chung-chieh Shan

December 02, 2011

Shankar, N

*
PVS *

by N Shankar

March 24, 1992

Shvartsman, Alex

*
A Reconfigurable Atomic Memory Service for Dynamic Networks *

by Alex Shvartsman

March 24, 2003

Silva, Alexandra

*
Formalizing Moessner's Theorem in Nuprl *

by Mark Bickford, Dexter Kozen, Alexandra Silva

June 08, 2012

Smaill, Alan

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

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

by Fausto Giunchiglia, Alan Smaill

1989

Smith, Scott F.

*
Partial Objects in Type Theory *
| cite »

by Scott F. Smith

1989

*
Computational Foundations of Basic Recursive Function Theory *
| cite »

by Robert L. Constable, Scott F. Smith

1988

*
Partial Objects *

by Scott F. Smith

November 24, 1987

*
Domains in Type Theory *

by Scott F. Smith

November 10, 1987

*
Partial Objects in Constructive Type Theory *
| cite »

by Scott F. Smith, Robert L. Constable

1987

*
Bar Types *

by Scott F. Smith

March 18, 1987

*
Term Model Semantics and Tait Computability Method *

by Scott F. Smith

March 11, 1987

*
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

*
Defining Lambda-prl and Its Extensions *

by Scott F. Smith

1984-1985

Smolka, Steffen

*
Isabelle Tutorial *

by Steffen Smolka

March 18, 2014

Stansifer, Ryan

*
Marhew's Principle *

by Ryan Stansifer

1984-1985

*
Prolog *

by Ryan Stansifer, Stuart F. Allen

1984-1985

Stehr, Mark-Oliver

*
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

Stevens, Andrew

*
20BJ as a Meta-logical Framework *

by Andrew Stevens

April 21, 1990

*
Rational Reconstruction of Boyer and Moore Prover *

by Andrew Stevens

December 01, 1987

Stoller, Scott D.

*
TLA *

by Scott D. Stoller, Chetan Murthy

November 01, 1994

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

by Douglas J. Howe, Scott D. Stoller

1994

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

by Scott D. Stoller

March 29, 1994

*
How to Integrate Set Theory and Computation? *

by Scott D. Stoller

September 14, 1993

*
Semantics *

by Scott D. Stoller

March 30, 1993

*
Semantics of the Nuprl Type Theory *

by Scott D. Stoller

March 16, 1993

Stump, Aarong

*
Proof Tools and Correct Program Development *

by Aarong Stump

February 03, 2003

Tate, Ross

*
Issues in Constructive Type Theory *

by Ross Tate

September 14, 2012

Trostle, Anne

*
Finding the Maximum Segment Sum *

by Anne Trostle

January 22, 2014

*
A Fast Algorithm for the Integer Square Root *

by Anne Trostle, Mark Bickford

June 09, 2014

*
Logical Investigations, with the Nuprl Proof Assistant *

by Robert L. Constable, Anne Trostle

July 22, 2014

*
An Algorithm for the Greatest Common Divisor *

by Anne Trostle

October 01, 2013

Underwood, Judith

*
Search Algorithms in Type Theory *
| cite »

by James L. Caldwell, Ian Gent, Judith Underwood

2000

*
Metalogical Frameworks II: Developing a Reflected Decision Procedure *
| cite »

by William Aitken, Robert L. Constable, Judith Underwood

1999

*
Classical Tools for Constructive Proof Search *
| cite »

by James L. Caldwell, Judith Underwood

1996

*
Aspects of the Computational Content of Proofs *
| cite »

by Judith Underwood

1994

*
A Constructive Completeness Proof for Intuitionistic Predicate Calculus *

by Judith Underwood

February 01, 1994

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

by Judith Underwood

1993

*
Extraction *

by Judith Underwood

March 16, 1993

*
A Constructive Completeness Proof for the Intuitionistic Propositional Calculus *
| cite »

by Judith Underwood

1990

Uribe, Juan

*
Formalizing Automata Theory I: Finite Automata *
| cite »

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe

1996

Vafeiadou, Garyfallia

*
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

van Dalen, Dirk

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

by Dirk van Dalen

June 26, 1998

van Renesse, Robbert

*
Developing Correctly Replicated Databases Using Formal Tools *

by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

June 23, 2014

*
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

*
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

*
Byzantine Chain Replication *
| cite »

by Robbert van Renesse, Chi Ho, Nicolas Schiper

December 20, 2012

*
Investigating Correct-by-Construction Attack-Tolerant Systems *
| cite »

by Robert L. Constable, Mark Bickford, Robbert van Renesse

2010

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable

2001

*
Proving Hybrid Protocols Correct *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu

2001

*
Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse

2001

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable

2001

*
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

*
Specifications and Proofs for Ensemble Layers *
| cite »

by Jason Hickey, Nancy Lynch, Robbert van Renesse

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

Vardi, Moshe

*
A Conversation with Moshe Vardi *

by Moshe Vardi

November 18, 2011

Vavasis, Steve

*
Collaborative Mathematics Environments *
| cite »

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

1996

Vogels, Werner

*
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

Walker, David

*
Regions, part 2: The Capability Calculus *

by David Walker

November 15, 1999

*
An Introduction to Region Inference *

by David Walker

November 08, 1999

Weirich, Stephanie

*
Intensional Polymorphism in Type-Erasure Semantics *

by Stephanie Weirich

April 28, 1998

Werner, Benjamin

*
Extraction of Programs *

by Benjamin Werner

1993-1994

Wilson, Todd

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

by Todd Wilson

July 11, 1996

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

by Todd Wilson

March 26, 1996

*
Motivation: Basis of a Set Theory for Nuprl *

by Todd Wilson

February 21, 1995

*
Computer Algebra, Theorem Proving, and Types *

by Todd Wilson

October 04, 1994

Wu, Jason

*
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 Discussion in Consensus *

by Jason Wu

February 10, 2012

*
Adding Shared Memory to the General Process Model *

by Jason Wu

April 20, 2012

Yan, Thomas

*
Gröbner Basis *

by Thomas Yan

September 20, 1994

*
Hilbert Basis Function *

by Thomas Yan

March 01, 1994

Zippel, Richard

*
Collaborative Mathematics Environments *
| cite »

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

1996

*
The MathBus Term Structure *

by Richard Zippel

1995-1996

Zohar, Yoni

*
Automated Reasoning in Herbrand Structures *

by Liron Cohen, Reuben Rowe, Yoni Zohar

June 03, 2019