Adjoint logic with a 2-category of modes

DOI10.1007/978-3-319-27683-0_16MaRDI QIDQ5283430zbMATH OpenOpenAlexFDO

Authors Daniel R. Licata, Michael Shulman

Publication date 21 July 2017

Published in Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-27683-0_16

zbMATH Keywords

proof theorycategory theoryhomotopy type theoryadjoint logic

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) 2-categories, bicategories, double categories (18N10)

Recommendations

• scientific article; zbMATH DE number 7204444
• Modal dependent type theory and dependent right adjoints
• Modes of adjointness
• Modalities in homotopy type theory
• Homotopical categories of logics

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 2079022 (Why is no real title available?)
• scientific article; zbMATH DE number 195199 (Why is no real title available?)
• A cubical approach to synthetic homotopy theory
• A judgmental reconstruction of modal logic
• Axiomatic cohesion
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Eilenberg-MacLane spaces in homotopy type theory
• Logic Programming with Focusing Proofs in Linear Logic
• Notions of computation and monads
• Univalence for inverse diagrams and homotopy canonicity
• \(\pi _{n }(S ^{n })\) in homotopy type theory

Cited in

(8)

• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• A message-passing interpretation of adjoint logic
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Back to futures
• Modal crash types for intermittent computing
• Multimodal dependent type theory

This page was built for publication: Adjoint logic with a 2-category of modes

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