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 at ?top-level? only. We give examples of its use and prove the correctness with respect to a natural-style operational semantics.
| Original language | English |
|---|---|
| Journal | Science of Computer Programming |
| Volume | 31 |
| Issue number | 1 |
| Pages (from-to) | 113-145 |
| ISSN | 0167-6423 |
| DOIs | |
| Publication status | Published - 1998 |
| Event | 1st International Static Analysis Symposium - Namur, Belgium Duration: 27 Sept 1994 → 29 Sept 1994 Conference number: 1 |
Conference
| Conference | 1st International Static Analysis Symposium |
|---|---|
| Number | 1 |
| Country/Territory | Belgium |
| City | Namur |
| Period | 27/09/1994 → 29/09/1994 |
Keywords
- Strictness and totality analysis
- Top-level conjunction types
- Natural-style operational semantics
- Annotated type system