CPSC 629 Deductive Systems


Abstract:
=========

We explore the theory of programming languages and the design of
logics using deductive systems.  In particular, we discuss how to
specify, implement, and verify properties of functional and logic
programming languages.

The deductive approach to the specification of programming languages
has become standard practice, and one of the goals of this course is
to provide good working knowledge of how to engineer language
descriptions, how to implement and experiment with related algorithms
such as operational semantics, and how to verify properties about the
design.  Throughout this course we will use the Twelf system as a
uniform meta-language in which we can express specification and
implementation, and meta-theory of the object languages we are
considering.


Lecture 1 : The programming language Mini-ML
Lecture 2 : Mini-ML's meta theory (Value soundness)
Lecture 3 : Simply typed lambda-calculus
Lecture 4 : Logical frameworks
Lecture 5 : Twelf
Lecture 6 : Hypothetical judgments
Lecture 7 : Type preservation for Mini-ML	
Lecture 8 : Induction  (informal introduction of meta-logic)
Lecture 9 : Meta-logical frameworks
Lecture 10: The meta-logic M2
Lecture 11: Proof terms
Lecture 12: Termination 
Lecture 13: Case analysis
Lecture 14: Compilation: CPM machine
Lecture 15: Compilation: Completeness theorem
Lecture 16: Compilation: Soundness theorem
Lecture 17: Church-Rosser theorem (for ulc)
Lecture 18: Church-Rosser theorem (for ulc)
Lecture 19: Intuitionistic Logic: Natural deduction calculus
Lecture 20: Intuitionistic Logic: Sequent calculus 
Lecture 21: Cut eliminiation theorem
Lecture 22: Logic Programming
Lecture 23: Hereditary Harrop formulas
Lecture 24: Resolution
Lecture 25: Uniform Proofs
Lecture 26: Project presentations


Project proposals are due beginning of Lecture 17
Project papers are due beginning of Lecture 26