Translating proofs from an impredicative type system to a predicative one (Q6610621)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Translating proofs from an impredicative type system to a predicative one |
scientific article; zbMATH DE number 7918698
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Translating proofs from an impredicative type system to a predicative one |
scientific article; zbMATH DE number 7918698 |
Statements
Translating proofs from an impredicative type system to a predicative one (English)
0 references
25 September 2024
0 references
type theory
0 references
impredicativity
0 references
predicativity
0 references
proof translation
0 references
universe polymorphism
0 references
unification modulo max
0 references
Agda
0 references
dedukti
0 references
