Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma

被引：0

作者：

Saffrich, Hannes ^{[1
]}

Thiemann, Peter ^{[1
]}

Weidner, Marius ^{[1
]}

机构：

[1] Univ Freiburg, Freiburg, Germany

来源：

PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON TYPE-DRIVEN DEVELOPMENT, TYDE 2024 | 2024年

关键词：

mechanized metatheory; finitely-stratified System F; denotational semantics; operational semantics; Agda;

D O I：

10.1145/3678000.3678201

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Intrinsically typed syntax is an important and popular method for mechanized reasoning about programming languages. We explore the limits of this method in the setting of finitely-stratified System F using the Agda proof assistant. This system supports elegant definitions of denotational semantics as well as big-step operational semantics based on intrinsically typed syntax. While its syntactic metatheory (i.e., type soundness) works well, we demonstrate that its semantic metatheory poses technical challenges, by defining a logical relation and proving its fundamental lemma. Our logical relation connects a denotational semantics with an operational one, which exposes issues with transfer lemmas as well as minor issues with universe polymorphism.

引用

页码：2 / 15

页数：14