View readings by author
Schedule & Readings
CS5860 - Fall 2011
Aug. 25 - Introduction to Course & Area of Formal Methods
- Gries - Why Use Logic?
- McCarthy - A Basis for a Mathematical Theory of Computation
Aug. 30 - Examples of using logic to reason about programs and processes
- Graham & Nademi - On Variations of Peterson's Mutual Exclusion Algorithm
- Hoare - An Axiomatic Basis for Computer Programming
Sept. 1 - An introduction to Classic ML and Event ML
- Lecture notes: PDF 1 slide per page | PDF 4 slides per page
- Kreitz & Rahli - Introduction to Classic ML
- EventML Installation:
Linux eventml_0.1-src.tar.gz updated 9/6/2011
Windows EventML-windows.zip updated 9/6/2011
See README file for instructions
Sept. 6 - Types and type inference in ML
- Lecture notes: PDF 1 slide per page | PDF 4 slides per page
Sept. 8 - CU Closed
Sept. 13 - Formal Logics - Introduction
- Lecture notes: PDF
- Smullyan: Tableau Proofs
new pages added 9/14 - Supplemental material : Core Type Theory
- Supplemental material : NP problems
Sept. 15 - Computational Logic
- Lecture notes: PDF
- Course notes: PDF
- Examples of Course Mini-Projects
- Constable: Semantics and Proof Rules
Sept. 20
Sept. 22 - Atomic Evidence, Examples of Computational Meaning of Logical Formulas, and Proofs
- Lecture notes: PDF
Sept. 27 - Logic of Quantified Statements
- Lecture notes: PDF
- Supplemental material: Smullyan: First Order Analytic Tableaux
Sept. 29 - Computational First-Order Logic
- Lecture notes: PDF
Oct. 4 - First-Order Logic as a Programming Language
- Lecture notes: PDF
Oct. 6 -Programmable Specifications
- Lecture notes: PDF
Oct. 11 -Fall Break
Oct. 13 -Formalizing Arithmetic
- Lecture notes: PDF - updated version posted 10/17
Oct. 18 -Formalizing Arithmetic Cont.
- Lecture notes: PDF - updated version posted 10/20
Oct. 20 - Arithmetic Specifications
- Lecture notes: PDF
- Supplemental material: The Stamps Problem: an example of induction
Oct. 25 - Induction
- Lecture notes: PDF
Oct. 27 - Induction and Interaction
- Lecutre notes: PDF
- Project Topics should be agreed on by the end of next week.
Please see Professor Constable before Nov 4 if you do not have an approved project. - Assignment: Please solve the exercises 1 to 6 on page 2 of the Oct. 25 lecture notes. Due Nov 7, 2011.
- Supplemental material: Manna Verification of Programs
- Supplemental material: Integer Square Root Derivation
- Collection of Boolean Logic Specifications: PDF
Nov. 1 - Program Verification
- Lecture notes: PDF
Nov. 3 - Recursion and Intro. to Event Logic
Nov. 8
- Lecture notes: not available online
Nov. 10 - Formal Applications in Security
- Lecture notes: PDF
Nov. 15 - Theory of Events in First Order Logic
- Lecture notes: Transcript | Hand written
- Supplemental material: PDF
Nov. 17 - Theory of Events
- Lecture notes: Transcript | Hand written
- Review of Induction: Transcript | Hand written
Nov. 22 - Consensus Protocols
- Lecture notes: PDF
- Assignment: a final homework question rev 11/23
Nov. 29 - Consensus Protocols
- Lecture notes: PDF
- Supplemental material : Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP
- Supplemental material: Halpern and Moses Knowledge and Common Knowledge in a Distributed Env
- Supplemental material: Guaspari: An Informal Explanation of Simple Consensus
Dec. 1 - Consensus Protocols
- Lecture notes: PDF
- Supplemental material: Halpern and Moses The Coordinated Attack Problem
- Supplemental material: Intro to Event ML
- Projects due at the end of the day, Wednesday December 7
- Extra credit reminders
see the end of Review of Indcution
and the bottom of page 1 in today's lecture notes