BakBdL12 (In proceedings)
|
Author(s) | Steffen van Bakel, Franco Barbanera and Ugo de' Liguoro |
Title | « Characterisation of Strongly Normalising -Terms » |
In | Proc. of ITRS'12 |
Series | EPTCS |
Editor(s) | Stephane Graham-Lengrand and Luca Paolini |
Volume | 121 |
Page(s) | 1-17 |
Year | 2013 |
Abstract |
A characterisation of strongly normalising terms of the -calculus is provided by means of a typeing system with intersection and product types. The presence of the latter ones (and of the type ) enables us to represent the particular notion of continuation used in the literature for defining the semantics of the -calculus. This allows to lift to -terms the well-known characterisation property for -terms possessed by the intersection types. An interpretation of Parigot's propositional logical system into ours will then provide an alternative proof of strong normalisation for terms typeable in that system. |
Download the complete article:
@inproceedings{BakBdL12,
volume = {121},
author = {Steffen van Bakel and Franco Barbanera and Ugo de' Liguoro},
series = {{EPTCS}},
booktitle = {{Proc. of ITRS'12}},
editor = {Stephane Graham-Lengrand and Luca Paolini},
title = {{Characterisation of Strongly Normalising $\lambda\mu$-Terms}},
abstract = {A characterisation of strongly normalising terms of the
$\lambda\mu$-calculus is provided by means of a typeing system
with intersection and product types. The presence of the latter
ones (and of the type $\omega$) enables us to represent the
particular notion of continuation used in the literature for
defining the semantics of the $\lambda\mu$-calculus. This allows
to lift to $\lambda\mu$-terms the well-known characterisation
property for $\lambda$-terms possessed by the intersection types.
An interpretation of Parigot's propositional logical system into
ours will then provide an alternative proof of strong
normalisation for terms typeable in that system.},
tag = {ITRS'12},
localfile = { http://dx.doi.org/10.4204/EPTCS.121.1},
year = {2013},
pages = {1-17},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)