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: Tijuana, Baja California change

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