Modalities and Parametric Adjoints

DOI10.1145/3514241zbMath1505.03030OpenAlexW4220778823MaRDI QIDQ5072609

Daniel Gratzer, G. A. Kavvos, Evan Cavallo, Adrien Guatto, Lars Birkedal

Publication date: 29 April 2022

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

dependent typescategorical semanticsparametricityguarded recursionFitch-style modalitiesmodal types

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (3)

When programs have to watch paint dry ⋮ Strange new universes: Proof assistants and synthetic foundations ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC

This page was built for publication: Modalities and Parametric Adjoints