|
|
|
|
Part I: Foundations of Computational Type Theory
|
|
Lecture 1:
Why Computational Type Theory?
|
| |
PS |
PDF |
|
Lecture 2:
What is a type? (I)
(Formal Language, Evaluation)
|
| |
PS |
PDF |
|
Lecture 3:
What is a type? (II)
(Semantics, Proof Theory)
|
| |
PS |
PDF |
|
Lecture 4:
Primitive Recursive Functions in Type Theory
|
| |
PS |
PDF |
|
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 |
PDF |
|
Lecture 9:
Tactical Theorem Proving in NuPRL
(slides only)
|
| |
PS |
PDF |
|
Lecture 10:
Refinement Logic
(slides only)
|
| |
PS |
PDF |
|
Lecture 11:
Propositions as Types
|
| |
Handwritten notes only
|
|
Lecture 12:
Propositions as Types (II)
|
| |
Handwritten notes only
|
|
Lecture 13:
Extending Nuprl's Type Theory
(slides only)
|
| |
PS |
PDF |
|
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 |
PDF |
|
Lecture 16:
Automatic Proof Procedures for Nuprl
(slides only)
|
| |
PS |
PDF |
|
Part III: Advanced Type Theory
|
|
Lecture 17:
Dependent Products and Function Spaces
(slides only)
|
| |
PS |
PDF |
|
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 |
PDF |
|
Lecture 21:
Set Types, Quotient Types, and Inductive Types
(slides only)
|
| |
PS |
PDF |
|
Lecture 22:
Quotient Types and Inductive Types
(slides only)
|
| |
PS |
PDF |
|
Lecture 23:
Meta-Reasoning
(slides only)
|
| |
PS |
PDF |
|
Lecture 24:
Reflection
(slides only)
|
| |
PS |
PDF |
|
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
|
|
|
|
|
|
|
The NuPRL 5 Manual is currently at draft stage
|
|
|
|
Chapter 1:
Introduction
|
|
PS |
PS (2:1) |
PDF |
|
Chapter 2:
A quick overview
|
|
PS |
PS (2:1) |
PDF |
|
Chapter 3:
Running Nuprl
|
|
PS |
PS (2:1) |
PDF |
|
Chapter 5:
Editing Terms
|
|
PS |
PS (2:1) |
PDF |
|
Chapter 9:
Rules and Tactics
|
|
PS |
PS (2:1) |
PDF |
|
Appendix A:
The Basic Nuprl Type Theory
|
|
PS |
PS (2:1) |
PDF |
|
Appendix B:
Introduction to Nuprl ML
|
|
PS |
PS (2:1) |
PDF |
|
|
The NuPRL 4.2 manual is still a good source of information
|
|
|
|
|
