[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
