Logical Frameworks

Tutorial at CADE-12

Frank Pfenning

Department of Computer Science Carnegie Mellon University

For notes (in preparation) contact fp@cs.cmu.edu

Overview

1. Introduction

2. Syntax

3. Deductions

4. Meta-programming and search 5. Meta-theory

6. Conclusion

Deductive Systems

Deductive systems are a common conceptual tool in mathematical logic and computer science. They are used to specify, for example,

• Logics

• Type theories

• Type systems of programming languages

• Operational semantics

• Compilation • Algorithms (e.g. type inference, unification, theorem prov-

ing)

Logical Frameworks

A logical framework is a meta-language for the specification of deductive systems. Applications as a teaching and research tool include

• Reasoning within a specified logic

• Implementation of algorithms (evaluation, type inference)

• Reasoning about a deductive system

Brief History, I

• Automath [de Bruijn’68]

• Theory of Judgments [Martin-Löf’85]

• (Edinburgh) Logical Framework [Harper, Honsell & Plotkin’87] Elf [Pf’89,Pf’91]

• Hereditary Harrop Formulas [Nadathur, Miller, & Scedrov’87] [Paulson’87] λProlog [Nadathur & Miller’88] Isabelle [Paulson’89]

Brief History, II

• Inductive definitions / FS0 [Feferman’87]

• Inductive type theory / ALF [Coquand, Magnusson, Nordström’91]

• Partial inductive definitions/Pi [Hallnäs’87] [Eriksson’93]

• Labelled deductive systems [Gabbay’89]

• Substructural frameworks [Schroeder-Heister’91] [Girard’93] [Miller’94]

• Equational frameworks [Martì-Oliet & Meseguer’93] [C. Kirchner, H. Kirchner & Vittek’93]

Brief History, III

General systems for constructive mathematics have also been used as logical frameworks. For example:

• NQTHM (Boyer-Moore) [Shankar’86]

• Otter (Lusk-Overbeek) [Wos’88]

• Nuprl (Constable et al.)

[Basin & Constable’91]

• Coq (Huet et al.) [Huet’93]

• LEGO [Pollack’93]

Frameworks as Conceptual Tool

Logical frameworks, their concepts and methods can be an aid to understanding, rather than just an implementation and checking device.

• Polymorphic type reconstruction [Pf’88]

• Canonical forms and uniform derivations [Pf’92]

• Properties of CPS [Danvy & Pf’93]

• Structural cut-elimination [Pf’94]

• Inductive residual theory [Huet’93]

• IsaWhelk [Basin’93]

• (Computation & Deduction course [Pf’92,Pf’94])

• …

Framework Design Goals

• Simple and uniform, concise

• Close to (good) informal practice

• Efficiently implementable

• Support for search and meta-programming

• Decide validity of derivations

• Feasibility of proving correctness of representations • Means for structuring large specifications

Outline

Example: first-order predicate logic • Abstract syntax

• Inference rules and derivations • Search and meta-programming • Meta-theory

FOL, Abstract Syntax

Variables x_{n}
Terms  t ::= x | f^{k}(t_{1}, …, t_{n})
Atoms  P ::= p^{k}(t_{1}, …, t_{n})
Formulas A ::= P | A_{1}A_{2} | ¬A | ∀x.A