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
Volume31
Issue number1
Pages (from-to)113-145
ISSN0167-6423
DOIs
StatePublished - 1998
Peer-reviewedYes

Conference

Conference1st International Static Analysis Symposium (SAS 94)
Number1
CountryBelgium
CityNamur
Period27/09/199429/09/1994
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:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 3973111