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

DOI10.1145/2837614.2837652zbMATH Open1347.68078OpenAlexW2267766518MaRDI QIDQ2828243FDOQ2828243

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

categorical semanticsintuitionistic logiclinear logiccomputational effectsresource modalitiesadjunction modelsCurry-Howard-Lambek correspondencepolarised calculi

Mathematics Subject Classification ID

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

• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Towards logical foundations for probabilistic computation
• Title not available (Why is no real title available?)
• Graded algebraic theories
• Curry and Howard meet Borel
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Call-By-Push-Value from a Linear Logic Point of View
• Back to futures
• Models of a non-associative composition
• Models of Linear Logic based on the Schwartz $\varepsilon$-product

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)