| deLiguoroT19a (Article)
|
| Author(s) | Ugo de' Liguoro and Riccardo Treglia |
| Title | « Intersection Types for the Computational lambda-Calculus » |
| Journal | CoRR |
| Volume | abs/1907.05706 |
| Year | 2019 |
| URL | http://arxiv.org/abs/1907.05706 |
| Abstract |
| We study polymorphic type assignment systems for untyped lambda-calculi with effects. We introduce an intersection type assignment system for Moggi's computational lambda-calculus, where a generic monad T is considered, and provide models of the calculus via inverse limit and filter model constructions and relate them. We prove soundness and completeness of the type system, together with subject reduction and expansion properties. Finally we establish the computational adequacy of the filter model via a characterization theorem of convergent terms. |
@article{deLiguoroT19a,
archiveprefix = {arXiv},
volume = {abs/1907.05706},
author = {Ugo de' Liguoro and Riccardo Treglia},
url = {http://arxiv.org/abs/1907.05706},
title = {Intersection Types for the Computational lambda-Calculus},
abstract = {We study polymorphic type assignment systems for untyped
lambda-calculi with effects. We introduce an intersection type
assignment system for Moggi's computational lambda-calculus, where
a generic monad T is considered, and provide models of the
calculus via inverse limit and filter model constructions and
relate them. We prove soundness and completeness of the type
system, together with subject reduction and expansion properties.
Finally we establish the computational adequacy of the filter
model via a characterization theorem of convergent terms. },
eprint = {1907.05706},
journal = {CoRR},
year = {2019},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
