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 Jan Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change
|14:00 - 14:25|
Stephanie WeirichUniversity of Pennsylvania, USA, Antoine VoizardUniversity of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of PennsylvaniaFile Attached
|14:25 - 14:50|
Martin BodinCMMFile Attached