Skip to main content
Cornell University


Meeting Tue/Thr 2:55pm - 4:10pm in Phillips 403

DateTopic Notes/Readings
Week 1
8/22 Introduction

Lecture 1

8/24 Introduction

Lecture 2

Principia Mathematica: The Theory of Logical Types

Hoare: Notes on Data Structuring

The Principles of Mathematics: The Doctrine of Types

Week 2
8/29 Introduction to First Order Logic

Lecture 3

Kleene Forward by Michael Beeson


8/31 Proof Styles and First Order Logic

Lecture 4

On the Meanings of Logical Constants and the Justifications of the Logical Laws

A new translation of L.E.J Brouwer's `Unreliability of the Logical Prinicples'

Types in Logic, Mathematics, and Programming from the Handbook of Proof Theory

Week 3
9/5 Number Theoretic Functions and Mathematical Induction

Lecture 5

Nuprl Proof : Integer Square Root Exists

Nuprl Proof: Example1

Nuprl Proof: Example2

9/7 Ancestral Logic

Lecture 6

Ancestral Logic

Week 4
9/12 Basic Types of CTT

Lecture 7

The Structure of Nuprl's Type Theory

9/14 Basic Types of CTT continued

Lecture 8

The Type Theoretic Interpretation of Constructive Set Theory

Constructive Mathematics and Computer Programming

Week 5
9/19 A Review of First-Order Logic

Lecture 9

The Structure of Nuprl's Type Theory

9/21 Evidence Semantics

Lecture 10

Reading: Evidence Semantics

Week 6
9/26 Implementing Euclid's Elements in Nuprl's Type Theory

Lecture 11 Intro

Presentation: Finding and Extracting Computational Content in Euclid's Elements

9/28 Creating and Organizing Evidence in Type Theory

Lecture 12

Week 7
10/3 The Structure of Refinement Proofs

Lecture 13

Supplementary Proofs

10/5 Nuprl Demonstration

Prof. Christoph Kreitz gave a demonstration of Nuprl and took questions.

Supplementary Proofs

Logical Investigations, with the Nuprl Proof Assistant

Week 8
10/10 Fall Break
10/12 Markov's Principle in Constructive Type Theory

Lecture 15

Constructive Analysis in Nuprl

Week 9
10/17 The Constructive Real Numbers

Lecture 16

Constructive Analysis in Nuprl (1)

10/19 The Constructive Real Numbers

Constructive Analysis in Nuprl (2)

Constructive Analysis in Nuprl (3)

Lecture 17

John Myhill : What is a Real Number?

Week 10
10/24 The Constructive Real Numbers

Lecture 18

Elementary Calculus - Keisler

10/26 Infinitessimal Calculus

Foundations of Infinitessimal Calculus

Lecture 19

Week 11
10/31 Constructive Nonstandard Models

Lecture 20a

Lecture 20b

11/2 Hybrid First Order Logic

Lecture 21

Lecture 21 Supplement

Week 12
11/7 Theory of Computability in CTT

Lecture 22

Computability and Recursion

11/9 Basic Recursive Function Theory in CTT

Lecture 23

Computational foundations of basic recursive function theory

Week 13
11/14 Asynchronous Distributed Computing

Lecture 24

Distributed Computing Slides

Generating Event Logics with Higher-Order Processes as Realizers

11/16 A Logical Foundation for Security

Lecture 25

An Abstract Semantics for Atoms in Nuprl

Unguessable Atoms

Week 14
11/28 Automated Reasoning and Ultra-Intuitionism

Lecture 26

Inconsistency of Primitive Recursive Arithmetic

11/30 The Age of Intelligent Machines

Lecture 27