CS 6180 An Introduction to Constructive Type Theory

Lectures

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

Date	Topic	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 PLCV
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

6180 An Introduction to Constructive Type Theory- (Fall 2017)

Lectures