1 of 18

Lecture 1: Course Overview

CM 500: Logical Frameworks

Tuesday, January 30, 2024

Chris Martens

2 of 18

Hi!

Who am I?

  • Chris Martens (https://hci.social/@chrisamaphone)
  • Assoc prof @ Northeastern, CS and Art+Design
  • Logic/type theory/PL person (logic programming, dependent types, substructural and modal logics)
  • Also, video games? (interactive narrative, procedural generation, NPC authoring tools, generative art)

3 of 18

What is this class?

An experiment!

  • 5 weeks long
  • No credit
  • No official affiliation
  • Just because I want to

Website: https://chrisamaphone.github.io/lf-class/

​

​

4 of 18

Format

  • Tuesdays = “lecture” (but interactive)
    • Assign exercises
  • Thursdays = discuss exercises assigned Tuesday

​

​

5 of 18

How you can help

  • Introduce yourself on Zulip
  • Proactively propose or request things (e.g.: new Zulip channels)
  • Ask questions; answer questions; come to Thursday sessions with stuff to say
  • Show up!

​

6 of 18

Lecture goal

  • Understand terms: object language, metalanguage, logical framework, deductive system, metatheory
  • See (in fast motion) how Twelf implements a logical framework and can be put to use for metatheory

7 of 18

What is a logical framework?

A [computational] theory for encoding other theories� (color convention: metalanguage, object language)

Encodings:

  • Representing objects of the theory (e.g. syntax, judgments, proofs)
  • Proofs as programs / objects with inspectable structure

Metatheory:

  • Proofs about the (object) theory
  • Proof checking
  • Proof search

8 of 18

Metatheory

Theory about the theor(y/ies)

Examples for PL:

  • Progress and preservation (“well-typed programs don’t go wrong”)
  • Two ways of saying something are equivalent
  • Translation from one language to another preserves a property
  • Normalization, termination, totality

Examples for logic:

  • Internal soundness/completeness (e.g. cut, identity)
  • Soundness/completeness (wrt another theory)

9 of 18

Twelf

http://twelf.org/

“Twelf is a language used to specify, implement, and prove properties of deductive systems such as programming languages and logics.”

10 of 18

Deductive Systems

Programming languages, logics

Formal specifications “on paper”

  • Inference rules, judgments, syntax

​

11 of 18

EXAMPLE: A first deductive system

  • Syntax: natural numbers
  • Judgments: even/odd

12 of 18

Mechanizing Definitions

“What does it mean to correctly represent [on-paper language definitions] in a formal framework?”

Representation is adequate iff isomorphic to said definition.

13 of 18

LF, Elf, Twelf

LF (“the Edinburgh Logical Framework”): Harper, Honsel, Plotkin. “A Framework for Defining Logics.”

Elf: logic programming language atop LF.

Twelf: metatheory checker for Elf.

14 of 18

Twelf Speedrun

(switch to editor)

15 of 18

Mechanizing Definitions

LF Signature:

  • LF types - Object-language syntax categories
  • LF type families - Object-language judgment forms (over syntax)
  • LF canonical forms - Object-language judgments and rules

16 of 18

Mechanizing Metatheory

LF Signature:

  • LF type families - OL theorem statements

​

Twelf concept:

  • Well-moded types (clauses) - OL proof cases
  • Total clause sets - OL proofs
    • Coverage checking
    • Termination checking

​

17 of 18

Course plan

  • Tuesday = “lecture”, Thursday = discussion of exercises
  • Schedule:
    • Week 1 (this week): Overview
    • Week 2: LF type theory
    • Week 3: Higher-order abstract syntax (encoding PLs with binders)
    • Week 4: Canonical Forms/Adequacy
    • Week 5: Participant demos?

​

18 of 18

Resources