Normalization of IZF with Replacement
ZF is a well investigated impredicative constructive version of Zermelo-Fraenkel set theory. Using set terms, we axiomatize IZF with Replacement, which we call \izfr, along with its intensional counterpart \iizfr. We define a typed lambda calculus $\li$ corresponding to proofs in \iizfr according to...
| מחבר ראשי: | |
|---|---|
| פורמט: | Article |
| שפה: | English |
| יצא לאור: |
Logical Methods in Computer Science e.V.
2008-04-01
|
| סדרה: | Logical Methods in Computer Science |
| נושאים: | |
| גישה מקוונת: | https://lmcs.episciences.org/1235/pdf |