HOAS -- Higher Order Abstract Syntax: a Survey

I will introduce HOAS, and run a short survey over current work in the field. I will discuss several papers, listed below, describing problematic issues from the literature. I will also discuss the relationship between our current syntax mechanism and other HOAS work. The main problems of HOAS that will be discussed are "exotic" terms and induction. The referral relation between the papers I surveyed for this seminar is:
Semantical Analysis of Higher-Order Abstract Syntax Higher-Order Abstract Syntax in Coq Primitive Recursion for Higher-Order Abstract Syntax Furio Honsell and Marino Miculan Primitive Recursion for Higher-Order Abstract Syntax Higher-Order Abstract Syntax A Modal Analysis of Staged Computation Primitive recursion for higher-order abstract syntax with dependant types A Modal Lambda-Calculus with Iteration and Case Constructs Recursion for Higher-Order Encodings A Type-Theoretic Approach to Induction with Higher-Order Encodings Reflecting Higher-Order Abstract Syntax in Nuprl

bibtex entries are on a seperage page.