Characterisation of normalisation properties for λμ using Strict negated intersection types
- Submitting institution
-
Imperial College of Science, Technology and Medicine
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2401
- Type
- D - Journal article
- DOI
-
10.1145/3149823
- Title of journal
- ACM Transactions on Computational Logic
- Article number
- ARTN 3
- First page
- 1
- Volume
- 19
- Issue
- 1
- ISSN
- 1529-3785
- Open access status
- Not compliant
- Month of publication
- February
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
10.1145/3149823
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
0
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The work introduces strict negated intersection types that are used to define a type system for λμ and an approximation semantics for λμ. Both can be used to define semantics for λμ and together they are used to characterise all important notions of termination. The results of this paper give a semantic foundation to the use of λμ, with its embedded notion of control through delimited continuations, in programming. The paper is an extension of an ITRS'16 paper (https://arxiv.org/abs/1702.02273v1).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
