log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
POPLMark Reloaded: Mechanizing Proofs by Logical Relations
Zoom
Tuesday, October 13, 2020, 4:15-5:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

We propose a new collection of challenge problems in mechanizing metatheory of programming languages for comparing and pushing the state of the art of proof assistants. In particular, we focus on proofs using logical relations and propose establishing strong normalization of a simply-typed lambda-calculus with a proof by Kripke-style logical relations as a benchmark. We give a modern view of this well-understood problem by formulating our logical relation on well-typed terms. Using this case study, we share some of the lessons learned tackling this challenge 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. We hope others will be motivated to submit solutions! 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.

Come join us via Zoom: https://umd.zoom.us/j/98723227318?pwd=K0RJZVZZM1Jhd2laMlg1ajgvUjltQT09

This talk is organized by Ian Sweet