CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Call-by-name, Call-by-need, and McCarthy's Amb

Andrew Keith Moran (Institutionen för datavetenskap)
Göteborg : Chalmers University of Technology, 1998. ISBN: 91-7197-684-1.

This dissertation examines the behaviour of McCarthy's amb in both a call-by-name and call-by-need context. Instead of following the usual denotational approach, we choose to explore the operational alternative. The languages involved are higher-order, and contain algebraic datatypes. For both call-by-name and call-by-need we follow a simple programme:

1. Develop a number of equivalent operational semantics; one that is "obviously correct", and others that are more abstract and better suited to reasoning.

2. Define notions of cost relative to the abstract operational semantics, and use the cost-decorated operational relations to define approximation and equivalence.

3. Develop an operational theory for the approximation and equivalence.

The call-by-name operational theory contains not only the expected equational laws, but also proof rules for proving properties of recursive programs containing McCarthy's amb: the cost equivalence theorem and cost equivalence induction. The theory is applied to many non-trivial examples, including stream processors, the combinators that form the basis of Fudgets. The programme is repeated for a call-by-need language containing McCarthy's amb, culminating in a context lemma for the convergent behaviour of McCarthy's amb in a call-by-need context.

Denna post skapades 2006-08-25. Senast ändrad 2013-09-25.
CPL Pubid: 866


Institutioner (Chalmers)

Institutionen för datavetenskap (1993-2001)


Information Technology

Chalmers infrastruktur

Ingår i serie

Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie 1424