[TYPES/announce] JFP paper: POPLMark reloaded: Mechanizing proofs by logical relations

[Brigitte Pientka]

Dear all,

we would like to announce our recent JFP paper

POPLMark reloaded: Mechanizing proofs by logical relations
Andreas Abel, Guillame Allais, Aliya Hameer, Alberto Momigliano, Brigitte Pientka, Steven Schaefer, Kathrin Stark, Journal of Functional Programming, 29, E19. doi:10.1017/S0956796819000170

on how to mechanize proofs using logical relations on well-typed terms. It is an expanded version of B. Pientka's invited talk at Certified Proofs and Programs (CPP'19): POPLMark reloaded: Mechanizing proofs by logical relations.

Specifically, this paper provides a modern tutorial to proving strong normalization of a simply-typed lambda-calculus with a proof by  Kripke-style logical relations. 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 provide one benchmark to better understand, compare and push the state of the art of proof assistants and to engage the community in discussions on what support in proof environments is  needed to provide better support for modelling variable binding, contexts, renamings, substitutions, etc. 
 
We hope that other developers of proof assistants, graduate students, researchers, etc. feel inspired to mechanize this challenge problem, so we can better learn about the trade-offs between different systems/mechanization approaches.

All solutions to the problem (including solutions in F* and Lean) can be found at

https://poplmark-reloaded.github.io/


Best,

Andreas Abel,
Guillame Allais,
Aliya Hameer,
Alberto Momigliano,
Brigitte Pientka,
Steven Schäfer,
Kathrin Stark