On strictness and totality

Mario Coppo, Ferruccio Damiani, Paola Giannini

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

In this paper we present a revised and extended version of the strictness and totality type assignment system introduced by Solberg, Nielson and Nielson in the Static Analysis Symposium ’94. Our main result is that (w.r.t. the possibility of replacing safely a lazy application by a strict one) the strictness and totality information given by this system is equivalent to the information given by two separate systems: one for strictness, and one for totality. This result is interesting from both a theoretical (understanding of the relations between strictness and totality) and a practical (more efficient checking and inference algorithms) point of view. Moreover we prove that both the system for strictness and the system for totality have a sound and complete inclusion relation between types w.r.t. the semantics induced by the term model of a language including a convergence to weak head normal form test at higher types.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computer Software - 3rd International Symposium, TACS 1997, Proceedings
EditorsMartín Abadi, Takayasu Ito
PublisherSpringer Verlag
Pages138-164
Number of pages27
ISBN (Print)354063388X, 9783540633884
DOIs
Publication statusPublished - 1997
Externally publishedYes
Event3rd International Symposium on Theoretical Aspects of Computer Software, TACS 1997 - Sendai, Japan
Duration: 23 Sept 199726 Sept 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1281
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Symposium on Theoretical Aspects of Computer Software, TACS 1997
Country/TerritoryJapan
CitySendai
Period23/09/9726/09/97

Fingerprint

Dive into the research topics of 'On strictness and totality'. Together they form a unique fingerprint.

Cite this