CSE490 Logic in Computer Science  Schedule
[ Home
 Schedule
 Assignments
 Software
 Resources
 Students
]
gla@postech Sungwoo Park
 Lectures are Monday and Wednesday 13:15pm  14:30pm, ¹«ÀºÀç±â³ä°ü 307È£.
 The schedule is subject to change throughout the semester.
 CS = Course Notes.
(The uptodate version including all chapters
[PS, PDF])
Date 
Lecture 
Reading 
Assignment Due 

Mon  Sep  4  
Judgments, Inductive proofs, Derivable rules, Admissible rules 
CSE321 Programming Languages Course Notes Chapter 2
[PS,
PDF]


Wed  Sep  6  
Propositions, Propositional logic (conjunction, implication, truth), Natural deduction 
CS Chapter 1 [PS, PDF]
On the Meaning of the Logical Constants and the Justification of the Logical Laws, MartinLöf
[HTML]
Truth of a Proposition, Evidence of a Judgement, Validity of a Proof, MartinLöf
[PDF]



Mon  Sep  11  
Propositional logic (disjunction, falsehood), Notational definition, Logical equivalence 


Wed  Sep  13  
Hypothetical judgments, Substitution principle, Structural properties 

Assignment 1 

Mon  Sep  18  
Local soundness and completeness 


Wed  Sep  20  
Proof reduction and expansion 



Mon  Sep  25  
Normal proofs 

Assignment 2 
Wed  Sep  27  
Normalization 



Mon  Oct  2  
CurryHoward isomorphism 
CS Chapter 2 [PS, PDF]


Wed  Oct  4  
Properties of proof terms 



Mon  Oct  9  
Sequent calculus 
CS Chapter 3 [PS, PDF]
 
Wed  Oct  11  
Cut elimination 



Mon  Oct  16  
Proof of normalization 

Assignment 3 
Wed  Oct  18  
Firstorder logic (1) 
CS Chapter 4 [PS, PDF]
 

  
Midterm,
Wednesday, Oct 25, 1:15pm  2:45pm, in the classroom. Closed book.
Exam [PS, PDF]
Solution [PS, PDF]


Mon  Oct  30  
Firstorder logic (2) 


Wed  Nov  1  
Firstorder logic (3) 



Mon  Nov  6  
Inductive datatypes, primitive recursion 
CS Chapter 5 [PS, PDF]
 
Wed  Nov  8  
(no class)




Mon  Nov  13  
Predicate on terms 


Wed  Nov  15  
Induction 



Mon  Nov  20  
Firstorder logic with datatypes 


Wed  Nov  22  
Classical logic, sequent calculus for classical logic 
CS Chapter 6 [PS, PDF]



Mon  Nov  27  
Double negation translation, CPS transformation 


Wed  Nov  29  
Linear logic 
Lecture notes by Frank Pfenning (PDF).
Chapters 1 and 2.



Mon  Dec  4  
Dual intuitionistic linear logic 


Wed  Dec  6  
Linear lambdacalculus 
Section 6.1 of Pfenning 


Mon  Dec  11  
(no class) 


Wed  Dec  13  
Modal logic 
Slide by Hyeonseung Im
Paper: A judgmental reconstruction of modal logic.
Pfenning and Davies.
[PDF]
[PS]


Fri  Dec  15  
Introduction to Coq
Mueunjae 309, 1:15pm 
[PPT]



  
Final Exam
Dec 20, 1pm  4pm (3 hours). Closed book.
Engineering building 109 (°øÇÐ2µ¿ 109È£)
Exam [PS, PDF]
Solution [PS, PDF]

[ Home
 Schedule
 Assignments
 Software
 Resources
 Students
]
gla@postech Sungwoo Park
