NDLI: A synthetic operational account of call-by-need evaluation

Please wait, while we are loading the content...

A declarative and bidirectional model transformation approach based on graph co-spans

Coq: the world's best macro assembler?

An operational foundation for the tactic language of Coq

Proofs you can believe in: proving equivalences between Prolog semantics in Coq

A semantics for weakly encapsulated search in functional logic programs

Are needed redexes really needed?

A parameterized graph transformation calculus for finite graphs with monadic branches

Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order

A synthetic operational account of call-by-need evaluation

A logical correspondence between natural semantics and abstract machines

Engineering definitional interpreters

Extensible sparse functional arrays with circuit parallelism

Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures

Reasoning about higher-order relational specifications

Time refinement in a functional synchronous language

Unifying the Knuth-Bendix, recursive path and polynomial orders

Theory propagation and rational-trees

Decentralized execution of constraint handling rules for ensembles

Finite type extensions in constraint programming

Eventual linear ranking functions

Detecting decidable classes of finitely ground logic programs with function symbols

Shape analysis in a functional language by using regular languages

Efficient computation of program equivalence for confluent concurrent constraint programming

Random testing of purely functional abstract datatypes: guidelines for dealing with operation invariance

Prolog programming with a map-reduce parallel construct

Bidirectionalization for free with runtime recording: or, a light-weight approach to the view-update problem

A synthetic operational account of call-by-need evaluation

Content Provider	ACM Digital Library
Author	Zerny, Ian Danvy, Olivier
Abstract	We present the first operational account of call by need that connects syntactic theory and implementation practice. Syntactic theory: the storeless operational semantics using syntax rewriting to account for demand-driven computation and for caching intermediate results. Implementational practice: the store-based operational technique using memo-thunks to implement demand-driven computation and to cache intermediate results for subsequent sharing. The implementational practice was initiated by Landin and Wadsworth and is prevalent today to implement lazy programming languages such as Haskell. The syntactic theory was initiated by Ariola, Felleisen, Maraist, Odersky and Wadler and is prevalent today to reason equationally about lazy programs, on par with Barendregt et al.'s term graphs. Nobody knows, however, how the theory of call by need compares to the practice of call by need: all that is known is that the theory of call by need agrees with the theory of call by name, and that the practice of call by need optimizes the practice of call by name. Our operational account takes the form of three new calculi for lazy evaluation of lambda-terms and our synthesis takes the form of three lock-step equivalences. The first calculus is a hereditarily compressed variant of Ariola et al.'s call-by-need lambda-calculus and makes "neededness" syntactically explicit. The second calculus distinguishes between strict bindings (which are induced by demand-driven computation) and non-strict bindings (which are used for caching intermediate results). The third calculus uses memo-thunks and an algebraic store. The first calculus syntactically corresponds to a storeless abstract machine, the second to an abstract machine with local stores, and the third to a lazy Krivine machine, i.e., a traditional store-based abstract machine implementing lazy evaluation. The machines are intensionally compatible with extensional reasoning about lazy programs and they are lock-step equivalent. Each machine functionally corresponds to a natural semantics for call by need in the style of Launchbury, though for non-preprocessed λ-terms. Our results reveal a genuine and principled unity of computational theory and computational practice, one that readily applies to variations on the general theme of call by need.
Starting Page	97
Ending Page	108
Page Count	12
File Format	PDF
ISBN	9781450321549
DOI	10.1145/2505879.2505898
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2013-09-16
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Syntactic theories Abstract machines Call by need Functional correspondence Reduction semantics Syntactic correspondence Natural semantics Lazy evaluation
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A Synthetic Operational Account of Call-by-Need Evaluation

A functional correspondence between call-by-need evaluators and lazy abstract machines (2004).

A Natural Semantics for Completely Lazy Evaluation

Lazy evaluation and delimited control

Improvements in a functional core language with call-by-need operational semantics

This document in subdirectoryRS/03/24/ A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines (2003)

This document in subdirectoryRS/04/3/ A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines ∗ (2004)

A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers

A logical correspondence between natural semantics and abstract machines

A synthetic operational account of call-by-need evaluation

Similar Documents

A Synthetic Operational Account of Call-by-Need Evaluation

A functional correspondence between call-by-need evaluators and lazy abstract machines (2004).

A Natural Semantics for Completely Lazy Evaluation

Lazy evaluation and delimited control

Improvements in a functional core language with call-by-need operational semantics

This document in subdirectoryRS/03/24/ A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines (2003)

This document in subdirectoryRS/04/3/ A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines ∗ (2004)

A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers

A logical correspondence between natural semantics and abstract machines

A synthetic operational account of call-by-need evaluation