Computation and Deduction (15-851)

Instructor: Frank Pfenning, fp@cs, WeH 8127, x8-6343
Times: TuTh 1:30-2:50
Room: WeH 5409
Credits: 1 CS core unit, 12 university units

We will explore the theory of programming languages using deductive systems. We will use such systems 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 a good working knowledge of how to engineer such language descriptions. Throughout the course we will use Elf as a uniform meta-language in which we can express specification, implementation, and meta-theory of the object languages we are considering. An implementation of Elf and examples will be available on-line for experimentation. Note that this course is an updated version of the course on Computation and Deduction in the Spring of 1992, but has little overlap with the course on Automated Theorem Proving in the Spring of 1993.

Course Notes and Assignments

Hardcopies of the course notes will be handed out. Other pointers:
  • list of assigned exercises
  • lecture announcement
  • draft course notes
  • suggested projects
  • lecture slides
  • implementation (in Elf)
  • Prerequisites

    There are no formal pre-requisites, but an exposure to functional programming and type systems might be helpful.

    Credit

    Credit (1 CS core unit) can be earned by doing homework (which will include some programming assignments) and a term paper. Homework is assigned frequently and is due one week later.

    Secretary

    Marge Profeta, profeta@cs.cmu.edu, WeH 8110, x8-5025

    Course Outline

    Material in brackets [] was not covered.
    0  Introduction and Overview
    
    1  Mini-ML
    1.1 Operational Semantics
    1.2 Value Soundness
    1.3 Type System
    1.4 Type Preservation
    
    2  Formalization in a Logical Framework
    2.1 Higher-Order Abstract Syntax
    2.2 Judgments as Types
    2.3 Higher-Level Judgments
    2.4 The LF Type Theory
    
    3  The Elf Programming Language
    3.1 A Mini-ML Interpreter
    3.2 An Implementation of Value Soundness
    3.3 Mini-ML Type Inference
    3.4 An Implementation of Type Preservation
    
    4  Aspects of Compilation
    4.1 Abstract Machines
    4.2 Compilation
    4.3 Compiler Correctness
    4.4 CPS Conversion and Callcc
    4.5 Properties of CPS
    
    5  Logic Programming
    5.1 Natural Deduction
    5.2 Normal Derivations and Proof Search
    5.2 Uniform Proofs
    5.3 Unification
    
    6  Formal Specifications
    6.1 Propositions as Types and Proofs as Programs
    6.2 Induction and Primitive Recursion
    6.3 Logical Interpretations
    
    [7  Equational Reasoning
     7.1 Rewriting
     7.2 A Church-Rosser Theorem
     7.3 Basic Concepts of Category Theory
     7.4 Cartesian Closed Categories]
    
    8  Advanced Type Systems
    8.1 Explicit Polymorphism
    8.2 The Calculus of Constructions
    [ 8.3 Subtyping and Intersection Types]