Locally Nameless at Scale
The Corespec project is an extensive mechanization in Coq of the metatheory of System D and System DC, two related, dependently-typed languages aimed at replacing the GHC’s internal language, Core. In this talk, we take a retrospective look at our development through the lens of a recent addition, eta-equivalence. In particular, we describe our experience with the practical application of locally nameless variable-binding representation for mechanized metatheory, supported by the Ott and LNgen tools.
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
14:00 - 14:50
|Locally Nameless at Scale|
Stephanie Weirich University of Pennsylvania, USA, Antoine Voizard University of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of PennsylvaniaFile Attached
|A Coq Formalisation of a Core of R|
Martin Bodin CMMFile Attached