scientific article; zbMATH DE number 7204444

DOI10.4230/LIPICS.FSCD.2017.25MaRDI QIDQ5111322zbMATH OpenFDO

Authors Daniel R. Licata, Michael Shulman, Mitchell Riley

Publication date 26 May 2020

zbMATH Keywords

substructural logicmodal logictype theoryhomotopy type theory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05) Categorical logic, topoi (03G30) Type theory (03B38)

Recommendations

• A uniform framework for substructural logics with modalities
• Multiplicative linear logics and fibrations
• Higher-order representation of substructural logics
• Fibring of logics as a categorial construction
• A categorical semantics for linear logical frameworks

Cites work

• scientific article; zbMATH DE number 517072 (Why is no real title available?)
• scientific article; zbMATH DE number 2079022 (Why is no real title available?)
• scientific article; zbMATH DE number 2152035 (Why is no real title available?)
• scientific article; zbMATH DE number 1907195 (Why is no real title available?)
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine
• A judgmental reconstruction of modal logic
• A linear logical framework
• Adjoint logic with a 2-category of modes
• Automata, Languages and Programming
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Display logic
• Fibered Multiderivators and (co)homological descent
• Functors are type refinement systems
• Higher-order representation of substructural logics
• Homotopy type theory. Univalent foundations of mathematics
• Hybridizing a logical framework
• I got plenty o' nuttin'
• On an intuitionistic modal logic
• Quantum gauge field theory in cohesive homotopy type theory
• The Logic of Bunched Implications
• The Mathematics of Sentence Structure
• Type theory in type theory using quotient inductive types
• Types for Proofs and Programs

Cited in

(28)

• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• A fresh view of linear logic as a logical framework
• An algebraic approach to subframe logics. Modal case
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• A linear logic framework for multimodal logics
• A fibrational tale of operational logical relations: pure, effectful and differential
• LNL polycategories and doctrines of linear logic
• A framework for substructural type systems
• Higher-order representation of substructural logics
• scientific article; zbMATH DE number 5917724 (Why is no real title available?)
• scientific article; zbMATH DE number 500952 (Why is no real title available?)
• A general framework for the semantics of type theory
• A fibrational framework for possible-world semantics of \textsc{Algol}-like languages
• Bifibrations of polycategories and classical linear logic
• UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
• Multiplicative linear logics and fibrations
• Adjoint logic with a 2-category of modes
• A message-passing interpretation of adjoint logic
• scientific article; zbMATH DE number 868086 (Why is no real title available?)
• scientific article; zbMATH DE number 1931660 (Why is no real title available?)
• Normalization for multimodal type theory
• A linear algebra approach to linear metatheory
• Modal dependent type theory and dependent right adjoints
• scientific article; zbMATH DE number 6917935 (Why is no real title available?)
• Back to futures
• Modal crash types for intermittent computing
• Multimodal dependent type theory
• A uniform framework for substructural logics with modalities

This page was built for publication:

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