Skip to main content
PRL Project

Knowledge Base list of Seminar Seminars

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

Browse by author | title | year | subject

List by Author

495 results


Aagaard, Mark

Seminar Verifying a Pipelined Circuit
by Mark Aagaard
April 05, 1994

Seminar Using Reflection to External Automated Theorem Provers
by Mark Aagaard
March 30, 1993

Seminar HOL Workshop
by Mark Aagaard
September 15, 1992

Aitken, William

Seminar Reflection
by William Aitken
April 06, 1993

Seminar Reflection 2
by William Aitken, William Aitken
March 05, 1992

Seminar Reflection 2
by William Aitken, William Aitken
March 05, 1992

Seminar Reflection 2
by William Aitken, William Aitken
February 18, 1992

Seminar Reflection 2
by William Aitken, William Aitken
February 18, 1992

Seminar A Basis for Constructive, Reflexive Type Theory
by William Aitken
October 01, 1990

Allen, Stuart F.

Seminar A Semantics for Abstract Atoms in Nuprl
by Stuart F. Allen
March 31, 2006

Seminar Anchoring Expository Text in Formal Mathematics -- Part II
by Stuart F. Allen
April 15, 2005

Seminar Anchoring Expository Text in Formal Mathematics
by Stuart F. Allen
December 06, 2004

Seminar Type Theory as a Legacy from Logicism
by Stuart F. Allen
March 08, 2004

Seminar Applied Logic as Part of an Effort to Accumulate Precise Knowledge
by Stuart F. Allen
February 09, 2004

Seminar Remarks on the FDL (Formal Digital Library) Project -- Continuation of talk begun November 17
by Stuart F. Allen
December 01, 2003

Seminar Remarks on the FDL (Formal Digital Library) Project
by Stuart F. Allen
November 17, 2003

Seminar Report on the Design of the Formal Digital Library
by Richard Eaton, Robert L. Constable, Stuart F. Allen
April 08, 2002

Seminar Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002

Seminar Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics
by Stuart F. Allen, Robert L. Constable
December 03, 2001

Seminar 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

Seminar 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

Seminar 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

Seminar Semantics and Pragmatics of Reflected Proof
by Stuart F. Allen, Sergei Artemov, Robert L. Constable
December 01, 1998

Seminar Some Uses of the Intersection Type
by Stuart F. Allen, Robert L. Constable
May 03, 1999

Seminar Using Nuprl as a Formal Assistant for Preparing Largely Informal Material
by Stuart F. Allen
March 29, 1999

Seminar Reflection Mechanisms in Nuprl
by Stuart F. Allen, Robert L. Constable
November 10, 1998

Seminar Application of Notational Methods in dy/dx
by Stuart F. Allen
March 31, 1998

Seminar Abstract Identifiers in Nuprl 5 (continued)
by Stuart F. Allen
October 28, 1997

Seminar Abstract Identifiers in Nuprl 5
by Stuart F. Allen
October 21, 1997

Seminar Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997

Seminar Designing a Logical Library
by Stuart F. Allen
February 24, 1997

Seminar New Nuprl Editor
by Stuart F. Allen
November 07, 1995

Seminar Overview of Nuprl 5
by Stuart F. Allen
September 19, 1995

Seminar Imperative Program Semantics
by Stuart F. Allen
May 02, 1995

Seminar The "Interface" Version of Nuprl
by Stuart F. Allen, Richard Eaton
November 15, 1994

Seminar Reasoning about Scientific Programs
by Conal Mannion, Stuart F. Allen
1993-1994

Seminar Polya/Nuprl
by Stuart F. Allen
1993-1994

Seminar Editing
by Stuart F. Allen
November 16, 1993

Seminar Attaching Context to Objects in the Library
by Stuart F. Allen
February 04, 1992

Seminar PRL Library Day
by Stuart F. Allen
November 19, 1991

Seminar Continuation of A Type Theoretic Interpretation of DougHowe's Squiggle Relation
by Stuart F. Allen
April 26, 1988

Seminar A Type Theoretic Interpretation of Doug Howe's Squiggle Relation
by Stuart F. Allen
April 19, 1988

Seminar Prolog
by Ryan Stansifer, Stuart F. Allen
1984-1985

Seminar Predicate Calculus Model
by Stuart F. Allen
1984-1985

Anand, Abhishek

Seminar Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014

Seminar Coinduction in Coq
by Abhishek Anand
November 12, 2014

Seminar From Replicated Databases to Ensembles of Collaborating Robots
by Abhishek Anand, Mark Bickford
November 19, 2014

Seminar The Beauty of Nuprl's Uniform Term Representation and How to Reason about those Terms in Coq
by Abhishek Anand
October 09, 2013

Seminar A verified proof assistant
by Vincent Rahli, Abhishek Anand
October 30, 2013

Seminar How far can we go with Induction-Recursion?
by Abhishek Anand, Vincent Rahli
November 20, 2013

Seminar The Type Base and Undecidability in Type Theory
by Abhishek Anand
September 21, 2012

Seminar Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012

Artemov, Sergei

Seminar Reflected Lambda Calculus
by Sergei Artemov
October 02, 2000

Seminar Stability of intuitionistic systems
by Sergei Artemov
April 24, 2000

Seminar Semantics and Pragmatics of Reflected Proof
by Stuart F. Allen, Sergei Artemov, Robert L. Constable
December 01, 1998

Seminar On the Reflection Mechanism in Nuprl
by Sergei Artemov
November 24, 1998

Seminar Proof Polynomials: Cut Elimination
by Sergei Artemov
October 07, 1997

Seminar Operational Modal Logic
by Sergei Artemov
January 29, 1996

Barzilay, Eli

Seminar Reflection in First-Order Logic
by Eli Barzilay
February 12, 2001

Seminar Latest results about reflection (TENTATIVE)
by Eli Barzilay
November 20, 2000

Seminar Reflection Part II
by Eli Barzilay
April 03, 2000

Seminar Analysis of reflection in programming languages using Scheme as the main example
by Eli Barzilay
March 06, 2000

Seminar Practical Uses of Quotations, Macros and Reflection
by Eli Barzilay
April 05, 1999

Barzilay, Regina

Seminar Online Demonstration of Syntactic Reflection. Realizing an Argument about Syntax (Tarski).
by Regina Barzilay
March 03, 2003

Seminar HOAS -- Higher Order Abstract Syntax: a Survey
by Regina Barzilay
October 21, 2002

Seminar The Abstract Term Type
by Regina Barzilay
March 04, 2002

Seminar 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

Seminar 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

Seminar 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

Basin, David A.

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
May 04, 1993

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
April 08, 1988

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
October 13, 1987

Seminar The Expressiveness of lambda Y
by David A. Basin
April 09, 1987

Beck, John

Seminar Category Theory as Basis for Mathematics
by John Beck
December 02, 1986

Benzinger, Ralph

Seminar Automated Higher-Order Complexity Analysis
by Ralph Benzinger
February 05, 2001

Seminar 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

Seminar 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

Seminar 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

Seminar Automatic Complexity Analysis Revisited
by Ralph Benzinger
January 31, 2000

Seminar Automated Complexity Analysis
by Ralph Benzinger
September 15, 1998

Bertot, Yves

Seminar Mechanizing the Proof of Correction of a Compiler Using Type Theory
by Yves Bertot
November 17, 1998

Bickford, Mark

Seminar Formalizing Bishop's Constructive Analysis in Constructive Type Theory
by Mark Bickford, Robert L. Constable
April 10, 2014

Seminar Synthesizing Protocols using the Logic of Events and EventML
by Robert L. Constable, Mark Bickford
September 17, 2014

Seminar There Are No Discontinuous Real Functions
by Mark Bickford, Vincent Rahli
October 08, 2014

Seminar Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014

Seminar Nominal Type Theory
by Mark Bickford, Vincent Rahli
October 29, 2014

Seminar From Replicated Databases to Ensembles of Collaborating Robots
by Abhishek Anand, Mark Bickford
November 19, 2014

Seminar Synthetic Topology in NuPRL
by Francisco Mota, Mark Bickford
December 03, 2014

Seminar The power of bar induction in constructive type theory
by Mark Bickford
September 25, 2013

Seminar Quotient Types in Nuprl
by Mark Bickford
November 13, 2013

Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Seminar Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012

Seminar Realizing Bar Induction in Nuprl
by Mark Bickford
October 26, 2012

Seminar NuPRL Demo
by Mark Bickford
September 16, 2011

Seminar Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011

Seminar Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012

Seminar Adding Communication Primitives to the Nuprl Evaluator
by Mark Bickford
May 04, 2012

Seminar Urelements in Type Theory: New Definition of "Inherence"
by Mark Bickford
November 18, 2005

Seminar Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
August 26, 2005

Seminar Automated Proofs in Event Logic
by Mark Bickford
September 16, 2005

Seminar Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
March 23, 2006

Seminar Event Systems: Introduction to the Logic of Events
by Mark Bickford
February 17, 2006

Seminar Real-time Message Automata
by Mark Bickford
February 11, 2005

Seminar Mark Presentation
by Mark Bickford
November 29, 2004

Seminar Urelements in Computational Type Theory
by Mark Bickford
November 11, 2005

Seminar The Logic of Events and Event Structure Patterns
by Mark Bickford
April 26, 2004

Seminar Leader Election Protocols
by Mark Bickford
October 06, 2003

Seminar Implementing the Logic of Events
by Mark Bickford
February 24, 2003

Seminar Application of Event Systems and the Logic of Distributed Systems to Leader Election
by Mark Bickford
September 30, 2002

Seminar Introduction to Event Systems and the Logic of Distributed Systems
by Mark Bickford, Robert L. Constable
September 16, 2002

Seminar Recent Results on the PCES Project
by Mark Bickford
April 01, 2002

Seminar Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001

Seminar Processing video streams using event notification systems
by Robert L. Constable, Mark Bickford
October 15, 2001

Seminar More on proof automation: Shostak's decision procedure and Nuprl
by Mark Bickford
September 24, 2001

Seminar 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

Seminar 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

Seminar 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

Seminar Continuation on reflection
by Mark Bickford
March 13, 2000

Seminar IO-automata and Ensemble
by Mark Bickford
February 21, 2000

Bridges, Douglas

Seminar Computational Content of Math
by Douglas Bridges
October 19, 1993

Bromley, H. M.

Seminar ML Execution
by H. M. Bromley
1984-1985

Seminar Nuprl Execution
by H. M. Bromley
1984-1985

Bryukhov, Yegor

Seminar Arithmetic module for MetaPRL: rules and Arith tactic
by Yegor Bryukhov
March 25, 2002

Caldwell, James L.

Seminar Extracting Readable and Efficient Programs from Nuprl Proofs
by James L. Caldwell
November 18, 1997

Seminar Formal Methods Program at NASA Langley Research Center
by James L. Caldwell
February 07, 1995

Chen, Wilfred Z.

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
May 04, 1993

Seminar CADE Practice Talk
by Wilfred Z. Chen
May 12, 1992

Seminar How to Strengthen the Notion of Obvious Step
by Wilfred Z. Chen
October 22, 1991

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
April 08, 1988

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
October 13, 1987

Cheney, James

Seminar Randomized Programming and Probabilistic Reasoning in Type Theory
by James Cheney
April 17, 2000

Cleaveland, Walter Rance

Seminar Implementing Finite Sets
by Walter Rance Cleaveland
September 09, 1986

Cohen, Liron

Seminar Intuitionistic Ancestral Logic
by Liron Cohen
July 12, 2012

Constable, Robert L.

Seminar Formalizing Bishop's Constructive Analysis in Constructive Type Theory
by Mark Bickford, Robert L. Constable
April 10, 2014

Seminar Synthesizing Protocols using the Logic of Events and EventML
by Robert L. Constable, Mark Bickford
September 17, 2014

Seminar Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014

Seminar An Extension of OCaml's Type Theory
by Robert L. Constable
October 23, 2013

Seminar Nuprl as a Programming Assistant
by Robert L. Constable
November 06, 2013

Seminar Introduction to the Fall Seminar Series
by Robert L. Constable
September 07, 2012

Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Seminar Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012

Seminar Seminar History and Initial Planning Meeting
by Robert L. Constable
September 09, 2011

Seminar Seminar History and Initial Planning Meeting
by Robert L. Constable, Robert L. Constable
September 09, 2011

Seminar Seminar History and Initial Planning Meeting
by Robert L. Constable, Robert L. Constable
September 09, 2011

Seminar Analyzing Access Control Logics Using Evidence Semantics
by Robert L. Constable
September 23, 2011

Seminar Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011

Seminar Stronger Role for Recursive Types Needed for Logic of Events
by Robert L. Constable
February 24, 2012

Seminar Reviewing Nuprl
by Robert L. Constable
March 09, 2012

Seminar Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012

Seminar Randomness and Free Choice Sequences
by Robert L. Constable
February 04, 2005

Seminar Remarks on Nijmegen trip
by Robert L. Constable
November 08, 2004

Seminar Foundations for the Management of Formal Mathematical Knowledge
by Robert L. Constable
October 25, 2004

Seminar Automated Reasoning in Category Theory
by Robert L. Constable
October 04, 2004

Seminar Important Episodes in the History of Constructive Mathematics--including the frog and mouse wars
by Robert L. Constable
March 01, 2004

Seminar Comparing Aspects of Set Theory and Type Theory
by Robert L. Constable
February 16, 2004

Seminar Planning Session for Spring Seminar Series
by Robert L. Constable
January 26, 2004

Seminar Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge
by Robert L. Constable
October 27, 2003

Seminar An Introduction to Event Systems
by Robert L. Constable
September 29, 2003

Seminar Introduction to the Fall Seminar Series
by Robert L. Constable
September 08, 2003

Seminar Continuing Discussion of the NSDL
by Robert L. Constable
April 14, 2003

Seminar Enabling Active Mathematical Documents in the National Science Digital Library
by Robert L. Constable
March 31, 2003

Seminar Uri Abraham's Models for Concurrency
by Robert L. Constable, Sabina Petride
January 27, 2003

Seminar Continuing Discussion of Objects
by Alexei Kopylov, Robert L. Constable
December 02, 2002

Seminar Classes and Objects
by Robert L. Constable
November 25, 2002

Seminar Introduction to Event Systems and the Logic of Distributed Systems
by Mark Bickford, Robert L. Constable
September 16, 2002

Seminar Properties of the Formal Digital Library
by Robert L. Constable
May 06, 2002

Seminar Report on the Edinburgh Conference: 35 Years of Automath
by Robert L. Constable
2001-2002

Seminar Report on the Design of the Formal Digital Library
by Richard Eaton, Robert L. Constable, Stuart F. Allen
April 08, 2002

Seminar Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002

Seminar Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics
by Stuart F. Allen, Robert L. Constable
December 03, 2001

Seminar Embedded Ststems
by Christoph Kreitz, Robert L. Constable
November 05, 2001

Seminar Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001

Seminar Processing video streams using event notification systems
by Robert L. Constable, Mark Bickford
October 15, 2001

Seminar NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 26, 2001

Seminar NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 26, 2001

Seminar NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 12, 2001

Seminar NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 12, 2001

Seminar How Nuprl Reasons
by Robert L. Constable
January 29, 2001

Seminar Research Directions
by Robert L. Constable
September 25, 2000

Seminar Reading BAAs and RFPs
by Robert L. Constable
October 16, 2000

Seminar Reading BAAs and RFPs (cont.)
by Robert L. Constable
October 23, 2000

Seminar Discussing the issues surrounding our library of formal algorithmic mathematics
by Robert L. Constable
November 13, 2000

Seminar Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999

Seminar Points of Contact with Girard (Nuprl ∩ Ludics)
by Robert L. Constable
September 13, 1999

Seminar Semantics and Pragmatics of Reflected Proof
by Stuart F. Allen, Sergei Artemov, Robert L. Constable
December 01, 1998

Seminar Listening to Theorem Provers who Talk to Each Other about Computer Systems
by Robert L. Constable
October 20, 1998

Seminar Some Uses of the Intersection Type
by Stuart F. Allen, Robert L. Constable
May 03, 1999

Seminar Reflection Mechanisms in Nuprl
by Stuart F. Allen, Robert L. Constable
November 10, 1998

Seminar On Modeling Ensemble
by Robert L. Constable, Jason Hickey
October 27, 1998

Seminar Computability is Ineffable in ZF Set Theory
by Robert L. Constable
April 01, 1997

Seminar Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997

Seminar Project Direction and Research Problems
by Robert L. Constable
February 06, 1996

Seminar Defining the Polynomial Time Functions over N in Nuprl
by Robert L. Constable
March 28, 1995

Seminar An Open Architecture for Nuprl
by Robert L. Constable
March 01, 1995

Seminar Representing Computational Complexity in Nuprl
by Robert L. Constable
November 22, 1994

Seminar Theorem Proving with Real Numbers
by Robert L. Constable
August 31, 1993

Seminar Project Overview
by Robert L. Constable
July 01, 1993

Seminar Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993

Seminar Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993

Seminar Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993

Seminar Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993

Seminar Collaborative Problem Solving Environment
by Robert L. Constable
1988

Seminar Typed Enumeration-Free External Setting for Computing Theory
by Robert L. Constable
November 03, 1987

Seminar Universally Closed Classes
by Robert L. Constable
1984-1985

Crary, Karl

Seminar Simple, Efficient Object Encoding using Intersection Types
by Karl Crary
April 14, 1998

Seminar Type Methodology for Modern Languages and Compilers
by Karl Crary
February 24, 1998

Seminar From System F to Typed Assembly Language
by Karl Crary
September 16, 1997

Seminar Formal Continuations and Classical Logic
by Karl Crary
March 10, 1997

Seminar Advancing the Type-Theoretic Underpinnings of Practical Programming Languages
by Karl Crary
1996-1997

Seminar Foundations for the Implementation of Higher-Order Subtyping: Part II
by Karl Crary
November 12, 1996

Seminar Foundations for the Implementation of Higher-Order Subtyping
by Karl Crary
November 05, 1996

Seminar KML
by Karl Crary
April 30, 1996

deBruijn, N. G.

Seminar Math Vernacular
by N. G. deBruijn
November 17, 1987

Eaton, Richard

Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Seminar Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012

Seminar Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
August 26, 2005

Seminar Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
March 23, 2006

Seminar Report on the Design of the Formal Digital Library
by Richard Eaton, Robert L. Constable, Stuart F. Allen
April 08, 2002

Seminar Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002

Seminar The Nuprl 5 Library
by Richard Eaton
February 09, 1998

Seminar Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997

Seminar Design and Implemention of the Library Component of Nuprl 5
by Richard Eaton
October 03, 1995

Seminar The "Interface" Version of Nuprl
by Stuart F. Allen, Richard Eaton
November 15, 1994

Egly, Uwe

Seminar On Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis
by Uwe Egly
September 22, 1998

Evfimievski, Sasha

Seminar 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

Seminar 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

Seminar 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

Seminar Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations
by Matthew Fluet
November 24, 2003

Seminar Variations on a Proof by Smullyan
by Matthew Fluet
May 05, 2003

Seminar The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002

Gent, Ian

Seminar The Enigma of Sat Hill Climbing Procedures
by Ian Gent
November 10, 1992

Glew, Neal

Seminar Typed Assembly Language
by Neal Glew
March 01, 1999

Seminar Formal Domain Theory
by Neal Glew
December 05, 1995

Gonthier, Georges

Seminar Verifying the Four Colour Theorem
by Georges Gonthier
May 20, 2005

Griffin, Timothy G.

Seminar Syntactic Abstraction
by Timothy G. Griffin
September 22, 1987

Seminar Using Lemmas
by Timothy G. Griffin
1984-1985

Seminar Arithpac
by Timothy G. Griffin
1984-1985

Hafizogullari, Ozan

Seminar 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

Seminar 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

Seminar 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

Seminar Continuation of talk on Polymorphic References
by Ozan Hafizogullari
September 24, 1999

Seminar Automatic Debugging Through Type Inference, Continued
by Ozan Hafizogullari
November 03, 1998

Seminar Automatic Debugging Through Type Inference
by Ozan Hafizogullari
October 06, 1998

Seminar Dead Code Elimination
by Ozan Hafizogullari, Christoph Kreitz
January 27, 1998

Seminar ML-like Type Reconstruction for Nuprl
by Ozan Hafizogullari
November 26, 1996

Harper, Robert W.

Seminar Lambda Calculus as Basis for Programming Language Design
by Robert W. Harper
1990-1991

Seminar The Lambda Calculus as a Basis for Language Design
by Robert W. Harper
1989-1990

Seminar Equality
by Robert W. Harper
1984-1985

Seminar Type Inference
by Robert W. Harper
1984-1985

Hayden, Mark

Seminar Formal Methods & Distributed Systems
by Mark Hayden
1996-1997

Seminar Group Communication with Functional Languages
by Mark Hayden
January 28, 1997

Hehner, Rick

Seminar Programs as Specification
by Rick Hehner
May 06, 1986

Hickey, Jason

Seminar Caltech Computer Science
by Jason Hickey
November 06, 2000

Seminar The Current Projects of the MetaPRL Group
by Aleksey Nogin, Jason Hickey
April 26, 1999

Seminar A Programming Environment for Building Reliable High Performance Systems
by Jason Hickey
February 15, 1999

Seminar On Modeling Ensemble
by Robert L. Constable, Jason Hickey
October 27, 1998

Seminar Logical Programming Environments
by Jason Hickey
March 03, 1998

Seminar Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997

Seminar Modules and Libraries
by Jason Hickey
February 18, 1997

Seminar Sharing Formal Mathematics and Programming
by Jason Hickey
1996-1997

Seminar Nuprl Tutorial
by Jason Hickey
February 02, 1997

Seminar Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997

Seminar Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997

Seminar Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997

Seminar Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997

Seminar Formal Objects in Type Theory
by Jason Hickey
1996-1997

Seminar Formal Module Systems and Nuprl-Light: A Programmer's Perspective
by Jason Hickey
February 13, 1996

Seminar Verifying HORUS in Nuprl
by Jason Hickey
November 28, 1995

Seminar Formal Abstract Data Types and Inheritance
by Jason Hickey
October 31, 1995

Seminar Formal Modules (Abstract Data Types) and Object Oriented Programming
by Jason Hickey
1995-1996

Seminar HORUS Verification Effort
by Jason Hickey
1995-1996

Seminar Square-Root Verification
by Jason Hickey
May 10, 1995

Seminar Very Dependent Function Space
by Jason Hickey
1994-1995

Seminar The Ultimate Programming Machine II: Very Dependent Types
by Jason Hickey
November 08, 1994

Seminar The Ultimate Programming Machine
by Jason Hickey
October 25, 1994

Seminar Formalizing the Theory Concept in Nuprl
by Jason Hickey
March 15, 1994

Seminar Formalizing the Theory Mechanism in NuPRL
by Jason Hickey
March 15, 1994

Seminar Abstract Programming in Nuprl
by Jason Hickey
November 23, 1993

Holland-Minkley, Amanda

Seminar Nuprl Library Annotation
by Amanda Holland-Minkley
April 05, 2004

Seminar A Linguistic View of Constuctive Type Theory
by Amanda Holland-Minkley
February 02, 2004

Seminar Automatic generation of texts from Nuprl proofs
by Amanda Holland-Minkley
February 04, 2002

Seminar Validating a methodology for natural language generation
by Amanda Holland-Minkley
March 05, 2001

Seminar 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

Seminar 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

Seminar 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

Seminar Verbalization of High-Level Formal Proofs
by Amanda Holland-Minkley
February 01, 1999

Howe, Douglas J.

Seminar Importing HOL Theorems into Nuprl
by Douglas J. Howe
July 30, 1998

Seminar Constructive Algorithms in Nuprl
by Douglas J. Howe
December 01, 1992

Seminar Set Models
by Douglas J. Howe
November 03, 1992

Seminar Structuring Proofs
by Douglas J. Howe, Paul B. Jackson
October 27, 1992

Seminar Fefprl
by Douglas J. Howe, Douglas J. Howe
October 20, 1992

Seminar Fefprl
by Douglas J. Howe, Douglas J. Howe
October 20, 1992

Seminar Fefprl
by Douglas J. Howe, Douglas J. Howe
October 05, 1992

Seminar Fefprl
by Douglas J. Howe, Douglas J. Howe
October 05, 1992

Seminar Thesis
by Douglas J. Howe
1984-1985

Seminar Theory of Reals
by Douglas J. Howe
1984-1985

Jackson, Paul B.

Seminar Verifying Garbage Collection Algorithms using the PVS Theorem Prover
by Paul B. Jackson
May 07, 1997

Seminar Developing Set Theory in HOL
by Paul B. Jackson
February 28, 1995

Seminar Verifying an Implementation of a Polynomial Algebra ADT
by Paul B. Jackson
November 29, 1994

Seminar The MIZAR Project
by Paul B. Jackson
February 15, 1994

Seminar Defining Polynomials in Constructive Type Theory
by Paul B. Jackson
1992-1993

Seminar Editor Demonstration
by Paul B. Jackson
March 09, 1993

Seminar Structuring Proofs
by Douglas J. Howe, Paul B. Jackson
October 27, 1992

Seminar Nuprl 3 vs. Nuprl 4
by Paul B. Jackson
November 05, 1991

Seminar Using Nuprl to Verify Floating Point Hardware
by Paul B. Jackson
April 17, 1990

Klavins, Eric

Seminar Some Recent Results in MetaPRL
by Eric Klavins
April 22, 2002

Knight, Brent

Seminar Program Optimization in Type Theory
by Brent Knight
October 18, 1994

Knoblock, Todd B.

Seminar Metamathematics of Reflection
by Todd B. Knoblock
April 22, 1987

Seminar Reflective PRL
by Todd B. Knoblock
1984-1985

Kopylov, Alexei

Seminar Verified Implementation of Red-Black Trees
by Alexei Kopylov
November 10, 2003

Seminar Representing Red-Black Trees in MetaPRL
by Alexei Kopylov
March 10, 2003

Seminar Continuing Discussion of Objects
by Alexei Kopylov, Robert L. Constable
December 02, 2002

Seminar Continuing on Objects and Classes
by Alexei Kopylov
November 18, 2002

Seminar Abstact Data Structures, Objects and Classes in the Nuprl Type Theory
by Alexei Kopylov
November 11, 2002

Seminar Representing Objects in Nuplr Type Theory
by Alexei Kopylov
April 29, 2002

Seminar Objects
by Alexei Kopylov
November 19, 2001

Seminar Record calculus
by Alexei Kopylov
November 12, 2001

Seminar Kopylov and Nogin CSL Submission
by Alexei Kopylov
April 02, 2001

Seminar A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory
by Alexei Kopylov, Aleksey Nogin
November 27, 2000

Seminar A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory (cont)
by Aleksey Nogin, Alexei Kopylov
December 04, 2000

Seminar Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999

Seminar Decidability of Linear Affine Logic
by Alexei Kopylov
November 01, 1999

Seminar Linear Logic
by Alexei Kopylov
October 18, 1999

Kozen, Dexter

Seminar A Proof-Theoretic Approach to Knowledge Acquisition"
by Dexter Kozen
January 28, 2002

Kreitz, Christoph

Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Seminar Microsoft's Spec#
by Christoph Kreitz
April 17, 2006

Seminar Constructive Proofs and Program Extraction
by Christoph Kreitz
February 23, 2004

Seminar The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002

Seminar Enhancing Proof Assistant Systems
by Christoph Kreitz
February 25, 2002

Seminar Embedded Ststems
by Christoph Kreitz, Robert L. Constable
November 05, 2001

Seminar Proof Automation in Constructive Type Theory
by Christoph Kreitz
September 17, 2001

Seminar Dead Code Elimination
by Ozan Hafizogullari, Christoph Kreitz
January 27, 1998

Seminar Formal Reasoning about Communication Systems
by Christoph Kreitz
1996-1997

Lawall, Julia

Seminar Proofs by Structural Induction using Partial Evaluation
by Julia Lawall
April 13, 1993

Leino, Rustan

Seminar DEC
by Rustan Leino
November 19, 1996

Lipton, Jim

Seminar Can we Compile the Prolog Program to a Type?
by Jim Lipton
November 12, 1991

Seminar Plotkin
by Jim Lipton
March 13, 1990

Seminar Logical Relations
by Jim Lipton
March 06, 1990

Seminar Intuitionistic ZF
by Jim Lipton
January 30, 1990

Seminar Realizabiity for IZF
by Jim Lipton
March 12, 1987

Seminar IZF and Recursive Realizability
by Jim Lipton
March 05, 1987

Liu, Annie

Seminar A Program Transformation System
by Annie Liu
1993-1994

Lorigo, Lori

Seminar Enhancing the search of mathematics & Hot topics in mathematical search
by Lori Lorigo
May 03, 2004

Seminar Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001

Seminar 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

Seminar 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

Seminar 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

Luchangco, Victor

Seminar A Formal Framework for Modeling Memory
by Victor Luchangco
February 22, 1999

Mannion, Conal

Seminar Notation and Computer Aided Mathematics
by Conal Mannion
December 06, 1994

Seminar Reasoning about Scientific Programs
by Conal Mannion, Stuart F. Allen
1993-1994

Seminar Formalizing Hamiltonian Dynamics
by Conal Mannion
November 09, 1993

Manohar, Rajit

Seminar A Methodology for Designing Asynchronous Circuits
by Rajit Manohar
May 10, 1999

Mantel, Heiko

Seminar Principles of Stepwise Refinement
by Heiko Mantel
November 22, 1999

Mayr, Tobias

Seminar SupInf
by Tobias Mayr
September 23, 1997

McAllister, David

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
May 04, 1993

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
April 08, 1988

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
October 13, 1987

Seminar The ONTIC System
by David McAllister
October 06, 1987

Melis, Erica

Seminar Proof presentation in the Omega system
by Erica Melis
October 25, 1999

Seminar Knowledge-Based Proof Planning
by Erica Melis
April 19, 1999

Mendler, Nax P.

Seminar M-L Type Theory, Categories, Inductive Types
by Nax P. Mendler
1990 Summ

Seminar Polymorphism Is Not Set Theoretic
by Nax P. Mendler
February 14, 1990

Seminar Strong Normalization in Lambda2
by Nax P. Mendler
October 02, 1986

Seminar PP-lambda in Nuprl
by Nax P. Mendler
1984-1985

Seminar Denotational Semantics
by Nax P. Mendler
1984-1985

Seminar Partial Recursive Functions
by Nax P. Mendler
1984-1985

Misra, Jaydev

Seminar Structured Concurrent Programming
by Jaydev Misra
September 15, 2006

Mitchell, John

Seminar Empty Types
by John Mitchell
September 25, 1986

Moczydlowski, Wojciech

Seminar Extraction in IZF
by Wojciech Moczydlowski
February 25, 2005

Seminar Set-theoretical models of type theory (cont.)
by Wojciech Moczydlowski
September 20, 2004

Seminar Set-theoretical models of type theory
by Wojciech Moczydlowski
September 13, 2004

Seminar (Constructive) set-theoretic semantics for (Constructive) higher-order logic
by Wojciech Moczydlowski
November 04, 2005

Seminar Coq and Nuprl
by Wojciech Moczydlowski
July 27, 2004

Moore, J Strother

Seminar An ACL2 Demo
by J Strother Moore
October 07, 2002

Moran, Evan

Seminar Order-theoretic Differences Between Two Variants of Type Theory
by Evan Moran
October 19, 2012

Seminar Unions and Unboxed Quotients
by Evan Moran
September 23, 2005

Seminar Non-existence of Unions
by Evan Moran
March 04, 2005

Seminar Separativeness and the Structure of the Singletons
by Evan Moran
October 18, 2004

Seminar Reversing Howe's Substitution Rule
by Evan Moran
September 27, 2004

Seminar Uniform Inhabitants for the Non-Union Blueprints, continued
by Evan Moran
October 28, 2005

Seminar (Re-)Introduction to Howe's Framework, continued
by Evan Moran
October 14, 2005

Seminar (Re-)Introduction to Howe's Framework
by Evan Moran
September 30, 2005

Seminar CFZ From Below (continued)
by Evan Moran
April 19, 2004

Seminar CFZ From Below
by Evan Moran
April 12, 2004

Seminar Discussion of Methods of Sharing Formal Mathematics
by Evan Moran
September 22, 2003

Seminar Bridges Between Set Theory and Type Theory
by Evan Moran
September 15, 2003

Seminar On Howe's Importation of HOL into Nuprl
by Evan Moran
September 29, 1998

Seminar Adding Intersection Types to Doug Howe's Classical Set-Theoretic Semantics
by Evan Moran
April 07, 1998

Seminar CZF, Type Theory, and Nuprl-Light (continued)
by Evan Moran
April 08, 1997

Seminar CZF, Type Theory, and Nuprl-Light
by Evan Moran
April 01, 1997

Mota, Francisco

Seminar Constructive Topology - A Theory of Observation
by Francisco Mota
October 15, 2014

Seminar Synthetic Topology in NuPRL
by Francisco Mota, Mark Bickford
December 03, 2014

Moten, Roderick

Seminar Design of the Nuprl Refiner
by Roderick Moten
September 26, 1995

Seminar The Refiner as the Inference Mechanism of Nuprl Proof Development System
by Roderick Moten
April 04, 1995

Seminar Tactic Trees in eXene
by Roderick Moten
September 22, 1992

Murthy, Chetan

Seminar Chet Says Good-Bye: Theory; Implementation (System); Methodology; Science
by Chetan Murthy
February 14, 1995

Seminar The Engineering Aspects of Proof-Environment Design
by Chetan Murthy
January 24, 1995

Seminar TLA
by Scott D. Stoller, Chetan Murthy
November 01, 1994

Seminar A (Possibly) New Scheme for Libraries/Proof-Contexts
by Chetan Murthy
September 03, 1993

Naumov, Pavel

Seminar Importing Isabelle Formal Mathematics into NuPRL
by Pavel Naumov
March 08, 1999

Seminar iPRL: A General Approach to Interpreting Isabelle Results in NuPRL
by Pavel Naumov
September 08, 1998

Seminar Presenting Semantics for a Fragment of the Java Programming Language in Nuprl Proof Development System
by Pavel Naumov
March 10, 1998

Seminar References in Type Theory
by Pavel Naumov
November 25, 1997

Seminar Reasoning about Java Classes in Nuprl (continued)
by Pavel Naumov
September 16, 1997

Seminar Reasoning about Java Classes in Nuprl
by Pavel Naumov
September 09, 1997

Nogin, Aleksey

Seminar Review of Theorem Provers Outside Cornell part 2
by Aleksey Nogin
February 18, 2002

Seminar Review of Theorem Provers Outside Cornell part 1
by Aleksey Nogin
February 11, 2002

Seminar Is a type uniquely determined by its equivalence relation?
by Aleksey Nogin
November 26, 2001

Seminar Trip Report
by Aleksey Nogin
October 22, 2001

Seminar Markov's Principle for Propositional Type Theory
by Aleksey Nogin
August 20, 2001

Seminar Modular approach to formalization of the quotient types
by Aleksey Nogin
April 23, 2001

Seminar Modular approach to quotient and other types
by Aleksey Nogin
April 16, 2001

Seminar New modular approach to formalizing complex types in type theory
by Aleksey Nogin
April 09, 2001

Seminar Internalizing proofs and provability
by Aleksey Nogin
February 19, 2001

Seminar 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

Seminar 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

Seminar 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

Seminar A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory
by Alexei Kopylov, Aleksey Nogin
November 27, 2000

Seminar A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory (cont)
by Aleksey Nogin, Alexei Kopylov
December 04, 2000

Seminar Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999

Seminar Differences between the MetaPRL type theory and the Nuprl type theory
by Aleksey Nogin
April 10, 2000

Seminar Efficient Programming by Extract in Nuprl Type Theory - Continued
by Aleksey Nogin
February 14, 2000

Seminar Efficient Programming by Extract in Nuprl Type Theory
by Aleksey Nogin
February 07, 2000

Seminar The Status of the Meta-Prl Project
by Aleksey Nogin
October 04, 1999

Seminar The Current Projects of the MetaPRL Group
by Aleksey Nogin, Jason Hickey
April 26, 1999

Seminar Speeding Up the MetaPRL Refiner
by Aleksey Nogin
February 08, 1999

Seminar Formal Models for Nuprl Evaluator
by Aleksey Nogin
March 24, 1998

Nogina, Elena

Seminar On continuity of computable real functions
by Elena Nogina
May 01, 2000

O'Donnell, Michael J.

Seminar Connecting Formal Semantics to Constructive Intuitions
by Michael J. O'Donnell
July 06, 1993

Otten, Jens

Seminar Efficient Automated Proof Search and Proof Reconstruction in Intuitionistic Logic
by Jens Otten, Stephan Schmitt
June 23, 1998

Paulin-Mohring, Christine

Seminar Recursive Types in Coq
by Christine Paulin-Mohring
September 08, 1994

Petride, Sabina

Seminar Uri Abraham's Models for Concurrency
by Robert L. Constable, Sabina Petride
January 27, 2003

Seminar The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002

Pientka, Brigitte

Seminar Instantiation of Existentially Quantified Variables in Inductive Specification Proofs
by Brigitte Pientka
May 05, 1998

Seminar A Uniform Rippling Approach for Instantiating Free Variables
by Brigitte Pientka
December 02, 1997

Pingali, Keshav

Seminar Distributed Snapshot Algorithms
by Keshav Pingali
February 17, 2003

Poernomo, Iman

Seminar Adapting Proofs-as-Programs for the Synthesis of Imperative SML Programs
by Iman Poernomo
December 08, 2003

Poetzsch, Arnd

Seminar Formalizing Program Synthesis
by Arnd Poetzsch
April 27, 1993

Rahli, Vincent

Seminar A Type Theory with Partial Equivalence Relations as Types
by Vincent Rahli
September 10, 2014

Seminar There Are No Discontinuous Real Functions
by Mark Bickford, Vincent Rahli
October 08, 2014

Seminar Nominal Type Theory
by Mark Bickford, Vincent Rahli
October 29, 2014

Seminar A verified proof assistant
by Vincent Rahli, Abhishek Anand
October 30, 2013

Seminar How far can we go with Induction-Recursion?
by Abhishek Anand, Vincent Rahli
November 20, 2013

Seminar Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011

Reitblatt, Mark

Seminar ACL2 Tutorial
by Mark Reitblatt
March 27, 2014

Seminar Recent work with Coq
by Mark Reitblatt
May 11, 2012

Remidde, Ettore

Seminar GOLEM
by Ettore Remidde
October 24, 1995

Sasaki, James T.

Seminar Optimizing Ext
by James T. Sasaki
1984-1985

Schlimm, Dirk

Seminar Intuitionism - The Philosophy of L. E. J. Brouwer
by Dirk Schlimm
April 24, 1998

Schmitt, Stephan

Seminar An Efficient Refiner for First-order Intuitionistic Logic (Part II)
by Stephan Schmitt
May 22, 2000

Seminar An Efficient Refiner for First-order Intuitionistic Logic
by Stephan Schmitt
February 28, 2000

Seminar Efficient Automated Proof Search and Proof Reconstruction in Intuitionistic Logic
by Jens Otten, Stephan Schmitt
June 23, 1998

Schwartzbach, Michael

Seminar Continuation of Categorial Models of Nuprl
by Michael Schwartzbach
October 28, 1986

Seminar Categorical Models of Nuprl
by Michael Schwartzbach
October 21, 1986

Schwichtenberg, Helmut

Seminar Program Development for Proof Transformations
by Helmut Schwichtenberg
October 12, 1994

Seminar Are There Long Reduction Sequences with Short Normal Forms?
by Helmut Schwichtenberg
September 29, 1992

Shan, Chung-chieh

Seminar Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
by Chung-chieh Shan
December 02, 2011

Shankar, N

Seminar PVS
by N Shankar
March 24, 1992

Shvartsman, Alex

Seminar A Reconfigurable Atomic Memory Service for Dynamic Networks
by Alex Shvartsman
March 24, 2003

Smith, Scott F.

Seminar Partial Objects
by Scott F. Smith
November 24, 1987

Seminar Domains in Type Theory
by Scott F. Smith
November 10, 1987

Seminar Bar Types
by Scott F. Smith
March 18, 1987

Seminar Term Model Semantics and Tait Computability Method
by Scott F. Smith
March 11, 1987

Seminar Defining Lambda-prl and Its Extensions
by Scott F. Smith
1984-1985

Smolka, Steffen

Seminar Isabelle Tutorial
by Steffen Smolka
March 18, 2014

Stansifer, Ryan

Seminar Marhew's Principle
by Ryan Stansifer
1984-1985

Seminar Prolog
by Ryan Stansifer, Stuart F. Allen
1984-1985

Stehr, Mark-Oliver

Seminar 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

Seminar 20BJ as a Meta-logical Framework
by Andrew Stevens
April 21, 1990

Seminar Rational Reconstruction of Boyer and Moore Prover
by Andrew Stevens
December 01, 1987

Stoller, Scott D.

Seminar TLA
by Scott D. Stoller, Chetan Murthy
November 01, 1994

Seminar An Operational Approach to Combining Classical Set Theory and Functional Programming Languages
by Scott D. Stoller
March 29, 1994

Seminar How to Integrate Set Theory and Computation?
by Scott D. Stoller
September 14, 1993

Seminar Semantics
by Scott D. Stoller
March 30, 1993

Seminar Semantics of the Nuprl Type Theory
by Scott D. Stoller
March 16, 1993

Stump, Aarong

Seminar Proof Tools and Correct Program Development
by Aarong Stump
February 03, 2003

Tate, Ross

Seminar Issues in Constructive Type Theory
by Ross Tate
September 14, 2012

Underwood, Judith

Seminar A Constructive Completeness Proof for Intuitionistic Predicate Calculus
by Judith Underwood
February 01, 1994

Seminar Extraction
by Judith Underwood
March 16, 1993

van Dalen, Dirk

Seminar L. E. J. Brouwer's Intuitionism: A Revolution in Two Installments
by Dirk van Dalen
June 26, 1998

Vardi, Moshe

Seminar A Conversation with Moshe Vardi
by Moshe Vardi
November 18, 2011

Walker, David

Seminar Regions, part 2: The Capability Calculus
by David Walker
November 15, 1999

Seminar An Introduction to Region Inference
by David Walker
November 08, 1999

Weirich, Stephanie

Seminar Intensional Polymorphism in Type-Erasure Semantics
by Stephanie Weirich
April 28, 1998

Werner, Benjamin

Seminar Extraction of Programs
by Benjamin Werner
1993-1994

Wilson, Todd

Seminar Work in Progress: A Formalization of the SUP-INF Algorithm
by Todd Wilson
July 11, 1996

Seminar Some Recent Results of R. Dyckhoff and A. Pitts
by Todd Wilson
March 26, 1996

Seminar Motivation: Basis of a Set Theory for Nuprl
by Todd Wilson
February 21, 1995

Seminar Computer Algebra, Theorem Proving, and Types
by Todd Wilson
October 04, 1994

Wu, Jason

Seminar 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

Seminar A Discussion in Consensus
by Jason Wu
February 10, 2012

Seminar Adding Shared Memory to the General Process Model
by Jason Wu
April 20, 2012

Yan, Thomas

Seminar Gröbner Basis
by Thomas Yan
September 20, 1994

Seminar Hilbert Basis Function
by Thomas Yan
March 01, 1994

Zippel, Richard

Seminar The MathBus Term Structure
by Richard Zippel
1995-1996