6180 An Introduction to Constructive Type Theory (Fall 2017)
Lectures
Meeting Tue/Thr 2:55pm  4:10pm in Phillips 403
Date  Topic  Notes/Readings  

Week 1  
8/22  Introduction  
8/24  Introduction 
Principia Mathematica: The Theory of Logical Types 

Week 2  
8/29  Introduction to First Order Logic  
8/31  Proof Styles and First Order Logic 
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  
9/7  Ancestral Logic  
Week 4  
9/12  Basic Types of CTT  
9/14  Basic Types of CTT continued 
The Type Theoretic Interpretation of Constructive Set Theory 

Week 5  
9/19  A Review of FirstOrder Logic  
9/21  Evidence Semantics  
Week 6  
9/26  Implementing Euclid's Elements in Nuprl's Type Theory  Presentation: Finding and Extracting Computational Content in Euclid's Elements  
9/28  Creating and Organizing Evidence in Type Theory  
Week 7  
10/3  The Structure of Refinement Proofs  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  Constructive Analysis in Nuprl  
Week 9  
10/17  The Constructive Real Numbers  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  Elementary Calculus  Keisler  
10/26  Infinitessimal Calculus  Foundations of Infinitessimal Calculus Lecture 19  
Week 11  
10/31  Constructive Nonstandard Models  Lecture 20b  
11/2  Hybrid First Order Logic  Lecture 21 Supplement  
Week 12  
11/7  Theory of Computability in CTT  Computability and Recursion  
11/9  Basic Recursive Function Theory in CTT  Computational foundations of basic recursive function theory  
Week 13  
11/14  Asynchronous Distributed Computing  Distributed Computing Slides Generating Event Logics with HigherOrder Processes as Realizers  
11/16  A Logical Foundation for Security  An Abstract Semantics for Atoms in Nuprl Unguessable Atoms 