Locally Nameless at Scale. Stephanie Weirich, A. V. In The Fourth International Workshop on Coq for Programming Languages, pages 3, January, 2018. Citation Key Alias: weirich, weirich2018
abstract   bibtex   
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.
@inproceedings{coqpl18,
	title = {Locally {Nameless} at {Scale}},
	abstract = {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.},
	language = {en},
	booktitle = {The {Fourth} {International} {Workshop} on {Coq} for {Programming} {Languages}},
	author = {Stephanie Weirich, Antoine Voizard, Anastasiya Kravchuk-Kirilyuk},
	month = jan,
	year = {2018},
	note = {Citation Key Alias: weirich, weirich2018},
	pages = {3}
}

Downloads: 0