Skip to content
Snippets Groups Projects
Select Git revision
  • master default
1 result
Compare
Name Last commit Last update
..
sources
README.md
guide.pdf
slides.pdf
README.md

N. Roux: “A Beginner's Guide to Logical Relations for a Logical Framework”

Based on “Logical Relations for a Logical Framework” (ACM Transactions on Computational Logic (2013)) by Rabe and Sojakova, Navid Roux delivered a talk and wrote a guide on motivating, introducing, and representing logical relations in the MMT system.

  • Manuscript/Guide: ./guide.pdf (submitted 2021-03-22)

  • Talk: https://www.youtube.com/watch?v=0rS3ol_J9Wo (post-recorded)

    Meta data of the official, unrecorded talk:

    • Title: Logical Relations for a Logical Framework
    • Presenter: Navid Roux
    • Date: 2021-01-27 14:45 - 16:15 CET
    • Place: virtual in Zoom meeting

  • Slides: ./slides.pdf (submitted 2021-01-27)

LaTeX Sources are contained in ./sources. See ./sources/README.md for building.
(Note to core kwarc members: the sources are manually mirrored, hopefully consistently, at https://gl.kwarc.info/supervision/roux_navid/-/tree/master/msc-seminar/slides-and-report.)

Abstract

Logical relations are an established proof technique for deriving meta-level theorems of formal systems. For example, they have been used to prove strong normalization, type safety, and correctness of compiler optimizations in the setting of various type theories and lambda calculi. Theories of logical relations have been stated for a wide range of formal systems.

To formalize formal systems themselves, logical frameworks have been sucessfully used, particularly shining when specifying syntax and deduction (e.g. using judgements-as-types and higherorder abstract syntax). And module systems over logical frameworks allow to modularly identify, translate, and combine full hierarchies of formal systems.

How to represent logical relations in such systems is an ongoing research question. In “Logical Relations for a Logical Framework” (ACM Transactions on Computational Logic (2013)), Rabe and Sojakova present a theory of logical relations applicable in the setting of logical frameworks that, when instantiated for formal systems formalized therein, gives a reasonable notion of logical relations within those systems.

We provide a detailed exposition of a special case, accessible to everyone familiar with basics of formalizing in logical frameworks. Our exposition is embedded in a coherent narrative spanning from concretely motivating logical relations (by walking through a proof of strong normalization for the simply-typed lambda calculus) up to concretely modeling a corresponding language feature for the MMT module system over the Edinburgh Logical Framework. The mechanics of our derived language feature are novel and forgo the need of introducing any logical relation-specific language primitive.