### Instructor: Dale Miller

lectures / homeworks / modules
*** The following course description is a small part of the final class. Only those parts particularly related to lambda Prolog are included here. ***
Course Description: This course should prove useful to anyone interested in computational uses of logic, especially those interested in Cognitive Science and Programming Languages. Logic programming will be taught and used in class to solve problems in cogitive science, AI, and programming languages.
• Syntax, proof theory, model theory, and operational semantics of various logics (classical, intuitionistic, linear).
• Presentation of the logic programming paradigm using the lambda Prolog language. This programming language incorporates large amounts of logic and will be used to illustrate and apply logical principles.
• Topics: typed lambda-calculus; propositions-as-types; natural deduction; sequent calculus; cut-elimination; implementations of natural deduction and sequent calculi; tactics and tacticals; proof and program transformations; explanation based generalization; parsing-as-deduction; meta-level and object-level distinctions; and classical, intuitionistic, linear, and modal logics.

Prerequisites: CSE 120 and some sophistication with proofs by induction (CSE 260 or Phil 5/6)

Textbook: "lambda Prolog: An Introduction to the Language and its Logic" (current draft) by Dale Miller. Additional course notes will also be used.

Grading: A combination of homework assignments, in-class exams, and (possibly) a final will be used to determine grades. It is expected that all homework is the work of individuals working independently.

Course Outline

• Simple types; Curry-Howard Isomorphism; propositional intuitionistic logic.
• Syntax and operational semantics of Prolog and lambda Prolog; kinds, types, modules, abstract datatypes.
• Inference rules; natural deduction; Horn clauses as natural deduction.
• Computation as proof-search versus proof-reduction; comparison of logic programming and functional programming.
• Unification, depth-first search, backtracking.
• Deductive databases; hypothetical reasoning; module importing.
• lambda-calculus, lambda-conversion, unification of lambda-terms; meta-level and object-level distinctions.
• Higher-order programming in logic programming; tactic-style theorem provers.
• Explanation based generalization; theorem proving strategies; parsing-as-deduction; program transformation; specifications of static and dynamic semantics of programming languages.
• Minimal models; fixed point proofs; Kripke models.
• Substructural logics: relevance, linear.