Formal verification of the equivalence of system F and the pure type system L2

• Main Author: Kaiser, Jonas
• Other Authors: Smolka, Gert
• Format: Doctoral or Postdoctoral Thesis
• Language: English
• Published: Saarländische Universitäts- und Landesbibliothek 2019
• Subjects: ddc:004; ddc:510; pure type system; System F; de Bruijn syntax; higher-order abstract syntax; contextual reasoning; Lambda; Sog; Beluga; Beluga*
• Online Access: http://nbn-resolving.org/urn:nbn:de:bsz:291--ds-284251; https://doi.org/10.22028/D291-28425

We develop a formal proof of the equivalence of two different variants of System F. The first is close to the original presentation where expressions are separated into distinct syntactic classes of types and terms. The second, L2 (also written as λ2), is a particular pure type system (PTS) where the notions of types and terms, and the associated expressions are unified in a single syntactic class. The employed notion of equivalence is a bidirectional reduction of the respective typing relations. A machine-verified proof of this result turns out to be surprisingly intricate, since the two variants noticeably differ in their expression languages, their type systems and the binding of local variables. Most of this work is executed in the Coq theorem prover and encompasses a general development of the PTS metatheory, an equivalence result for a stratified and a PTS variant of the simply typed λ-calculus as well as the subsequent extension to the full equivalence result for System F. We utilise nameless de Bruijn syntax with parallel substitutions for the representation of variable binding and develop an extended notion of context morphism lemmas as a structured proof method for this setting. We also provide two developments of the equivalence result in the proof systems Abella and Beluga, where we rely on higher-order abstract syntax (HOAS). This allows us to compare the three proof systems, as well as HOAS and de Bruijn for the purpose of developing formal metatheory. Wir präsentieren einen maschinell verifizierten Beweis der Äquivalenz zweier Darstellungen des Lambda-Kalküls System F. Die erste unterscheidet syntaktisch zwischen Termen und Typen und entspricht somit der geläufigen Form. Die zweite, L2 bzw. λ2, ist ein sog. Pure Type System (PTS), bei welchem alle Ausdrücke in einer syntaktischen Klasse zusammen fallen. Unser Äquivalenzbegriff ist eine bidirektionale Reduktion der jeweiligen Typrelationen. Ein formaler Beweis dieser Eigenschaft ist aufgrund der Unterschiede der Ausdruckssprachen, der ...