Realizability algebras: a program to well order R
The theory of classical realizability is a framework in which we can develop the proof-program correspondence. Using this framework, we show how to transform into programs the proofs in classical analysis with dependent choice and the existence of a well ordering of the real line. The principal tool...
Furkejuvvon:
| Váldodahkki: | |
|---|---|
| Materiálatiipa: | Artigo |
| Giella: | Inglês |
| Almmustuhtton: |
Logical Methods in Computer Science e.V.
2011-08-01
|
| Ráidu: | Logical Methods in Computer Science |
| Fáttát: | |
| Liŋkkat: | https://lmcs.episciences.org/1070/pdf |
| Fáddágilkorat: |
Eai fáddágilkorat, Lasit vuosttaš fáddágilkora!
|