HOAS on top of FOAS formalized in Isabelle/HOL

Permalink

https://hdl.handle.net/2142/15449

Title: HOAS on top of FOAS formalized in Isabelle/HOL
Author(s): Popescu, Andrei
Contributor(s): Gunter, Elsa L.
Issue Date: 2010
Keyword(s): Higher-Order Abstract Syntax, Isabelle/HOL
Abstract: "This collection of documents presents the Isabelle formalization of Higher-Order Abstract Syntax (HOAS) as a definitional layer on top of First-Order Abstract Syntax (FOAS). The formal scripts shown here are provided as a technical companion to the paper ""HOAS on top of FOAS"" to be presented at LICS 2010 (and to its more detailed technical report version). They work with Isabelle2009-1. The scripts are currently under (intensive!) development. To obtain the latest version of the theory, please contact the author at uuomul@yahoo.com."
Type of Resource: other
Language: en
Permalink: http://hdl.handle.net/2142/15449