For lectures 2-4 see Stuart Allen's notes
Back to overview of courses
|
||||
|
||||
|
Summary |
||||
|
CS 786 is an advanced
graduate course on the foundations of Type Theory and of the Nuprl System.
Course notes and slides are available in postscript and PDF format. Notes are also provided in 2:1 reduced postscript format and slides in 4:1 reduction. |
||||
| Lecture 5: The NuPRL Type Theory: Syntax & Semantics (Slides) | |||||
| Lecture 6: The NuPRL Type Theory: Inference System (Slides) | |||||
| Lecture 7: The Types of NuPRL (Slides) | |||||
| |
|||||
| NuPRL 5 Manual, Appendix A: The Basic Nuprl Type Theory (Draft) | |||||
| The NuPRL 4.2 manual is still a good source of information | |||||
| There are also draft notes from a 1985 lecture, when Nuprl had just come out. | |||||
|
For lectures 2-4 see Stuart Allen's notes |
|||||
|
If you understand German, you may want to look up my 1995 course notes on
Automated Logic and Programming
|
|||||
|
The 1986 book
Implementing Mathematics with the NuPRL proof development system
is available online as well
|
|||||
|
Back to overview of courses |
|||||
This page is still under construction.
