Encoding type universes without using matching modulo associativity and commutativity

DOI10.4230/LIPICS.FSCD.2022.24zbMATH Open1541.68171MaRDI QIDQ6544119

Frédéric Blanqui

Publication date: 27 May 2024

zbMATH Keywords

rewritingtype theorylogical frameworktype universes

Mathematics Subject Classification ID

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

Related Items (1)

Sharing proofs with predicative theories through universe-polymorphic elaboration

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)