Denotational Semantics
- Type attributes become values in the semantics.
-
[[pi |- module I1(I2:Type-structure) =
D:{I1:Deltaclass
-> theta(Delta)}dec]]e s
=({I1=m}, s)
where m(deltaclass) v s'
= [[pi -U- {I2:deltaclass} |- D:
theta(delta)]](e -U- {I2=v})s'
-
[[pi |- import I(T):theta(delta)]]e s
= m(deltaclass)([[pi |- T: deltaclass]]e)s
where (I=m) in e
- m in deltaclass -> [[deltaclass]]
-> Store
-> ([[theta(delta)]] x Store)
- Argument structure depends on m's first argument!
- Dependent types
Serious questions about soundness open.
Author: Wolfgang Schreiner
Last Modification: May 7, 1998