More course notes will become available soon
| |
|||||
| 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:
Meta-Reasoning
(slides only)
|
PS | ||||
|
Lecture 24:
Reflection
(slides only)
|
PS | ||||
|
Lecture 25:
Undecidability, Incompleteness and
Undefinability
|
Handwritten notes only | ||||
|
Lecture 26:
Expressing Unsolvability in a Type-theoretical
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