Go backward to
Orthogonality
Go up to
Top
Go forward to
Categorical Product
Model of the Programming Language
Are our constructions of records and lambda abstractions the "right" ones?
Justification by category theory.
Categorical product
.
Categorical exponentiation
.
Definitions:
<E
1
, E
2
>:= (
fst
=
E
1
,
snd
=
E
2
)
e
V
1 :=
with
e
do
fst
e
V
2 :=
with
e
do
snd
(E
1
= E
2
) := [[
pi
|- E
1
:
theta
]]
e
= [[
pi
|- E
2
:
theta
]]
e
,
e
in
Env
pi
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998
