Strictness and Totality Analysis

Strictness and Totality Analysis

Kirsten Lackner Solberg
Hanne Riis Nielson
Flemming Nielson

In 6th NWPT, page 346


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.

Solberg: Dept. of Math. and Computer Science, Odense University, Denmark. Nielson: Computer Science Dept., Aarhus University, Denmark. Email: {kls,hrn,fn}

Available as PostScript, DVI.

[BRICS symbol] BRICS WWW home page