projects
/
lambda.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
add <a id=cps-reverse>
[lambda.git]
/
topics
/
_week5_system_F.mdwn
diff --git
a/topics/_week5_system_F.mdwn
b/topics/_week5_system_F.mdwn
index
684f42b
..
86f1c75
100644
(file)
--- a/
topics/_week5_system_F.mdwn
+++ b/
topics/_week5_system_F.mdwn
@@
-18,10
+18,10
@@
System F is due (independently) to Girard and Reynolds.
It enhances the simply-typed lambda calculus with quantification over
types. In System F, you can say things like
It enhances the simply-typed lambda calculus with quantification over
types. In System F, you can say things like
-<code>&
Gamm
a; α (\x.x):(α -> α)</code>
+<code>&
Lambd
a; α (\x.x):(α -> α)</code>
This says that the identity function maps arguments of type α to
This says that the identity function maps arguments of type α to
-results of type α, for any choice of α. So the &
Gamm
a; is
+results of type α, for any choice of α. So the &
Lambd
a; is
a universal quantifier over types.
a universal quantifier over types.