

Notes from the current course 


Part I: Foundations of Computational Type Theory  
Lecture 1:
Why Computational Type Theory?

PS  
Lecture 2:
What is a type? (I)
(Formal Language, Evaluation)

PS  
Lecture 3:
What is a type? (II)
(Semantics, Proof Theory)

PS  
Lecture 4:
Primitive Recursive Functions in Type Theory

PS  
Lecture 5:
Research Directions (I)
(Bar Types and Partial Recursive Functions)

Handwritten notes only  
Lecture 6:
Research Directions (II)
(Church's Thesis)

Handwritten notes only  
Lecture 7:
Research Directions (III)
(Halting Problem and Rice's Theorem)

Handwritten notes only  
Part II: The core of NuPRL's type theory  
Lecture 8:
Introduction to NuPRL
(slides only)

PS  
Lecture 9:
Tactical Theorem Proving in NuPRL
(slides only)

PS  
Lecture 10:
Refinement Logic

PS  
Lecture 11:
Propositions as Types
(historical development)

Handwritten notes only  
Lecture 12:
Propositions as Types (II)

Handwritten notes only  
Lecture 13:
Extending Nuprl's Type Theory
(slides only)

PS  
Lecture 14:
Classical vs. Constructive Mathematics
(Based on the 1989 paper "Assigning Meaning to Proofs")

Handwritten notes only  
Lecture 15:
Proof Automation in First Order Logic
(slides only)

PS  
Lecture 16:
Automatic Proof Procedures for Nuprl
(slides only)

PS  
Part III: Advanced Type Theory  
Lecture 17:
Dependent Products and Function Spaces
(slides only)

PS  
Lecture 18:
Intersection Types
(binary, family, dependent intersection
[See Kopylov's paper
PS
PDF]; subtyping)

Handwritten notes only  
Lecture 19:
Type Constructs based on Intersection (I)
(subtying, top, record types [Marktoberdorf Slides
PPT])

Handwritten notes only  
Lecture 20:
Type Constructs based on Intersection (II)
(dependent records, abstract data types, basic algebra)

PS  
Lecture 21:
Universes and Set Types
(slides only)

PS  
Lecture 22:
Quotient Types and Inductive Types
(slides only)

PS  
Lecture 23:
MetaReasoning
(slides only)

PS  
Lecture 24:
Reflection
(slides only)

PS  
Lecture 25:
Undecidability, Incompleteness and
Undefinability

Handwritten notes only  
Lecture 26:
Expressing Unsolvability in a Typetheoretical
Setting

Handwritten notes only  
Lecture 27:
Gödel's theorem and Reflected Formal Theories

Handwritten notes only  
Lecture 28:
Digital Libraries of Formal Algorithmic Knowledge

Handwritten notes only  


The 1986 book
Implementing Mathematics with the NuPRL proof development system
is available online and as printable version 

There are also draft notes from a 1985 lecture, when Nuprl had just come out.  
If you understand German, you may want to look up my 1995 course notes on
Automated Logic and Programming 

A preliminary version of that course in 1991 had an English manuscript.
The later sections of this manuscript were never completed though 

The NuPRL 5 Manual is now complete 
This page is still under construction. More course notes will become available soon