Sharing proofs with predicative theories through universe-polymorphic elaboration
From MaRDI portal
Publication:6635505
DOI10.46298/LMCS-20(3:23)2024MaRDI QIDQ6635505
Thiago Felicissimo, Frédéric Blanqui
Publication date: 12 November 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
type theoryAgdapredicativityproof translationimpredicativityDeduktiuniverse polymorphismunification for universe levelsuniverse-polymorphic elaboration
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Unification in commutative idempotent monoids
- Higher-order rewrite systems and their confluence
- Type checking with universes
- Combinatory reduction systems: Introduction and survey
- Setoid type theory -- a syntactic translation
- Proof-checking Euclid
- Universe Polymorphism in Coq
- Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Definitions by rewriting in the Calculus of Constructions
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- A modular construction of type theories
- Encoding type universes without using matching modulo associativity and commutativity
- Adequate and computational encodings in the logical framework Dedukti
- Translating proofs from an impredicative type system to a predicative one
- Type theory with explicit universe polymorphism
This page was built for publication: Sharing proofs with predicative theories through universe-polymorphic elaboration
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6635505)
