View readings by author
Schedule & Readings
CS5860 - Fall 2014
Aug. 27 - Introduction to Course & Area of Formal Methods
- Lecture 1 Notes: PDF
Sept 1 - No class, Labor Day
Sept 3 - Specification Languages
- Lecture 2 Notes: PDF
Sept 8 - Computability, Unrealizable Types/Propositions
- Lecture 3 Notes: PDF
Sept 10 - Propositions as Types and Construction of Evidence as Proofs
- Lecture 4 notes: PDF
Sept 15 - Predicate Calculus (First-Order Logic)
- Lecture 5 Notes: PDF
- Constable: Proof Rules for ituitionistic First Order Logic in Refinement Style
Sept 17 - More Predicate Calculus and Progamming Problems Expressed as Types
Sept 22 - Predicate Calculus
- Lecture 7 Notes: PDF
Sept 24 - Q
- Lecture 8 Notes: PDF
- Rahli: Library Q
- Boolos and Jeffrey: Representability in Q and Undecidability, indefinability and incompleteness
Sept 29 - Equality
- Lecture 9 Notes: PDF
Oct 1 - No class, Gates Hall dedication and 50th Anniversary of CS Department events
Oct 6 - iQ
- Lecture 10 Notes: PDF
Oct 8 - Primitive recursive arithmetic
- Lecture 11 Notes: PDF
- Kleene: Postulates from Kleene's Introduction to Meta-Mathematics
- Martin-Löf: Informal Notes on Foundations
Before reading Martin-Löf, think about and write down what your defintion of 'zero' is right now. Compare this to what he defines.
Oct 13 - No class due to fall break
Oct 15 - Foundations of Number Theory
- Lecture 12 Notes: PDF
Oct 20 & Oct 22 - Numerical Specifications and Programs
- Lecture 13 and 14 Notes: PDF
Oct 27 - Algorithm for the Integer Square Root
- Lecture 15: Nuprl page
- Kreitz: PDF
Oct 29 - Real Numbers
- Lecture 16: PDF
- Formalizing Constructive Analysis in Nuprl: Nuprl page
- Allen: Square Root of 2 is Irrational
Nov 3 - Real Analysis
Nov 5 - Bishop and Cantor Theorems
- Lecture 18: PDF
Nov 10 - Foundations of Constructive Mathematics
Nov 12 - Semantics
- Lecture 20: PDF
- Martin-Löf: Constructive Mathematics and Computer Programming
- Constable: Handbook of Proof Theory
- Bishop: Aspects of Constructivism
Nov 17 - Type Theory
- Lecture 21: PDF
- K. Kunen: 9 Axioms of Set Theory
- Stuart Allen: A Non-Type-Theoretic Definition of Martin-Löf's Types
Nov 19 - Introduction to Process Event Theory for Distributed Computing
- Lecture 22: PDF
- Selected Distributed Computing Literatures: References
- Distributed Systems Talk: Event Structures over Process Models
- Bickford, Constable, and Guaspari: Generating Event Logics with Higher-Order Processes as Realizers
Nov 24 - Guest lecture by Abhishek Anand
Dec 1 - Consensus Protocols
- Lecture 23: PDF
- Rahli, Guaspari, Bickford, and Constable Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
Dec 3 - Summary of Topics
- Lecture 24: PDF