Functor Categories and Two-Level Languages

10 years 10 months ago
Functor Categories and Two-Level Languages
Abstract. We propose a denotational semantics for the two-level language of [GJ91, Gom92], and prove its correctness w.r.t. a standard denotational semantics. Other researchers (see [Gom91, GJ91, Gom92, JGS93, HM94]) have claimed correctness for lambda-mix (or extensions of it) based on denotational models, but the proofs of such claims rely on imprecise definitions and are basically flawed. At a technical level there are two important differences between our model and more naive models in Cpo: the domain for interpreting dynamic expressions is more abstract (we interpret code as -terms modulo -conversion), the semantics of newname is handled differently (we exploit functor categories). The key idea is to interpret a two-level language in a suitable functor category CpoDop rather than Cpo. The semantics of newname follows the ideas pioneered by Oles and Reynolds for modeling the stack discipline of Algol-like languages. Indeed, we can think of the objects of D (i.e. the natural numbers...
Eugenio Moggi
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Authors Eugenio Moggi
Comments (0)