Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

POPLMark reloaded: Mechan… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

POPLMark reloaded: Mechanizing proofs by logical relations

Artikel i vetenskaplig tidskrift
Författare Andreas Abel
G. Allais
A. Hameer
B. Pientka
A. Momigliano
S. Schafer
K. Stark
Publicerad i Journal of Functional Programming
Volym 29
ISSN 0956-7968
Publiceringsår 2019
Publicerad vid Institutionen för data- och informationsteknik (GU)
Språk en
Länkar dx.doi.org/10.1017/s095679681900017...
Ämnesord typed lambda-calculus, order abstract syntax, metatheory, framework, language, normalization, formalization, challenge, binders, power, Computer Science
Ämneskategorier Data- och informationsvetenskap

Sammanfattning

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.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?