Characterisation of approximation and (head) normalisation for λμ using strict intersection types
File(s)1702.02273v1.pdf (159.92 KB)
Published version
Author(s)
van Bakel, Steffen
Type
Conference Paper
Abstract
We study the strict type assignment for λμ that is presented in [7]. We define a notion of approximants of λμ-terms, show that it generates a semantics, and that for each typeable term there is an approximant that has the same type. We show that this leads to a characterisation via assignable types for all terms that have a head normal form, and to one for all terms that have a normal form, as well as to one for all terms that are strongly normalisable.
Date Issued
2017-02-08
Date Acceptance
2017-02-01
Citation
Electronic Proceedings in Theoretical Computer Science, EPTCS, 2017, 242, pp.20-30
ISSN
2075-2180
Start Page
20
End Page
30
Journal / Book Title
Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume
242
Copyright Statement
© Steffen van Bakel. This work is licensed under theCreative Commons Attribution License (https://creativecommons.org/licenses/by/3.0/)
License URL
Source
Eighth Workshopon Intersection Types and Related Systems (ITRS 2016)
Subjects
cs.LO
cs.LO
F.3.2
Publication Status
Published
Start Date
2016-06-26
Coverage Spatial
Porto, Portugal
Date Publish Online
2017-02-08