Safe Recursive Boxes

Gérard Boudol 1
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
Abstract : We study recursion in call-by-value functional languages, and more specifically a recursion construct recently introduced by Dreyer, which builds recursive boxed values. We design a type and effect system, featuring binary effects, for a call-by-value lambda-calculus extended with this recursion construct. We show that this system has the good properties required for an implicitly, statically typed language: the typable expressions do not yield run-time errors, and a principal type can be computed for any typable expression.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071467
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 5:38:11 PM
Last modification on : Monday, November 12, 2018 - 10:58:00 AM
Long-term archiving on: Sunday, April 4, 2010 - 10:17:02 PM

Identifiers

  • HAL Id : inria-00071467, version 1

Citation

Gérard Boudol. Safe Recursive Boxes. RR-5115, INRIA. 2004. ⟨inria-00071467⟩

Share

Metrics

Record views

137

Files downloads

140