Show simple item record

dc.contributor.authorMcDermott, D
dc.contributor.authorMycroft, A
dc.date.accessioned2019-02-22T18:01:32Z
dc.date.available2019-02-22T18:01:32Z
dc.date.issued2019
dc.identifier.isbn9783030171834
dc.identifier.issn0302-9743
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/289870
dc.description.abstractTraditionally, reasoning about programs under varying evaluation regimes (call-by-value, call-by-name etc.) was done at the meta-level, treating them as term rewriting systems. Levy’s call-by-push-value (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both call-by-value and call-by-name, and by allowing equational reasoning about changes to evaluation order between or within programs. We extend CBPV to additionally deal with call-by-need, which is non-trivial because of shared reductions. This allows the equational reasoning to also support call-by-need. As an example, we then prove that call-by-need and call-by-name are equivalent if nontermination is the only side-effect in the source language. We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.
dc.publisherSpringer International Publishing
dc.titleExtended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order
dc.typeConference Object
prism.endingPage262
prism.publicationDate2019
prism.publicationNameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
prism.startingPage235
prism.volume11423 LNCS
dc.identifier.doi10.17863/CAM.37109
dcterms.dateAccepted2019-01-26
rioxxterms.versionofrecord10.1007/978-3-030-17184-1_9
rioxxterms.versionAM
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2019-01-01
dc.contributor.orcidMcDermott, D [0000-0002-6705-1449]
dc.contributor.orcidMycroft, A [0000-0001-7013-8572]
dc.identifier.eissn1611-3349
dc.publisher.urlhttps://doi.org/10.1007/978-3-030-17184-1
rioxxterms.typeConference Paper/Proceeding/Abstract
pubs.funder-project-idEPSRC (1789520)
cam.issuedOnline2019-04-06
pubs.conference-nameESOP 2019
pubs.conference-start-date2019-04-08
cam.orpheus.successThu Nov 05 11:53:32 GMT 2020 - Embargo updated
pubs.conference-finish-date2019-04-11
rioxxterms.freetoread.startdate2020-01-01


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record