Hostname: page-component-7b9c58cd5d-9klzr Total loading time: 0 Render date: 2025-03-15T23:52:46.965Z Has data issue: false hasContentIssue false
  • English
  • Français

A computational formalization for partial evaluation

Published online by Cambridge University Press:  01 October 1997

JOHN HATCLIFF  and
OLIVIER DANVY
JOHN HATCLIFF
Affiliation:
Department of Computer Science, Oklahoma State University, 219 Mathematical Sciences, Stillwater, OK, 74078-1053, USA. E-mail: [email protected]
OLIVIER DANVY
Affiliation:
BRICS
Basic Research in Computer Science, Centre of the Danish National Research Foundation.
, Department of Computer Science, Aarhus University, Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We formalize a partial evaluator for Eugenio Moggi's computational metalanguage. This formalization gives an evaluation-order independent view of binding-time analysis and program specialization, including a proper treatment of call unfolding. It also enables us to express the essence of ‘control-based binding-time improvements’ for let expressions. Specifically, we prove that the binding-time improvements given by ‘continuation-based specialization’ can be expressed in the metalanguage via monadic laws.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 7 , Issue 5 , October 1997 , pp. 507 - 541
Copyright
1997 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)