Encoding type universes without using matching modulo associativity and commutativity

DOI10.4230/LIPICS.FSCD.2022.24MaRDI QIDQ6544119zbMATH OpenFDO

Authors Frédéric Blanqui

Publication date 27 May 2024

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2022.24

zbMATH Keywords

logical frameworkrewritingtype theorytype universes

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Recommendations

• A modular construction of type theories
• Pure patterns type systems
• Encoding modal logics in logical frameworks
• scientific article; zbMATH DE number 1088050
• Rewriting calculus with(out) types

Cited in

(4)

• Sharing proofs with predicative theories through universe-polymorphic elaboration
• Reconstruction of SMT proofs with Lambdapi
• Checking linear integer arithmetic proofs in Lambdapi
• Impredicativity, cumulativity and product covariance in the logical framework dedukti

This page was built for publication: Encoding type universes without using matching modulo associativity and commutativity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6544119)