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

DOI10.1007/978-3-662-49498-1_9MaRDI QIDQ2802478zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Call-by-value non-determinism in a linear logic type discipline
• Call-by-value in a basic logic for interaction
• scientific article; zbMATH DE number 2120508
• A formal equational theory for call-by-push-value
• Linearity in the non-deterministic call-by-value setting
• scientific article; zbMATH DE number 1086682
• Factorization in call-by-name and call-by-value calculi via linear logic
• Extended call-by-push-value: reasoning about effectful programs and evaluation order
• Call-by-value combinatory logic and the lambda-value calculus
• Linear dependent types in a call-by-value scenario

Cites work

• scientific article; zbMATH DE number 2185654 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 4103051 (Why is no real title available?)
• scientific article; zbMATH DE number 1303724 (Why is no real title available?)
• scientific article; zbMATH DE number 1942458 (Why is no real title available?)
• scientific article; zbMATH DE number 2120508 (Why is no real title available?)
• A Semantical and Operational Account of Call-by-Value Solvability
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• A new constructive logic: classic logic
• A theory of effects and resources: adjunction models and polarised calculi
• Adjunction models for call-by-push-value with stacks
• 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
• Linear logic
• Locus solum: From the rules of logic to the logic of rules.
• Logic Programming with Focusing Proofs in Linear Logic
• Probabilistic coherence spaces are fully abstract for probabilistic PCF
• Probabilistic coherence spaces as a model of higher-order probabilistic computation
• The Scott model of linear logic is the extensional collapse of its relational model
• The duality of computation
• The duality of computation under focus
• The enriched effect calculus: syntax and semantics

Cited in

(8)

• Operational properties of \texttt{Lily}, a polymorphic linear lambda calculus with recursion
• Call-by-value non-determinism in a linear logic type discipline
• Probabilistic call by push value
• Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus
• Factorization in call-by-name and call-by-value calculi via linear logic
• The bang calculus and the two Girard's translations
• The bang calculus revisited
• The bang calculus revisited

This page was built for publication: Call-By-Push-Value from a Linear Logic Point of View

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