A Categorical Semantics for Linear Logical Frameworks

DOI10.1007/978-3-662-46678-0_7zbMath1461.03014arXiv1501.05016OpenAlexW1923962694MaRDI QIDQ2948554

Matthijs Vákár

Publication date: 1 October 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1501.05016

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Type theory (03B38) Traced monoidal categories, compact closed categories, star-autonomous categories (18M10)

Related Items (7)

Linear Dependent Type Theory for Quantum Programming Languages ⋮ Games for Dependent Types ⋮ Game semantics for dependent types ⋮ A formal logic for formal category theory ⋮ A Classical Sequent Calculus with Dependent Types ⋮ Reverse AD at higher types: pure, principled and denotationally correct ⋮ Dependent Types and Fibred Computational Effects

This page was built for publication: A Categorical Semantics for Linear Logical Frameworks