# 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:
## 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]