Files in this item



application/ (3MB)
zip-archived collection of documentsZIP


Title:HOAS on top of FOAS formalized in Isabelle/HOL
Author(s):Popescu, Andrei
Contributor(s):Gunter, Elsa L.
Subject(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
Issue Date:2010
Genre:Technical Report
Publication Status:unpublished
Date Available in IDEALS:2010-04-30

This item appears in the following Collection(s)

Item Statistics