Go backward to Type Attributes of Type Structures
Go up to Top
Go forward to Semantics of Type Structures II

Semantics of Type Structures I

Program
- [[D in C: comm]] $s$ = [[ $P$ ₁ |- C: comm]] $e$ ₁ $s$ ,
  where ( $e$ ₁, $s$ ₁) = [[{} |- D: $P$ ₁dec]]{} $s$
Declaration
- [[ $P$ |- define I=U: {I: $H$ }dec]] $e$ $s$ = ({I= $f$ }, $s$ )
  where $f$ $s'$ = [[ $P$ |- U: $H$ ]] $e$ $s'$ and U in{E, T, C}
- [[ $P$ |- D₁;D₂: ( $P$ ₁ U $P$ ₂)dec]] $e$ $s$ =
      ( $e$ ₁ union $e$ ₂, $s$ ₂) where
      ( $e$ ₁, $s$ ₁) = [[ $P$ |- D₁: $P$ ₁dec]] $e$ $s$
      ( $e$ ₂, $s$ ₂) = [[ $P$ U $P$ ₁ |- D₂: $P$ ₂dec]] ( $e$ union $e$ ₁) $s$ ₁
- [[ $P$ |-var I:T: {I: $D$ }dec]] $e$ $s$ = ({I= $v$ }, $s'$ )
  where ( $v$ , $s'$ ) = [[ $P$ |- T: $D$ class]] $e$ $s$

Id: abstraction2.tex,v 1.1 1996/04/10 07:30:13 schreine Exp schreine