The bang calculus and the two Girard's translations

MaRDI QIDQ5018484zbMATH OpenFDO

Authors Giulio Guerrieri, Giulio Manzonetto

Publication date 20 December 2021

Full work available at URL https://arxiv.org/abs/1904.06845, http://eptcs.web.cse.unsw.edu.au/paper.cgi?LinearityTLLA2018.2

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1231468
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Girard translation and logical predicates
• scientific article; zbMATH DE number 2079016
• Term Rewriting and Applications

Cites work

• Call-by-name, call-by-value and the \(\lambda\)-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
• Categorical semantics of linear logic
• Collapsing non-idempotent intersection types
• Computational interpretations of linear logic
• Finiteness spaces
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 512773 (Why is no real title available?)
• Lambda calculus and intuitionistic linear logic
• Linear logic
• Localisation and interaction in one dimension
• Mathematical foundations of programming semantics, 9th international conference, New Orleans, LA, USA, April 7--10, 1993. Proceedings
• Notions of computation and monads
• On phase semantics and denotational semantics: The exponentials
• Open call-by-value
• Parallel reductions in \(\lambda\)-calculus
• Polarized proof-nets and \(\lambda \mu\)-calculus
• Probabilistic coherence spaces as a model of higher-order probabilistic computation
• Programming languages and systems. 16th Asian symposium, APLAS 2018, Wellington, New Zealand, December 2--6, 2018. Proceedings
• Proof nets and the call-by-value \(\lambda\)-calculus
• Term Rewriting and Applications
• The call-by-value λ-calculus: a semantic investigation
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The Scott model of linear logic is the extensional collapse of its relational model

Cited in

(20)

• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• The bang calculus revisited
• Taylor expansion, finiteness and strategies
• 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 spirit of node replication
• scientific article; zbMATH DE number 1231468 (Why is no real title available?)
• scientific article; zbMATH DE number 2079016 (Why is no real title available?)
• Girard translation and logical predicates
• On reduction and normalization in the computational core
• scientific article; zbMATH DE number 7756108 (Why is no real title available?)
• The bang calculus revisited
• scientific article; zbMATH DE number 7809762 (Why is no real title available?)
• Node Replication: Theory And Practice
• Categorifying non-idempotent intersection types
• Meaningfulness and genericity in a subsuming framework (invited talk)
• Sharing and linear logic with restricted access
• Genericity through stratification
• The benefits of diligence
• A rewriting theory for quantum -calculus

This page was built for publication: The bang calculus and the two Girard's translations

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