A Normalizing Intuitionistic Set Theory with Inaccessible Sets
We propose a set theory strong enough to interpret powerful type theories underlying proof assistants such as LEGO and also possibly Coq, which at the same time enables program extraction from its constructive proofs. For this purpose, we axiomatize an impredicative constructive version of Zermelo-F...
I tiakina i:
| Kaituhi matua: | |
|---|---|
| Hōputu: | Artigo |
| Reo: | Inglês |
| I whakaputaina: |
Logical Methods in Computer Science e.V.
2007-08-01
|
| Rangatū: | Logical Methods in Computer Science |
| Ngā marau: | |
| Urunga tuihono: | https://lmcs.episciences.org/837/pdf |
| Ngā Tūtohu: |
Kāore He Tūtohu, Me noho koe te mea tuatahi ki te tūtohu i tēnei pūkete!
|