Module Layers

-------------------------------------------------------------------------

We distinguish two layers, the physical layer and the logical layer. Values or terms that inhabit the logical layer are erased.

We do not wish to rigidly stratify the syntax of values and terms in two layers, as this would lead us to duplicating many constructs. Instead, we duplicate only one construct: pairs. A pair carries two annotations, which indicate which layer each component inhabits. This gives rise to four pair constructs: physical/physical, logical/physical, physical/logical, and logical/logical. As far as type-checking is concerned, these four constructs behave analogously; the layer annotations are reflected in the types. The layer annotations are effectively taken into account in the definition of erasure, where physical/physical pairs become pairs, mixed pairs are mapped to their single physical component, and logical pairs are erased. They are also taken into account in the definition of well-layeredness. Annotating pairs with layers allows us to define erasure without requiring any type information, and to keep the definitions of well-typedness and well-layeredness separate.

tex: layers

A pair has some physical existence if at least one of its component is physical. This is reflected in the following definition.

This tactic performs case analysis on the layer variables found in the context.

Basic lemmas.