## CS 5860 Fall 14:

## Announcements:

Projects due Thursday, December 11. Early submissions greatly encouraged!

## Instructor:

Robert Constable

## Time:

Mon/Weds

10:10AM - 11:25AM

## Location:

Upson 211

Projects due Thursday, December 11. Early submissions greatly encouraged!

Robert Constable

Mon/Weds

10:10AM - 11:25AM

Upson 211

View readings by author

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