Translating proofs from an impredicative type system to a predicative one

DOI10.4230/LIPICS.CSL.2023.19MaRDI QIDQ6610621

Frédéric Blanqui, Ashish Kumar Barnawal, Thiago Felicissimo

Publication date: 25 September 2024

zbMATH Keywords

type theoryAgdapredicativityproof translationimpredicativityuniverse polymorphismdeduktiunification modulo max

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (1)

Sharing proofs with predicative theories through universe-polymorphic elaboration

This page was built for publication: Translating proofs from an impredicative type system to a predicative one

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