Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory

DOI10.1145/3209108.3209119MaRDI QIDQ5145355zbMATH OpenOpenAlexFDO

Authors Andreas Nuyts, Dominique Devriese

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3209108.3209119

zbMATH Keywords

algebra in type theorycubical type theoryerasureintersectionsirrelevanceparametricitypresheaf semanticsunions

Mathematics Subject Classification ID

Type theory (03B38) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20)

Recommendations

• A relationally parametric model of dependent type theory
• Proofs for free. Parametricity for dependent types
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• Parametricity and dependent types
• Formal parametric polymorphism

Cited in

(16)

• Graded modal dependent type theory
• Irrelevance in type theory with a heterogeneous equality judgement
• Internal parametricity for cubical type theory
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• Dual-context calculi for modal logic
• Multimodal dependent type theory
• An extension of Möbius-Lie geometry with conformal ensembles of cycles and its implementation in a GiNaC library
• A relationally parametric model of dependent type theory
• Irrelevance, heterogeneous equality, and call-by-value dependent type systems
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• \(\eta\)-equivalence in core dependent Haskell
• A dependent dependency calculus
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Transpension: the right adjoint to the Pi-type
• A sound and complete substitution algorithm for multimode type theory
• Unifying cubical and multimodal type theory

This page was built for publication: Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory

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