Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2018 / Oberseminar / Brigitte Pientka: "POPLMark Reloaded: Mechanizing Logical Relations Proofs"


Inhaltsbereich

Brigitte Pientka: "POPLMark Reloaded: Mechanizing Logical Relations Proofs"

Oberseminar, Freitag, 27.04.2018, 14 Uhr c.t.
Wann 14:15 15:15 27.04.2018
von bis
Wo L109
Termin übernehmen vCal
iCal

Brigitte Pientka

POPLMark Reloaded: Mechanizing Logical Relations Proofs

Abstract:
Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. Over the past decade, the POPLMark challenge popularized the use of proof assistants in mechanizing the metatheory of programming languages. Focusing on the the meta-theory of System F<, it allowed the programming languages community to survey existing techniques to represent and reason about syntactic structures with binders and promote the use of proof assistants. Today, mechanizing proofs is a stable fixture in the daily life of programming languages researchers.

As a follow-up to the POPLMark Challenge, we propose a new collection of benchmarks that use proofs by logical relations. Such proofs are now used to attack problems in the theory of complex languages models, with applications to issues in equivalence of programs, compiler correctness, representation independence and even more intensional properties such as non-interference, differential privacy and secure multi-language inter-operability. Yet, they remain challenging to mechanize.

In this talk, we focus on one particular challenge problem, namely strong normalization of a simply-typed lambda-calculus with a proof by Kripke-style logical relations. We will advocate a modern view of this well-understood problem by formulating our logical relation on well-typed terms. Using this case study, we share some of the lessons learned tackling this challenge problem in Beluga, a proof environment that supports higher-order abstract syntax encodings, first-class context and first-class substitutions. We also discuss and highlight similarities, strategies, and limitations in other proof assistants when tackling this challenge problem.

We hope others will be motivated to submit solutions! The goal of this talk is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses.

This is joint work with A. Abel (Chalmers), G. Allais (Radboud University), A. Hameer (McGill University), A. Momigliano (Univ. Milan), S. Schäfer (Univ. Saarbrücken), K. Stark (Univ. Saarbrücken)

Artikelaktionen


Funktionsleiste