Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

12

FOSSACS
2016
Springer

favoriteEmaildiscussreport

51views Software Engineering» more FOSSACS 2016»

Reasoning About Call-by-need by Means of Types

8 years 18 days ago

Reasoning About Call-by-need by Means of Types

Download www.pps.univ-paris-diderot.fr

Abstract. We ﬁrst develop a (semantical) characterization of call-byneed normalization by means of typability, i.e. we show that a term is normalizing in call-by-need if and only if it is typable in a suitable system with non-idempotent intersection types. This ﬁrst result is used to derive a new completeness proof of call-by-need w.r.t. call-by-name. Concretely, we show that call-by-need and call-by-name are observationally equivalent, so that in particular, the former turns out to be a correct implementation of the latter.

Delia Kesner

Real-time Traffic

FOSSACS 2016 | Software Engineering |

claim paper

Related Content

» Modeling and Reasoning about Service Behaviors and Their Compositions

» Local ClosedWorld Assumptions for reasoning about Semantic Web data

» Singleton types here singleton types there singleton types everywhere

» A Formal Approach to Reasoning about the Effectiveness of Partial Evaluation

» Relational parametricity for references and recursive types

» The logical approach to stack typing

» Types with semantics soundness proof assistant

» Fast and loose reasoning is morally correct

» Dependent type inference with interpolants

» Toward a foundational typed assembly language

Post Info
More Details (n/a)

Added	03 Apr 2016
Updated	03 Apr 2016
Type	Journal
Year	2016
Where	FOSSACS
Authors	Delia Kesner

Comments (0)