BLEG: Curry-Howard equates (proposition, proof) to (type, function). What equates it to computation (state, trace)? Russell-Whitehead?
-
-
-
Replying to @mietek
Russell-Whitehead correspondance: propositions as states of your formal system, proofs as transition traces from one proposition to another.
1 reply 0 retweets 0 likes -
Replying to @Ngnghm
A proposition is a type; it can describe the shape of your state, but how would it describe the state itself?
2 replies 0 retweets 0 likes
Replying to @mietek
In Russell-Whitehead, a proposition is a state of the machine itself: a sequence of symbols denoting what has been deduced so far.
11:28 AM - 13 Apr 2017
0 replies
0 retweets
0 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
Read my blog!