@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}
}

{"_id":"3vnvjakSbAKK6tryP","bibbaseid":"stephanieweirich-locallynamelessatscale-2018","authorIDs":[],"author_short":["Stephanie Weirich, A. V."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","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":[{"propositions":[],"lastnames":["Stephanie","Weirich"],"firstnames":["Antoine","Voizard"],"suffixes":[]}],"month":"January","year":"2018","note":"Citation Key Alias: weirich, weirich2018","pages":"3","bibtex":"@inproceedings{coqpl18,\n\ttitle = {Locally {Nameless} at {Scale}},\n\tabstract = {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.},\n\tlanguage = {en},\n\tbooktitle = {The {Fourth} {International} {Workshop} on {Coq} for {Programming} {Languages}},\n\tauthor = {Stephanie Weirich, Antoine Voizard, Anastasiya Kravchuk-Kirilyuk},\n\tmonth = jan,\n\tyear = {2018},\n\tnote = {Citation Key Alias: weirich, weirich2018},\n\tpages = {3}\n}\n\n","author_short":["Stephanie Weirich, A. V."],"key":"coqpl18","id":"coqpl18","bibbaseid":"stephanieweirich-locallynamelessatscale-2018","role":"author","urls":{},"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.715Z","downloads":0,"keywords":[],"search_terms":["locally","nameless","scale","stephanie weirich"],"title":"Locally Nameless at Scale","year":2018,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}