Call-By-Push-Value from a Linear Logic Point of View

DOI10.1007/978-3-662-49498-1_9zbMath1335.03064OpenAlexW2486165584MaRDI QIDQ2802478

Thomas Ehrhard

Publication date: 26 April 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-49498-1_9

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40) Eilenberg-Moore and Kleisli constructions for monads (18C20)

Related Items

Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus, Unnamed Item, Factorization in call-by-name and call-by-value calculi via linear logic, The bang calculus revisited, The bang calculus revisited, Unnamed Item

Cites Work

• The Scott model of linear logic is the extensional collapse of its relational model
• Probabilistic coherence spaces as a model of higher-order probabilistic computation
• Linear logic
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• Locus Solum: From the rules of logic to the logic of rules
• A theory of effects and resources: adjunction models and polarised calculi
• Adjunction Models For Call-By-Push-Value With Stacks
• The enriched effect calculus: syntax and semantics
• The duality of computation
• The Duality of Computation under Focus
• A new constructive logic: classic logic
• Logic Programming with Focusing Proofs in Linear Logic
• Probabilistic coherence spaces are fully abstract for probabilistic PCF
• A Semantical and Operational Account of Call-by-Value Solvability
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item