To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

POPLMark reloaded: Mechan… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

POPLMark reloaded: Mechanizing proofs by logical relations

Journal article
Authors Andreas Abel
G. Allais
A. Hameer
B. Pientka
A. Momigliano
S. Schafer
K. Stark
Published in Journal of Functional Programming
Volume 29
ISSN 0956-7968
Publication year 2019
Published at Department of Computer Science and Engineering (GU)
Language en
Links dx.doi.org/10.1017/s095679681900017...
Keywords typed lambda-calculus, order abstract syntax, metatheory, framework, language, normalization, formalization, challenge, binders, power, Computer Science
Subject categories Computer and Information Science

Abstract

We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?