A theory of effects and resources: adjunction models and polarised calculi

DOI10.1145/2837614.2837652MaRDI QIDQ2828243zbMATH OpenOpenAlexFDO

Authors Pierre-Louis Curien, Guillaume Munch-Maccagnoni, Marcelo P. Fiore

Publication date 24 October 2016

Published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

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

zbMATH Keywords

adjunction modelscategorical semanticscomputational effectsCurry-Howard-Lambek correspondenceintuitionistic logiclinear logicpolarised calculiresource modalities

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical semantics of formal languages (18C50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• The enriched effect calculus: syntax and semantics
• Enriching an Effect Calculus with Linear Types
• Adjunction models for call-by-push-value with stacks
• scientific article; zbMATH DE number 2172969
• The costructure–cosemantics adjunction for comodels for computational effects

Cited in

(13)

• Graded algebraic theories
• Call-By-Push-Value from a Linear Logic Point of View
• Back to futures
• Dual-context calculi for modal logic
• Models of Linear Logic based on the Schwartz \varepsilon-product
• Models of a non-associative composition
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Towards logical foundations for probabilistic computation
• Curry and Howard meet Borel
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Two-dimensional Kripke semantics. II: Stability and completeness
• Adjoint natural deduction
• Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads

This page was built for publication: A theory of effects and resources: adjunction models and polarised calculi

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