We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Encoding Tight Typing in a Unified Framework

Abstract: This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, ie. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV.
Comments: arXiv admin note: text overlap with arXiv:2002.04011
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Cite as: arXiv:2105.00564 [cs.LO]
  (or arXiv:2105.00564v3 [cs.LO] for this version)

Submission history

From: Andrés Ezequiel Viso [view email]
[v1] Sun, 2 May 2021 22:27:57 GMT (69kb)
[v2] Fri, 9 Jul 2021 13:53:22 GMT (585kb)
[v3] Thu, 28 Oct 2021 08:58:17 GMT (285kb,D)

Link back to: arXiv, form interface, contact.