Go backward to Generalization
Go up to Top
Go forward to The Correspondence Principle
Denotational Semantics
- Type attributes become values in the semantics.
-
[[pi |- module I(I:Type-structure) =
D:{I:Deltaclass
theta(Delta)}dec]]
=({I=}, )
where (deltaclass)
= [[pi -U- {I:deltaclass} |- D:
theta(delta)]]( -U- {I=})
-
[[pi |- import I(T):theta(delta)]]
= (deltaclass)([[pi |- T: deltaclass]])
where (I=) in
- in deltaclass [[deltaclass]]
Store
([[theta(delta)]] x Store)
- Argument structure depends on 's first argument!
- Dependent types
Serious questions about soundness open.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: parameter.tex,v 1.1 1996/04/25 11:40:48 schreine Exp schreine