# Knowledge Base list of Seminars

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

## List by Year

399 results

2014

*
Synthetic Topology in NuPRL *

by Francisco Mota, Mark Bickford

December 03, 2014

*
From Replicated Databases to Ensembles of Collaborating Robots *

by Abhishek Anand, Mark Bickford

November 19, 2014

*
Coinduction in Coq *

by Abhishek Anand

November 12, 2014

*
Nominal Type Theory *

by Mark Bickford, Vincent Rahli

October 29, 2014

*
Topics in Type Theory *

by Abhishek Anand, Robert L. Constable, Mark Bickford

October 22, 2014

*
Constructive Topology - A Theory of Observation *

by Francisco Mota

October 15, 2014

*
There Are No Discontinuous Real Functions *

by Mark Bickford, Vincent Rahli

October 08, 2014

*
Synthesizing Protocols using the Logic of Events and EventML *

by Robert L. Constable, Mark Bickford

September 17, 2014

*
A Type Theory with Partial Equivalence Relations as Types *

by Vincent Rahli

September 10, 2014

*
Formalizing Bishop's Constructive Analysis in Constructive Type Theory *

by Mark Bickford, Robert L. Constable

April 10, 2014

*
ACL2 Tutorial *

by Mark Reitblatt

March 27, 2014

*
Isabelle Tutorial *

by Steffen Smolka

March 18, 2014

2013

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

by Abhishek Anand, Vincent Rahli

November 20, 2013

*
Quotient Types in Nuprl *

by Mark Bickford

November 13, 2013

*
Nuprl as a Programming Assistant *

by Robert L. Constable

November 06, 2013

*
A verified proof assistant *

by Vincent Rahli, Abhishek Anand

October 30, 2013

*
An Extension of OCaml's Type Theory *

by Robert L. Constable

October 23, 2013

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

by Abhishek Anand

October 09, 2013

*
The power of bar induction in constructive type theory *

by Mark Bickford

September 25, 2013

2012

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

by Jason Wu

November 09, 2012

*
Realizing Bar Induction in Nuprl *

by Mark Bickford

October 26, 2012

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

by Evan Moran

October 19, 2012

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

by Robert L. Constable, Mark Bickford, Abhishek Anand

October 12, 2012

*
Wider Deployment of Nuprl *

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

September 28, 2012

*
The Type Base and Undecidability in Type Theory *

by Abhishek Anand

September 21, 2012

*
Issues in Constructive Type Theory *

by Ross Tate

September 14, 2012

*
Introduction to the Fall Seminar Series *

by Robert L. Constable

September 07, 2012

*
Intuitionistic Ancestral Logic *

by Liron Cohen

July 12, 2012

2011-2012

*
Recent work with Coq *

by Mark Reitblatt

May 11, 2012

*
Adding Communication Primitives to the Nuprl Evaluator *

by Mark Bickford

May 04, 2012

*
Adding Shared Memory to the General Process Model *

by Jason Wu

April 20, 2012

*
Impredicative vs Predicative Type Theory *

by Robert L. Constable, Mark Bickford, Richard Eaton

April 13, 2012

*
Reviewing Nuprl *

by Robert L. Constable

March 09, 2012

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

by Robert L. Constable

February 24, 2012

*
A Discussion in Consensus *

by Jason Wu

February 10, 2012

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

by Chung-chieh Shan

December 02, 2011

*
A Conversation with Moshe Vardi *

by Moshe Vardi

November 18, 2011

*
Simple Consensus Algorithm *

by Robert L. Constable, Mark Bickford, Vincent Rahli

October 28, 2011

*
Analyzing Access Control Logics Using Evidence Semantics *

by Robert L. Constable

September 23, 2011

*
NuPRL Demo *

by Mark Bickford

September 16, 2011

*
Seminar History and Initial Planning Meeting *

by Robert L. Constable

September 09, 2011

*
Seminar History and Initial Planning Meeting *

by Robert L. Constable, Robert L. Constable

September 09, 2011

2006-2007

*
Structured Concurrent Programming *

by Jaydev Misra

September 15, 2006

2005-2006

*
Microsoft's Spec# *

by Christoph Kreitz

April 17, 2006

*
A Semantics for Abstract Atoms in Nuprl *

by Stuart F. Allen

March 31, 2006

*
Automating Proofs in Event Logic *

by Mark Bickford, Richard Eaton

March 23, 2006

*
Event Systems: Introduction to the Logic of Events *

by Mark Bickford

February 17, 2006

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

by Mark Bickford

November 18, 2005

*
Unions and Unboxed Quotients *

by Evan Moran

September 23, 2005

*
Automated Proofs in Event Logic *

by Mark Bickford

September 16, 2005

*
Automating Proofs in Event Logic *

by Mark Bickford, Richard Eaton

August 26, 2005

2004-2005

*
Urelements in Computational Type Theory *

by Mark Bickford

November 11, 2005

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

by Wojciech Moczydlowski

November 04, 2005

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

by Evan Moran

October 28, 2005

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

by Evan Moran

October 14, 2005

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

by Evan Moran

September 30, 2005

*
Verifying the Four Colour Theorem *

by Georges Gonthier

May 20, 2005

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

by Stuart F. Allen

April 15, 2005

*
Non-existence of Unions *

by Evan Moran

March 04, 2005

*
Extraction in IZF *

by Wojciech Moczydlowski

February 25, 2005

*
Real-time Message Automata *

by Mark Bickford

February 11, 2005

*
Randomness and Free Choice Sequences *

by Robert L. Constable

February 04, 2005

*
Anchoring Expository Text in Formal Mathematics *

by Stuart F. Allen

December 06, 2004

*
Mark Presentation *

by Mark Bickford

November 29, 2004

*
Remarks on Nijmegen trip *

by Robert L. Constable

November 08, 2004

*
Foundations for the Management of Formal Mathematical Knowledge *

by Robert L. Constable

October 25, 2004

*
Separativeness and the Structure of the Singletons *

by Evan Moran

October 18, 2004

*
Automated Reasoning in Category Theory *

by Robert L. Constable

October 04, 2004

*
Reversing Howe's Substitution Rule *

by Evan Moran

September 27, 2004

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

by Wojciech Moczydlowski

September 20, 2004

*
Set-theoretical models of type theory *

by Wojciech Moczydlowski

September 13, 2004

2004 Summ

*
Coq and Nuprl *

by Wojciech Moczydlowski

July 27, 2004

2003-2004

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

by Lori Lorigo

May 03, 2004

*
The Logic of Events and Event Structure Patterns *

by Mark Bickford

April 26, 2004

*
CFZ From Below (continued) *

by Evan Moran

April 19, 2004

*
CFZ From Below *

by Evan Moran

April 12, 2004

*
Nuprl Library Annotation *

by Amanda Holland-Minkley

April 05, 2004

*
Type Theory as a Legacy from Logicism *

by Stuart F. Allen

March 08, 2004

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

by Robert L. Constable

March 01, 2004

*
Constructive Proofs and Program Extraction *

by Christoph Kreitz

February 23, 2004

*
Comparing Aspects of Set Theory and Type Theory *

by Robert L. Constable

February 16, 2004

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

by Stuart F. Allen

February 09, 2004

*
A Linguistic View of Constuctive Type Theory *

by Amanda Holland-Minkley

February 02, 2004

*
Planning Session for Spring Seminar Series *

by Robert L. Constable

January 26, 2004

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

by Iman Poernomo

December 08, 2003

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

by Stuart F. Allen

December 01, 2003

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

by Matthew Fluet

November 24, 2003

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

by Stuart F. Allen

November 17, 2003

*
Verified Implementation of Red-Black Trees *

by Alexei Kopylov

November 10, 2003

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

by Robert L. Constable

October 27, 2003

*
Leader Election Protocols *

by Mark Bickford

October 06, 2003

*
An Introduction to Event Systems *

by Robert L. Constable

September 29, 2003

*
Discussion of Methods of Sharing Formal Mathematics *

by Evan Moran

September 22, 2003

*
Bridges Between Set Theory and Type Theory *

by Evan Moran

September 15, 2003

*
Introduction to the Fall Seminar Series *

by Robert L. Constable

September 08, 2003

2002-2003

*
Variations on a Proof by Smullyan *

by Matthew Fluet

May 05, 2003

*
Continuing Discussion of the NSDL *

by Robert L. Constable

April 14, 2003

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

by Robert L. Constable

March 31, 2003

*
A Reconfigurable Atomic Memory Service for Dynamic Networks *

by Alex Shvartsman

March 24, 2003

*
Representing Red-Black Trees in MetaPRL *

by Alexei Kopylov

March 10, 2003

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

by Regina Barzilay

March 03, 2003

*
Implementing the Logic of Events *

by Mark Bickford

February 24, 2003

*
Distributed Snapshot Algorithms *

by Keshav Pingali

February 17, 2003

*
Proof Tools and Correct Program Development *

by Aarong Stump

February 03, 2003

*
Uri Abraham's Models for Concurrency *

by Robert L. Constable, Sabina Petride

January 27, 2003

*
Continuing Discussion of Objects *

by Alexei Kopylov, Robert L. Constable

December 02, 2002

*
Classes and Objects *

by Robert L. Constable

November 25, 2002

*
Continuing on Objects and Classes *

by Alexei Kopylov

November 18, 2002

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

by Alexei Kopylov

November 11, 2002

*
The Calculemus Autumn School *

by Christoph Kreitz, Sabina Petride, Matthew Fluet

October 28, 2002

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

by Regina Barzilay

October 21, 2002

*
An ACL2 Demo *

by J Strother Moore

October 07, 2002

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

by Mark Bickford

September 30, 2002

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

by Mark Bickford, Robert L. Constable

September 16, 2002

2001-2002

*
Properties of the Formal Digital Library *

by Robert L. Constable

May 06, 2002

*
Representing Objects in Nuplr Type Theory *

by Alexei Kopylov

April 29, 2002

*
Some Recent Results in MetaPRL *

by Eric Klavins

April 22, 2002

*
Report on the Design of the Formal Digital Library *

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

April 08, 2002

*
Recent Results on the PCES Project *

by Mark Bickford

April 01, 2002

*
Arithmetic module for MetaPRL: rules and Arith tactic *

by Yegor Bryukhov

March 25, 2002

*
Explaining the Formal Digital Library *

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

March 11, 2002

*
The Abstract Term Type *

by Regina Barzilay

March 04, 2002

*
Enhancing Proof Assistant Systems *

by Christoph Kreitz

February 25, 2002

*
Review of Theorem Provers Outside Cornell part 2 *

by Aleksey Nogin

February 18, 2002

*
Review of Theorem Provers Outside Cornell part 1 *

by Aleksey Nogin

February 11, 2002

*
Automatic generation of texts from Nuprl proofs *

by Amanda Holland-Minkley

February 04, 2002

*
A Proof-Theoretic Approach to Knowledge Acquisition" *

by Dexter Kozen

January 28, 2002

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

by Stuart F. Allen, Robert L. Constable

December 03, 2001

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

by Aleksey Nogin

November 26, 2001

*
Objects *

by Alexei Kopylov

November 19, 2001

*
Record calculus *

by Alexei Kopylov

November 12, 2001

*
Embedded Ststems *

by Christoph Kreitz, Robert L. Constable

November 05, 2001

*
Report on the DARPA PCES PI meeting *

by Robert L. Constable, Lori Lorigo, Mark Bickford

October 29, 2001

*
Trip Report *

by Aleksey Nogin

October 22, 2001

*
Processing video streams using event notification systems *

by Robert L. Constable, Mark Bickford

October 15, 2001

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

by Mark Bickford

September 24, 2001

*
Proof Automation in Constructive Type Theory *

by Christoph Kreitz

September 17, 2001

*
Markov's Principle for Propositional Type Theory *

by Aleksey Nogin

August 20, 2001

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

by Robert L. Constable

2001-2002

2000-2001

*
Modular approach to formalization of the quotient types *

by Aleksey Nogin

April 23, 2001

*
Modular approach to quotient and other types *

by Aleksey Nogin

April 16, 2001

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

by Aleksey Nogin

April 09, 2001

*
Kopylov and Nogin CSL Submission *

by Alexei Kopylov

April 02, 2001

*
NSF ITR proposal *

by Robert L. Constable, Robert L. Constable

March 26, 2001

*
NSF ITR proposal *

by Robert L. Constable, Robert L. Constable

March 12, 2001

*
Validating a methodology for natural language generation *

by Amanda Holland-Minkley

March 05, 2001

*
Internalizing proofs and provability *

by Aleksey Nogin

February 19, 2001

*
Reflection in First-Order Logic *

by Eli Barzilay

February 12, 2001

*
Automated Higher-Order Complexity Analysis *

by Ralph Benzinger

February 05, 2001

*
How Nuprl Reasons *

by Robert L. Constable

January 29, 2001

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

by Aleksey Nogin, Alexei Kopylov

December 04, 2000

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

by Alexei Kopylov, Aleksey Nogin

November 27, 2000

*
Latest results about reflection (TENTATIVE) *

by Eli Barzilay

November 20, 2000

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

by Robert L. Constable

November 13, 2000

*
Caltech Computer Science *

by Jason Hickey

November 06, 2000

*
Reading BAAs and RFPs (cont.) *

by Robert L. Constable

October 23, 2000

*
Reading BAAs and RFPs *

by Robert L. Constable

October 16, 2000

*
Reflected Lambda Calculus *

by Sergei Artemov

October 02, 2000

*
Research Directions *

by Robert L. Constable

September 25, 2000

*
Summer Reports *

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

September 18, 2000

*
Summer Reports *

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

September 11, 2000

*
Summer Reports *

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

September 04, 2000

1999-2000

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

by Stephan Schmitt

May 22, 2000

*
On continuity of computable real functions *

by Elena Nogina

May 01, 2000

*
Stability of intuitionistic systems *

by Sergei Artemov

April 24, 2000

*
Randomized Programming and Probabilistic Reasoning in Type Theory *

by James Cheney

April 17, 2000

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

by Aleksey Nogin

April 10, 2000

*
Reflection Part II *

by Eli Barzilay

April 03, 2000

*
Continuation on reflection *

by Mark Bickford

March 13, 2000

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

by Eli Barzilay

March 06, 2000

*
An Efficient Refiner for First-order Intuitionistic Logic *

by Stephan Schmitt

February 28, 2000

*
IO-automata and Ensemble *

by Mark Bickford

February 21, 2000

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

by Aleksey Nogin

February 14, 2000

*
Efficient Programming by Extract in Nuprl Type Theory *

by Aleksey Nogin

February 07, 2000

*
Automatic Complexity Analysis Revisited *

by Ralph Benzinger

January 31, 2000

*
Intersections, Unions and Games *

by Robert L. Constable, Alexei Kopylov, Aleksey Nogin

December 06, 1999

*
Principles of Stepwise Refinement *

by Heiko Mantel

November 22, 1999

*
Regions, part 2: The Capability Calculus *

by David Walker

November 15, 1999

*
An Introduction to Region Inference *

by David Walker

November 08, 1999

*
Decidability of Linear Affine Logic *

by Alexei Kopylov

November 01, 1999

*
Proof presentation in the Omega system *

by Erica Melis

October 25, 1999

*
Linear Logic *

by Alexei Kopylov

October 18, 1999

*
The Status of the Meta-Prl Project *

by Aleksey Nogin

October 04, 1999

*
Continuation of talk on Polymorphic References *

by Ozan Hafizogullari

September 24, 1999

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

by Robert L. Constable

September 13, 1999

1998-1999

*
A Methodology for Designing Asynchronous Circuits *

by Rajit Manohar

May 10, 1999

*
Some Uses of the Intersection Type *

by Stuart F. Allen, Robert L. Constable

May 03, 1999

*
The Current Projects of the MetaPRL Group *

by Aleksey Nogin, Jason Hickey

April 26, 1999

*
Knowledge-Based Proof Planning *

by Erica Melis

April 19, 1999

*
Practical Uses of Quotations, Macros and Reflection *

by Eli Barzilay

April 05, 1999

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

by Stuart F. Allen

March 29, 1999

*
Importing Isabelle Formal Mathematics into NuPRL *

by Pavel Naumov

March 08, 1999

*
Typed Assembly Language *

by Neal Glew

March 01, 1999

*
A Formal Framework for Modeling Memory *

by Victor Luchangco

February 22, 1999

*
A Programming Environment for Building Reliable High Performance Systems *

by Jason Hickey

February 15, 1999

*
Speeding Up the MetaPRL Refiner *

by Aleksey Nogin

February 08, 1999

*
Verbalization of High-Level Formal Proofs *

by Amanda Holland-Minkley

February 01, 1999

*
Semantics and Pragmatics of Reflected Proof *

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

December 01, 1998

*
On the Reflection Mechanism in Nuprl *

by Sergei Artemov

November 24, 1998

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

by Yves Bertot

November 17, 1998

*
Reflection Mechanisms in Nuprl *

by Stuart F. Allen, Robert L. Constable

November 10, 1998

*
Automatic Debugging Through Type Inference, Continued *

by Ozan Hafizogullari

November 03, 1998

*
On Modeling Ensemble *

by Robert L. Constable, Jason Hickey

October 27, 1998

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

by Robert L. Constable

October 20, 1998

*
Automatic Debugging Through Type Inference *

by Ozan Hafizogullari

October 06, 1998

*
On Howe's Importation of HOL into Nuprl *

by Evan Moran

September 29, 1998

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

by Uwe Egly

September 22, 1998

*
Automated Complexity Analysis *

by Ralph Benzinger

September 15, 1998

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

by Pavel Naumov

September 08, 1998

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

by Mark-Oliver Stehr

1998-1999

1998 Summ

*
Importing HOL Theorems into Nuprl *

by Douglas J. Howe

July 30, 1998

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

by Dirk van Dalen

June 26, 1998

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

by Jens Otten, Stephan Schmitt

June 23, 1998

1997-1998

*
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs *

by Brigitte Pientka

May 05, 1998

*
Intensional Polymorphism in Type-Erasure Semantics *

by Stephanie Weirich

April 28, 1998

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

by Dirk Schlimm

April 24, 1998

*
Simple, Efficient Object Encoding using Intersection Types *

by Karl Crary

April 14, 1998

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

by Evan Moran

April 07, 1998

*
Application of Notational Methods in dy/dx *

by Stuart F. Allen

March 31, 1998

*
Formal Models for Nuprl Evaluator *

by Aleksey Nogin

March 24, 1998

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

by Pavel Naumov

March 10, 1998

*
Logical Programming Environments *

by Jason Hickey

March 03, 1998

*
Type Methodology for Modern Languages and Compilers *

by Karl Crary

February 24, 1998

*
The Nuprl 5 Library *

by Richard Eaton

February 09, 1998

*
Dead Code Elimination *

by Ozan Hafizogullari, Christoph Kreitz

January 27, 1998

*
A Uniform Rippling Approach for Instantiating Free Variables *

by Brigitte Pientka

December 02, 1997

*
References in Type Theory *

by Pavel Naumov

November 25, 1997

*
Extracting Readable and Efficient Programs from Nuprl Proofs *

by James L. Caldwell

November 18, 1997

*
Abstract Identifiers in Nuprl 5 (continued) *

by Stuart F. Allen

October 28, 1997

*
Abstract Identifiers in Nuprl 5 *

by Stuart F. Allen

October 21, 1997

*
Proof Polynomials: Cut Elimination *

by Sergei Artemov

October 07, 1997

*
SupInf *

by Tobias Mayr

September 23, 1997

*
From System F to Typed Assembly Language *

by Karl Crary

September 16, 1997

*
Reasoning about Java Classes in Nuprl (continued) *

by Pavel Naumov

September 16, 1997

*
Reasoning about Java Classes in Nuprl *

by Pavel Naumov

September 09, 1997

1996-1997

*
Verifying Garbage Collection Algorithms using the PVS Theorem Prover *

by Paul B. Jackson

May 07, 1997

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

by Evan Moran

April 08, 1997

*
Computability is Ineffable in ZF Set Theory *

by Robert L. Constable

April 01, 1997

*
CZF, Type Theory, and Nuprl-Light *

by Evan Moran

April 01, 1997

*
Formal Continuations and Classical Logic *

by Karl Crary

March 10, 1997

*
Discussion of Issues in Logic Library Design *

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

March 03, 1997

*
Designing a Logical Library *

by Stuart F. Allen

February 24, 1997

*
Modules and Libraries *

by Jason Hickey

February 18, 1997

*
Nuprl Tutorial *

by Jason Hickey

February 02, 1997

*
Group Communication with Functional Languages *

by Mark Hayden

January 28, 1997

*
ML-like Type Reconstruction for Nuprl *

by Ozan Hafizogullari

November 26, 1996

*
DEC *

by Rustan Leino

November 19, 1996

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

by Karl Crary

November 12, 1996

*
Foundations for the Implementation of Higher-Order Subtyping *

by Karl Crary

November 05, 1996

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

by Karl Crary

1996-1997

*
Formal Methods & Distributed Systems *

by Mark Hayden

1996-1997

*
Formal Objects in Type Theory *

by Jason Hickey

1996-1997

*
Formal Reasoning about Communication Systems *

by Christoph Kreitz

1996-1997

*
Nuprl-Light *

by Jason Hickey, Jason Hickey

1996-1997

*
Nuprl-Light *

by Jason Hickey, Jason Hickey

1996-1997

*
Sharing Formal Mathematics and Programming *

by Jason Hickey

1996-1997

1996 Summ

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

by Todd Wilson

July 11, 1996

1995-1996

*
KML *

by Karl Crary

April 30, 1996

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

by Todd Wilson

March 26, 1996

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

by Jason Hickey

February 13, 1996

*
Project Direction and Research Problems *

by Robert L. Constable

February 06, 1996

*
Operational Modal Logic *

by Sergei Artemov

January 29, 1996

*
Formal Domain Theory *

by Neal Glew

December 05, 1995

*
Verifying HORUS in Nuprl *

by Jason Hickey

November 28, 1995

*
New Nuprl Editor *

by Stuart F. Allen

November 07, 1995

*
Formal Abstract Data Types and Inheritance *

by Jason Hickey

October 31, 1995

*
GOLEM *

by Ettore Remidde

October 24, 1995

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

by Richard Eaton

October 03, 1995

*
Design of the Nuprl Refiner *

by Roderick Moten

September 26, 1995

*
Overview of Nuprl 5 *

by Stuart F. Allen

September 19, 1995

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

by Jason Hickey

1995-1996

*
HORUS Verification Effort *

by Jason Hickey

1995-1996

*
The MathBus Term Structure *

by Richard Zippel

1995-1996

1994-1995

*
Square-Root Verification *

by Jason Hickey

May 10, 1995

*
Imperative Program Semantics *

by Stuart F. Allen

May 02, 1995

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

by Roderick Moten

April 04, 1995

*
Defining the Polynomial Time Functions over N in Nuprl *

by Robert L. Constable

March 28, 1995

*
An Open Architecture for Nuprl *

by Robert L. Constable

March 01, 1995

*
Developing Set Theory in HOL *

by Paul B. Jackson

February 28, 1995

*
Motivation: Basis of a Set Theory for Nuprl *

by Todd Wilson

February 21, 1995

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

by Chetan Murthy

February 14, 1995

*
Formal Methods Program at NASA Langley Research Center *

by James L. Caldwell

February 07, 1995

*
The Engineering Aspects of Proof-Environment Design *

by Chetan Murthy

January 24, 1995

*
Notation and Computer Aided Mathematics *

by Conal Mannion

December 06, 1994

*
Verifying an Implementation of a Polynomial Algebra ADT *

by Paul B. Jackson

November 29, 1994

*
Representing Computational Complexity in Nuprl *

by Robert L. Constable

November 22, 1994

*
The "Interface" Version of Nuprl *

by Stuart F. Allen, Richard Eaton

November 15, 1994

*
The Ultimate Programming Machine II: Very Dependent Types *

by Jason Hickey

November 08, 1994

*
TLA *

by Scott D. Stoller, Chetan Murthy

November 01, 1994

*
The Ultimate Programming Machine *

by Jason Hickey

October 25, 1994

*
Program Optimization in Type Theory *

by Brent Knight

October 18, 1994

*
Program Development for Proof Transformations *

by Helmut Schwichtenberg

October 12, 1994

*
Computer Algebra, Theorem Proving, and Types *

by Todd Wilson

October 04, 1994

*
GrÃ¶bner Basis *

by Thomas Yan

September 20, 1994

*
Recursive Types in Coq *

by Christine Paulin-Mohring

September 08, 1994

*
Very Dependent Function Space *

by Jason Hickey

1994-1995

1993-1994

*
Verifying a Pipelined Circuit *

by Mark Aagaard

April 05, 1994

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

by Scott D. Stoller

March 29, 1994

*
Formalizing the Theory Concept in Nuprl *

by Jason Hickey

March 15, 1994

*
Formalizing the Theory Mechanism in NuPRL *

by Jason Hickey

March 15, 1994

*
Hilbert Basis Function *

by Thomas Yan

March 01, 1994

*
The MIZAR Project *

by Paul B. Jackson

February 15, 1994

*
A Constructive Completeness Proof for Intuitionistic Predicate Calculus *

by Judith Underwood

February 01, 1994

*
Abstract Programming in Nuprl *

by Jason Hickey

November 23, 1993

*
Editing *

by Stuart F. Allen

November 16, 1993

*
Formalizing Hamiltonian Dynamics *

by Conal Mannion

November 09, 1993

*
Computational Content of Math *

by Douglas Bridges

October 19, 1993

*
How to Integrate Set Theory and Computation? *

by Scott D. Stoller

September 14, 1993

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

by Chetan Murthy

September 03, 1993

*
Semantics *

by Scott D. Stoller

March 30, 1993

*
A Program Transformation System *

by Annie Liu

1993-1994

*
Extraction of Programs *

by Benjamin Werner

1993-1994

*
Polya/Nuprl *

by Stuart F. Allen

1993-1994

*
Reasoning about Scientific Programs *

by Conal Mannion, Stuart F. Allen

1993-1994

1993 Summ

*
Theorem Proving with Real Numbers *

by Robert L. Constable

August 31, 1993

*
Connecting Formal Semantics to Constructive Intuitions *

by Michael J. O'Donnell

July 06, 1993

*
Project Overview *

by Robert L. Constable

July 01, 1993

1992-1993

*
TBA *

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

May 04, 1993

*
Formalizing Program Synthesis *

by Arnd Poetzsch

April 27, 1993

*
Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus *

by Robert L. Constable, Robert L. Constable

April 19, 1993

*
Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus *

by Robert L. Constable, Robert L. Constable

April 19, 1993

*
Proofs by Structural Induction using Partial Evaluation *

by Julia Lawall

April 13, 1993

*
Reflection *

by William Aitken

April 06, 1993

*
Using Reflection to External Automated Theorem Provers *

by Mark Aagaard

March 30, 1993

*
Extraction *

by Judith Underwood

March 16, 1993

*
Semantics of the Nuprl Type Theory *

by Scott D. Stoller

March 16, 1993

*
Editor Demonstration *

by Paul B. Jackson

March 09, 1993

*
Constructive Algorithms in Nuprl *

by Douglas J. Howe

December 01, 1992

*
The Enigma of Sat Hill Climbing Procedures *

by Ian Gent

November 10, 1992

*
Set Models *

by Douglas J. Howe

November 03, 1992

*
Structuring Proofs *

by Douglas J. Howe, Paul B. Jackson

October 27, 1992

*
Fefprl *

by Douglas J. Howe, Douglas J. Howe

October 20, 1992

*
Fefprl *

by Douglas J. Howe, Douglas J. Howe

October 05, 1992

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

by Helmut Schwichtenberg

September 29, 1992

*
Tactic Trees in eXene *

by Roderick Moten

September 22, 1992

*
HOL Workshop *

by Mark Aagaard

September 15, 1992

*
Defining Polynomials in Constructive Type Theory *

by Paul B. Jackson

1992-1993

1991-1992

*
CADE Practice Talk *

by Wilfred Z. Chen

May 12, 1992

*
PVS *

by N Shankar

March 24, 1992

*
Reflection 2 *

by William Aitken, William Aitken

March 05, 1992

*
Reflection 2 *

by William Aitken, William Aitken

February 18, 1992

*
Attaching Context to Objects in the Library *

by Stuart F. Allen

February 04, 1992

*
PRL Library Day *

by Stuart F. Allen

November 19, 1991

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

by Jim Lipton

November 12, 1991

*
Nuprl 3 vs. Nuprl 4 *

by Paul B. Jackson

November 05, 1991

*
How to Strengthen the Notion of Obvious Step *

by Wilfred Z. Chen

October 22, 1991

1990-1991

*
A Basis for Constructive, Reflexive Type Theory *

by William Aitken

October 01, 1990

*
Lambda Calculus as Basis for Programming Language Design *

by Robert W. Harper

1990-1991

1990 Summ

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

by Nax P. Mendler

1990 Summ

1989-1990

*
20BJ as a Meta-logical Framework *

by Andrew Stevens

April 21, 1990

*
Using Nuprl to Verify Floating Point Hardware *

by Paul B. Jackson

April 17, 1990

*
Plotkin *

by Jim Lipton

March 13, 1990

*
Logical Relations *

by Jim Lipton

March 06, 1990

*
Polymorphism Is Not Set Theoretic *

by Nax P. Mendler

February 14, 1990

*
Intuitionistic ZF *

by Jim Lipton

January 30, 1990

*
The Lambda Calculus as a Basis for Language Design *

by Robert W. Harper

1989-1990

1988

*
Collaborative Problem Solving Environment *

by Robert L. Constable

1988

1987-1988

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

by Stuart F. Allen

April 26, 1988

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

by Stuart F. Allen

April 19, 1988

*
TBA *

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

April 08, 1988

*
Rational Reconstruction of Boyer and Moore Prover *

by Andrew Stevens

December 01, 1987

*
Partial Objects *

by Scott F. Smith

November 24, 1987

*
Math Vernacular *

by N. G. deBruijn

November 17, 1987

*
Domains in Type Theory *

by Scott F. Smith

November 10, 1987

*
Typed Enumeration-Free External Setting for Computing Theory *

by Robert L. Constable

November 03, 1987

*
TBA *

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

October 13, 1987

*
The ONTIC System *

by David McAllister

October 06, 1987

*
Syntactic Abstraction *

by Timothy G. Griffin

September 22, 1987

1986-1987

*
Metamathematics of Reflection *

by Todd B. Knoblock

April 22, 1987

*
The Expressiveness of lambda Y *

by David A. Basin

April 09, 1987

*
Bar Types *

by Scott F. Smith

March 18, 1987

*
Realizabiity for IZF *

by Jim Lipton

March 12, 1987

*
Term Model Semantics and Tait Computability Method *

by Scott F. Smith

March 11, 1987

*
IZF and Recursive Realizability *

by Jim Lipton

March 05, 1987

*
Category Theory as Basis for Mathematics *

by John Beck

December 02, 1986

*
Continuation of Categorial Models of Nuprl *

by Michael Schwartzbach

October 28, 1986

*
Categorical Models of Nuprl *

by Michael Schwartzbach

October 21, 1986

*
Strong Normalization in Lambda ^{2} *

by Nax P. Mendler

October 02, 1986

*
Empty Types *

by John Mitchell

September 25, 1986

*
Implementing Finite Sets *

by Walter Rance Cleaveland

September 09, 1986

1985-1986

*
Programs as Specification *

by Rick Hehner

May 06, 1986

1984-1985

*
Arithpac *

by Timothy G. Griffin

1984-1985

*
Defining Lambda-prl and Its Extensions *

by Scott F. Smith

1984-1985

*
Denotational Semantics *

by Nax P. Mendler

1984-1985

*
Equality *

by Robert W. Harper

1984-1985

*
Marhew's Principle *

by Ryan Stansifer

1984-1985

*
ML Execution *

by H. M. Bromley

1984-1985

*
Nuprl Execution *

by H. M. Bromley

1984-1985

*
Optimizing Ext *

by James T. Sasaki

1984-1985

*
Partial Recursive Functions *

by Nax P. Mendler

1984-1985

*
PP-lambda in Nuprl *

by Nax P. Mendler

1984-1985

*
Predicate Calculus Model *

by Stuart F. Allen

1984-1985

*
Prolog *

by Ryan Stansifer, Stuart F. Allen

1984-1985

*
Reflective PRL *

by Todd B. Knoblock

1984-1985

*
Theory of Reals *

by Douglas J. Howe

1984-1985

*
Thesis *

by Douglas J. Howe

1984-1985

*
Type Inference *

by Robert W. Harper

1984-1985

*
Universally Closed Classes *

by Robert L. Constable

1984-1985

*
Using Lemmas *

by Timothy G. Griffin

1984-1985