Modalities and Parametric Adjoints

DOI10.1145/3514241MaRDI QIDQ5072609zbMATHOpenAlexFDO

Authors Daniel Gratzer, Evan Cavallo, G. A. Kavvos, 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

categorical semanticsdependent typesparametricityguarded 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)

Recommendations

• Modes of adjointness
• On monotone modalities and adjointness
• scientific article; zbMATH DE number 67510
• Adjoining adjoints
• scientific article; zbMATH DE number 2165869
• Adjoints, multi-adjoints, pluri-adjoints
• Adjoint action and its generalizations
• Modality, quantification, and many Vlach-operators
• Adjoint multidimensional acausal systems
• scientific article; zbMATH DE number 1286232

Cited in

(11)

• When programs have to watch paint dry
• scientific article; zbMATH DE number 67510 (Why is no real title available?)
• Modal dependent type theory and dependent right adjoints
• Normalization for multimodal type theory
• Multimodal dependent type theory
• Transpension: the right adjoint to the Pi-type
• Multimodal dependent type theory
• Fibrational modal type theory
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Strange new universes: Proof assistants and synthetic foundations
• Origins of parameters in adimensional models

This page was built for publication: Modalities and Parametric Adjoints

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