Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

BakBdL12 (In proceedings)
Author(s) Steffen van Bakel, Franco Barbanera and Ugo de' Liguoro
Title« Characterisation of Strongly Normalising λμ-Terms »
InProc. of ITRS'12
SeriesEPTCS
Editor(s) Stephane Graham-Lengrand and Luca Paolini
Volume121
Page(s)1-17
Year2013
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: EPTCS.121.1

BibTeX code

@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},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!