CPSC 629: Deductive Systems

 

Instructor: Carsten Schürmann
Department of Computer Science
Yale University
Time: TTh 4:00-5:15
Room: AKW 500

  Home
  Schedule
  Handouts
  Assignments
  Projects
  Links
 
  

Schedule

Lecture 1 : The Programming Language Mini-ML
Lecture 2 : Mini-ML's Operational Semantics
Lecture 3 : Mini-ML's Typing Discipline
Lecture 4 : Typing Preservation for Mini-ML
Lecture 5 : Higher-Order Abstract Syntax
Lecture 6 : The Simply Typed Lambda Calculus
Lecture 7 : The Logical Framework LF: Part I
Lecture 8 : The Logical Framework LF: Part II
Lecture 9 : Twelf
Lecture 10 : Hypothetical Judgments
Lecture 11 : Meta-Theory
Lecture 12 : Type Preservation For Mini-ML
Lecture 13 : Natural Deduction
Lecture 14 : Recitation
Lecture 15 : Sequent Calculus
Lecture 16 : Curry-Howard Isomorphism
Lecture 17 : The Meta-Logic M2+ (Part I)
Lecture 18 : The Meta-Logic M2+ (Part II)
Lecture 19 : Compilation: The CPM machine
Lecture 20 : Compilation: de Bruijn Encoding
Lecture 21 : Compilation: de Bruijn Transformation
Lecture 22 : Compilation: CLS machine
Lecture 23: Compilation: Soundness theorem
Lecture 24: Church-Rosser theorem (for ulc)
Lecture 25: Church-Rosser theorem (for ulc)
Lecture 26: Project presentations