Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 5:38:11 PM
Last modification on : Friday, February 4, 2022 - 3:19:54 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:17:02 PM


  • HAL Id : inria-00071467, version 1


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



Record views


Files downloads