|
How formulae became type| old_uid | 17181 |
|---|
| title | How formulae became type |
|---|
| start_date | 2019/01/30 |
|---|
| schedule | 18h-20h |
|---|
| online | no |
|---|
| summary | The Curry-Howard correspondence between constructive logical formulae and types for lambda-terms has a prehistory, a history and some promises of a future life. I will summarize the history of this correspondence focussing on some lesser known contributions, mostly from areas outside proof-theory, leading to a reappraisal of the Heyting-Kolmogorov interpretation of the intuitionistic logical constants. |
|---|
| responsibles | Joinet |
|---|
| |
|