Sat 13 Jan 2018 14:00 - 14:25 at Watercourt A - PL Metatheory Chair(s): Steve Zdancewic

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

CoqPL-2018
14:00 - 14:50: - PL Metatheory at Watercourt A
Chair(s): Steve Zdancewic
CoqPL-2018151584840000014:00 - 14:25
Talk
File Attached
CoqPL-2018151584990000014:25 - 14:50
Talk
File Attached