Richard Zach on Nostr: Tait's two most well-known contributions are perhaps the development of the ...
Tait's two most well-known contributions are perhaps the development of the Schütte-Tait method of proving cut elimination (Tait 1968) and the method of proving normalization for lambda calculus using Tait computability predicates (Tait 1967). He is also sometimes credited with the observation that the Curry–Howard correspondence between formulas and types and proofs and lambda terms extends to normalization of natural deduction and reduction of the corresponding lambda term.
Published at
2024-03-24 22:44:27Event JSON
{
"id": "ce434501a997c91b1872741b7765961af1f034e45cd5987c7bc3d64e7a88fe7b",
"pubkey": "580ba9c3849e80d58cbcd2c76728f33468f41c54396d73656137b224781f45d2",
"created_at": 1711320267,
"kind": 1,
"tags": [
[
"e",
"6ecf6274707acd9389e5abc6077a41a5356746ddf62877e48c98f56d1c71a378",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/rrrichardzach/statuses/112153085066884653",
"activitypub"
]
],
"content": "Tait's two most well-known contributions are perhaps the development of the Schütte-Tait method of proving cut elimination (Tait 1968) and the method of proving normalization for lambda calculus using Tait computability predicates (Tait 1967). He is also sometimes credited with the observation that the Curry–Howard correspondence between formulas and types and proofs and lambda terms extends to normalization of natural deduction and reduction of the corresponding lambda term.",
"sig": "c3b22f4038b7c0a9d8fbd6956d19e8b78ceae150621e483e89a1a0cbacd5eb57595801ef29837b4e9bae442e5c5b084cead2ea4abedfa719d4e4ec5f68c96458"
}
