Strictness and Totality Analysis
Strictness and Totality Analysis
Kirsten Lackner Solberg
Hanne Riis Nielson
Flemming Nielson
In 6th
NWPT, page 346
Abstract:
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.
Comments
Solberg: Dept. of Math. and Computer Science, Odense
University, Denmark. Nielson: Computer Science Dept., Aarhus University,
Denmark. Email: {kls,hrn,fn}@daimi.aau.dk.
Available as PostScript,
DVI.
![[BRICS symbol]](http://www.daimi.aau.dk/BRICS/GIF/BRICS/msymbol8mm.GIF)
BRICS WWW home page