CSE433 Logic in Computer Science  Schedule
[ Home
 Schedule
 Assignments
 Software
 Resources
 Students
]
gla@postech Sungwoo Park
 The schedule is subject to change throughout the semester.
 CS = Course Notes.
(The uptodate version including all chapters
[PS, PDF])
)
Date 
Lecture 
Reading 
Quiz and Assignment Due 

Tue  Sep  4  
Judgments, Inference rules, Inductive proofs
(No class  Inauguration ceremony. To be rescheduled: 10am, Sep 7, in the classroom) 
CSE321 Programming Languages Course Notes Chapter 2
[PS,
PDF]


Thu  Sep  6  
Inductive proofs, Overview of logic 



Thu  Sep  11  
Propositions, Propositional logic, 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]

Quiz 1
[PS,
PDF ]

Thu  Sep  13  
Notational definition, Logical equivalence

class1.v 
Assignment 1 

Tue  Sep  18  
Hypothetical judgments, Substitution principle, Structural properties 


Thu  Sep  20  
Local soundness and completeness, Proof reduction and expansion 

Assignment 2 

Tue  Sep  25  
(No class  Chusok)



Thu  Sep  27  
Normal proofs, Normalization 



Tue  Oct  2  
CurryHoward isomorphism
(Instructor out of town. To be rescheduled: 11:45am, Sep 28, in the classroom)

CS Chapter 2 [PS, PDF]


Thu  Oct  4  
Properties of proof terms


Assignment 3 

Tue  Oct  9  
Firstorder logic  Introduction 
CS Chapter 3 [PS, PDF]

Quiz 2
[PS,
PDF ]

Thu  Oct  11  
Firstorder logic  Quantifications 



Tue  Oct  16  
Firstorder logic  Soundness and completeness 

Assignment 4 
Thu  Oct  18  
Firstorder logic  Proof terms 



  
Midterm,
Oct 25 (Thursday), 10am  1pm, classroom. Closed book.
Exam [PS, PDF]
Solution [PS, PDF]

Assignment 5
(Oct 23)


Tue  Oct  30  
Introduction to datatypes 
CS Chapter 5 [PS, PDF]
 

Thu  Nov  1  
Primitive recursion 



Tue  Nov  6  
Predicate on terms 


Thu  Nov  8  
Induction on terms 



Tue  Nov  13  
Proof terms 

Thu  Nov  15  
Examples of induction 


Tue  Nov  20  
Induction on predicates 

Assignment 6 
Thu  Nov  22  
Examples of induction on predicates 



Tue  Nov  27  
Definitional equality 

Assignment 7 
Thu  Nov  29  
Classical logic
(Instructor out of town. To be rescheduled: 7:00pm, Dec 12, in the classroom)
 CS Chapter 6 [PS, PDF]
 

Tue  Dec  4  
CPS transformation 

Assignment 8 
Thu  Dec  6  
Linear logic (I) 
Chapters 1 and 2 of Course Notes
by Frank Pfenning
 

Tue  Dec  11  
Linear logic (II) 


Thu  Dec  13  
Review 



  
Final Exam
Dec 18 (Tuesday), 7pm  10pm (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
