Pith. sign in

REVIEW

The Bang Calculus and the Two Girard's Translations

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1904.06845 v1 pith:73QOHJU2 submitted 2019-04-15 cs.LO cs.DMcs.PL

The Bang Calculus and the Two Girard's Translations

Giulio Guerrieri (Dipartimento di Informatica -- Scienza e Ingegneria (DISI) , Universit\`a di Bologna , Bologna , Italy) , Giulio Manzonetto (LIPN , UMR 7030 , Universit\'e Paris 13 , Sorbonne Paris Cit\'e
show 2 more authors
Villetaneuse France)
This is my paper
classification cs.LO cs.DMcs.PL
keywords bangcalculuscall-by-namecall-by-valuegirardlambda-calculitranslationsallows
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original abstract

We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-operator that allows both call-by-name and call-by-value lambda-calculi to be encoded in. We investigate how the bang calculus subsumes both call-by-name and call-by-value lambda-calculi from a syntactic and a semantic viewpoint.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.