Course on Logic Programming (15-810D)

Instructor: Frank Pfenning, fp@cs, WeH 8127, x8-6343
Times: Tu Th 10:30-11:50
Room: WeH 5409
Credits: 1 CU (CS)
Mailing List: comp-ded@cs.cmu.edu; mail fp@cs to be included
Office Hours: By appointment or by chance (Mon, Wed, Fri preferred)
Course Directory: /afs/cs/user/fp/courses/95-lp

Quick Pointers:

Description

Logic programming is a paradigm in which specifications and programs are expressed within the same language. Traditionally, this language has been Prolog, a first-order Horn logic augmented with some extra-logical features. Modern research in logic programming is concerned with languages that are simultaneously more expressive and purer than Prolog, including types and modes, higher-order features, constraints, linearity and state, concurrency, and modules.

This course provides a thorough introduction to logic programming. We will follow two threads: in one thread we will discuss language design, programming techniques, and theoretical foundations, in the other efficient implementation. As a joint project we will construct a compiler, incrementally adding features as the class progresses.

Prerequisites

There are no formal prerequisites, but familiarity with Standard ML (the implementation language for the compiler) will be assumed. Students outside computer science and enterprising undergraduates are welcome, but require permission of the instructor.

Evaluation

Grades are based on class participation, homework (for the first part of the course) and the contribution to the class project.

Outline

  1. Computation as Proof Search
    1. Natural Deduction and Sequent Calculus
    2. Uniform Derivations
    3. Resolving Non-Determinism
    4. A First Interpreter
  2. Prolog
    1. Programming with Extra-Logical Constructs
    2. The Interpreter Revisited
    3. Common Techniques and Pitfalls
    4. Warren's Abstract Machine
  3. Structured Logic Programming
    1. Types and Polymorphism
    2. Modes and Directionality
    3. [Modules]
    4. [Subtyping]
  4. Constraint Logic Programming
    1. The CLP Model
    2. Some Constraint Domains
    3. Implementation Techniques
  5. Linear Logic Programming
    1. Linear Logic and Uniform Derivations
    2. Imperative Logic Programming
    3. Implementation Techniques
  6. [Reasoning about Logic Programs]
    1. [Proof Terms and Dependent Types]
    2. [Inductive Definitions]
    3. [Abstract Interpretation]
    4. [Advanced Compilation]
[Topics in brackets were not covered]

Course Material

Some notes and papers will be handed out and also available from my secretary (Marge Profeta, WeH 8110). We will also refer to the two books below, which have been put on reserve in the E&S library.
  1. Richard A. O'Keefe. The Craft of Prolog. MIT Press, 1990.
  2. Hassan Ait-Kaci. Warren's Abstract Machine: A Tutorial Reconstruction. MIT Press, 1991.

fp@cs