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

DOI10.1145/3209108.3209119zbMATH Open1453.03005OpenAlexW2798299123MaRDI QIDQ5145355FDOQ5145355

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

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

zbMATH Keywords

erasureparametricityintersectionsunionsirrelevancecubical type theorypresheaf semanticsalgebra in type theory

Mathematics Subject Classification ID

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

Cited In (11)

• Transpension: the right adjoint to the Pi-type
• Title not available (Why is that?)
• Title not available (Why is that?)
• An extension of Mobius--Lie geometry with conformal ensembles of cycles and its implementation in a GiNaC library
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Title not available (Why is that?)
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• Title not available (Why is that?)
• Title not available (Why is that?)
• Irrelevance in type theory with a heterogeneous equality judgement
• A dependent dependency calculus

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)