HOAS on top of FOAS formalized in Isabelle/HOL
Andrei Popescu · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2010
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 [email protected].