HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information

# Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution

Abstract : We \emph{present} the $\lambda\sigma_w^a$-calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how $\lambda\sigma_w^a$ can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely \emph{weak reduction strategies}, \emph{recursion}, \emph{space leaks}, \emph{recursive data structures}, and \emph{parallel evaluation}, in a uniform way. First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing $\lambda$-graph-reduction vs. environment-based evaluation. Second, we show how to add \emph{constructors and explicit recursion} to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of \emph{space leaks} in $\lambda\sigma_w^a$ and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the «trimming» performed by the STG machine does not leak space. In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages.
Keywords :
Document type :
Reports
Domain :

Cited literature [1 references]

https://hal.inria.fr/inria-00073599
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 1:17:24 PM
Last modification on : Friday, February 4, 2022 - 3:22:04 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:51:40 PM

### Identifiers

• HAL Id : inria-00073599, version 1

### Citation

Zine-El-Abidine Benaissa, Pierre Lescanne, Kristoffer H. Rose. Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution. [Research Report] RR-3092, INRIA. 1997. ⟨inria-00073599⟩

Record views