Bounding normalization time through intersection types
Logic in Computer Science
2013-08-02 v1
Abstract
Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.
Cite
@article{arxiv.1307.8205,
title = {Bounding normalization time through intersection types},
author = {Erika De Benedetti and Simona Ronchi Della Rocca},
journal= {arXiv preprint arXiv:1307.8205},
year = {2013}
}
Comments
In Proceedings ITRS 2012, arXiv:1307.7849