Sharing proofs with predicative theories through universe-polymorphic elaboration (Q6635505)
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: Sharing proofs with predicative theories through universe-polymorphic elaboration |
scientific article; zbMATH DE number 7941267
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Sharing proofs with predicative theories through universe-polymorphic elaboration |
scientific article; zbMATH DE number 7941267 |
Statements
Sharing proofs with predicative theories through universe-polymorphic elaboration (English)
0 references
12 November 2024
0 references
type theory
0 references
impredicativity
0 references
predicativity
0 references
proof translation
0 references
universe polymorphism
0 references
universe-polymorphic elaboration
0 references
unification for universe levels
0 references
Agda
0 references
Dedukti
0 references
