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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

14:00 - 14:50: - PL Metatheory at Watercourt A
Chair(s): Steve ZdancewicUniversity of Pennsylvania
CoqPL-201814:00 - 14:25
Stephanie WeirichUniversity of Pennsylvania, USA, Antoine VoizardUniversity of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of Pennsylvania
File Attached
CoqPL-201814:25 - 14:50
File Attached