Knowledge Base list of
Seminars
PhD theses from the project are accessible at the NCSTRL web site.
List by Year
380 results
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 Lambda2
by Nax P. Mendler
October 02, 1986
Empty Types
by John Mitchell
September 25, 1986
Implementing Finite Sets
by Walter Rance Cleaveland
September 09, 1986
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