Call-By-Push-Value from a Linear Logic Point of View
DOI10.1007/978-3-662-49498-1_9zbMATH Open1335.03064OpenAlexW2486165584MaRDI QIDQ2802478FDOQ2802478
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
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
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)
Cites Work
- Linear logic
- Title not available (Why is that?)
- Locus solum: From the rules of logic to the logic of rules.
- Control categories and duality: On the categorical semantics of the lambda-mu calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- A new constructive logic: classic logic
- Logic Programming with Focusing Proofs in Linear Logic
- Title not available (Why is that?)
- Probabilistic coherence spaces as a model of higher-order probabilistic computation
- The duality of computation
- The Scott model of linear logic is the extensional collapse of its relational model
- Title not available (Why is that?)
- Probabilistic coherence spaces are fully abstract for probabilistic PCF
- Title not available (Why is that?)
- Adjunction models for call-by-push-value with stacks
- Call-by-name, call-by-value, call-by-need and the linear lambda calculus
- A Semantical and Operational Account of Call-by-Value Solvability
- A general storage theorem for integers in call-by-name \(\lambda\)- calculus
- The duality of computation under focus
- A theory of effects and resources: adjunction models and polarised calculi
- 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)
