CS 6862 
Applied Logic 
Spring 2011 
Schedule and Lecture NotesHere is a list of the lectures planned for the course. Note that topics are subject to change. 

Date  Topic  Lecture Notes and Readings 
Jan 25  Course Introduction, the story of logic

Lecture 1: pdf 
Jan 27  Ways of defining logics formally, recursive types  Lecture 2: pdf 
Feb 1  Boolean logics propositional, first order (FOL) 
Lecture 3: pdf 
Feb 3  Computational logics  first order  Lecture 4: pdf 
Feb 8 
Evidence semantics  Lecture 5: pdf 
Feb 10  Evidence semantics continued  Lecture 6: pdf 
Feb 15  Consistency and completeness issues  Lecture 7: pdf 
Feb 17  Types and sets  Lecture 8: pdf 
Feb 22  FirstOrder theories PA, HA  Lecture 9: pdf 
Feb 24  Peano Arith (PA) and Heyting Arithmetic (HA)  Lecture 10: pdf 
Mar 1  Godel translation of PA into HA  Lecture 11: pdf 
Mar 3  Markov's Principle  Lecture 12: pdf 
Mar 8  Marvov's Principle (MP) and Hoare While Rule  
Mar 10  Consistency of Markov's Principle  Lecture 13: pdf 
Mar 15  Godel system T, higherorder functions 
Lecture 14: pdf 
Mar 17  Translating classical proofs to constructive proofs, Murthy results  Lecture 15: pdf Problem Set 3 
Mar 22  **Spring Break**  
Mar 24  **Spring Break**  
Mar 29  Brouwer ordinals and Wtypes  Lecture 16: pdf 
Mar 31 

Lecture 17: pdf 
Apr 5  Kleene theorem on recursive fans, Continuity principles 
Lecture 18: 
Apr 7  Brouwer's Bar Theorem, Kleene realizability 

Apr 12  MartinLof's Intuitionistic Type Theory (ITT) 

Apr 14  Realizing Bar Induction 
Lecture 21: pdf 
Apr 19  Howe's computational equality and Howe's trick  Lecture 22: pdf 
Apr 21  Partial equivalence relation (per) semantics  
Apr 26  Richer types  dependent records 

Apr 28  Bar types and unsolvable problems  Lecture 25: pdf 
May 3 May 5 
Process type Unsolvability without Church's Thesis (CT) 
Lecture 27: pdf 