Go backward to The Semantics of Abstractions
Go up to Top
Go forward to Soundness of the Typing Rules
The Semantics of Abstractions
- Expression: [[E: Texp]] in Environment
-> Store -> [[T]]
- [[p |- N: intexp]]e s = [[p |- N:
int]]e
- [[p |- @L: intexp]]e s =
lookup([[p |-L: intloc]]e, s)
- [[p |- E_1+E_2: intexp]]e s =
plus(
[[p |- E_1: intexp]]e s, [[p
|- E_2: intexp]]e s)
- [[p |- E_1=E_2: boolexp]]e s =
equal(
[[p |- E_1: intexp]]e s, [[p
|- E_2: intexp]]e s)
- [[p |- not E: boolexp]]e s =
not([[p |- E: boolexp]]e s)
- [[p |- I: Texp]]e s, where (I=v) in e
- Location: [[L: intloc]] in Environment -> Location
- [[p |- loc_i: intloc]]e = loc_i
- Numeral: [[N: int]] in Environment -> Int
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: abstraction.tex,v 1.1 1996/03/05 08:55:21 schreine Exp schreine