Logic of Programs CS 6860

CS 6860 Fall 15:

Announcements:

Instructor:

Robert Constable

Time:

Tues/Thurs

10:10AM - 11:25AM

Location:

Upson 215

Schedule & Readings
CS6860 - Fall 2015

DateTopicNotes
Aug 25 -Introduction to the course
Aug 27 -Smullyan's Propositional Calculus
Sept 1 -Recommended reading
-Styles of proof
Sept 3 -Minimal propositional calculus
Sept 8 -Minimal propositional calculus continued
Sept 10 -iPC and mPC
-Computational content
Sept 15 -Computational content of any(t)
  • Lecture 7 Notes
  • Proof and computation rules, Sections 2.2-2.3 from Intuitionistic completeness of first-order logic, Robert Constable and Mark Bickford. In the Annals of Pure and Applied Logic, vol. 165, January 2014.
Sept 17 -Intuitionistic logic
-Constructive logic
Sept 22 -Propositional Calculus as a programming language
Sept 24 -Evidence semantics
-New semantics for iPC
-Classical PC
Sept 29 -Gilvenko's theorem
-Building proofs by evidence term
Oct 1 -Evidence terms
Oct 6 -Visser rules
Oct 8 -Completeness
Oct 16 -More on completeness and the intersection type
Oct 20 -More on completeness and iFOL
Oct 22 -Computable functions
-More on completeness
Oct 27 -Dummett and intuitionism
Oct 29 -Second-order intuitionistic logic
Nov 3 -Second-order intuitionistic logic
Nov 5 -More second-order intuitionistic logic
Nov 10 -More second-order logic
Nov 12 -Relating classical and constructive logic
Nov 17 -Classical and constructive logic
Nov 17 -Second order logic
Nov 24 -Second-order logic proof
Nov 26 Thanksgiving
Dec 1 -Type Theory
Dec 3 -Protocols