The bang calculus revisited

DOI10.1016/J.IC.2023.105047MaRDI QIDQ6116183zbMATH OpenOpenAlexFDO

Authors Antonio Bucciarelli, Delia Kesner, A. Ríos, Andrés Viso

Publication date 17 July 2023

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2023.105047

zbMATH Keywords

bang calculuscall-by-push-valueintersection types

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A semantic account of strong normalization in linear logic
• A semantic measure of the execution time in linear logic
• A Semantical and Operational Account of Call-by-Value Solvability
• A type assignment for -calculus complete both for FPTIME and strong normalization
• An equivalence between lambda- terms
• An extension of basic functionality theory for -calculus
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Call-By-Push-Value from a Linear Logic Point of View
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Call-by-value solvability, revisited
• Collapsing non-idempotent intersection types
• Computing connected proof(-structure)s from their Taylor expansion
• Consuming and persistent types for classical logic
• Execution time of λ-terms via denotational semantics and intersection types
• Functional Characters of Solvable Terms
• scientific article; zbMATH DE number 1479634 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 2120508 (Why is no real title available?)
• scientific article; zbMATH DE number 7204443 (Why is no real title available?)
• scientific article; zbMATH DE number 7700629 (Why is no real title available?)
• Linear logic
• Modal embeddings and calling paradigms
• Non-idempotent intersection types and strong normalisation
• Non-idempotent intersection types for the lambda-calculus
• Normal functors, power series and -calculus
• On phase semantics and denotational semantics: The exponentials
• Open call-by-value
• Programming languages and systems. 28th European symposium on programming, ESOP 2019, held as part of the European joint conferences on theory and practice of software, ETAPS 2019, Prague, Czech Republic, April 6--11, 2019. Proceedings
• Quantitative types for the linear substitution calculus
• Reasoning about call-by-need by means of types
• Reductions of Residuals are Finite
• Solvability in resource lambda-calculus
• Taylor expansion for Call-By-Push-Value
• The bang calculus and the two Girard's translations
• The bang calculus revisited
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The relational model is injective for multiplicative exponential linear logic
• The structural \(\lambda \)-calculus
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• Types of fireballs
• Uniformity and the Taylor expansion of ordinary lambda-terms

Cited in

(9)

• scientific article; zbMATH DE number 1273997 (Why is no real title available?)
• Böhm and Taylor for all!
• Meaningfulness and genericity in a subsuming framework (invited talk)
• Sharing and linear logic with restricted access
• A quantitative approach to global state composition
• Genericity through stratification
• Hybrid intersection types for PCF
• The benefits of diligence
• A rewriting theory for quantum -calculus

This page was built for publication: The bang calculus revisited

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