Strictness and Totality Analysis

Publication: Research - peer-reviewConference article – Annual report year: 1998

View graph of relations

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 languageEnglish
JournalScience of Computer Programming
Publication date1998
Volume31
Journal number1
Pages113-145
ISSN0167-6423
DOIs
StatePublished

Conference

Conference1st International Static Analysis Symposium (SAS 94)
Number1
CountryBelgium
CityNamur
Period27/09/9429/09/94
CitationsWeb of Science® Times Cited: 3

Keywords

  • Strictness and totality analysis, Top-level conjunction types, Natural-style operational semantics, Annotated type system
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

ID: 3973111