Go backward to 1. Version Go up to Top

2. Version

Family of procedure domains:

Nat-proc = Nat -> Store -> Poststore_{_|_}
Array-proc = Array -> Store -> Poststore_{_|_}
Record-proc = Proc -> Store -> Poststore_{_|_}

Type-tag =
    Nat-tag + Array-tag + Record-tag + Err-tag
    where Nat-tag = ...= Unit
T': Type-structure -> Environment -> Type-tag

D[[proc I₁(I₂:T) = C]] = lambda e. lambda s.
    cases (T'[[T]]e) of
        isNat-tag() ->
            ((updateenv [[I₁]] inNat-proc(lambda n.
                C[[C]](updateenv [[I₂]]
                    inNat(n) e)) e),
            (return s))
        isArray-tag() -> ...
        isRecord-tag() -> ...
        isErr-tag() -> (e, (signalerr s))
    end