Strictness and Totality Analysis
DOI:
https://doi.org/10.7146/dpb.v23i474.6947Abstract
We define a novel inference system for strictness and totality analysis for the simply-typed lazy lambda-calculus with constants and fixpoints. Strictness information identifies those terms that definitely denote bottom (i.e. do not evaluate to WHNF) whereas totality information identifies those terms that definitely do not denote bottom (i.e. do evaluate to WHNF). The analysis is presented as an annotated type system allowing conjunctions only at ``top level´´. We give examples of its use and prove the correctness with respect to a natural-style operational semantics.Downloads
Published
1994-06-01
How to Cite
Solberg, K. L., & Nielson, H. R. (1994). Strictness and Totality Analysis. DAIMI Report Series, 23(474). https://doi.org/10.7146/dpb.v23i474.6947
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.