In this paper we present two non-standard-type inference systems for conjunctive strictness and totality analyses of higher-order-typed functional programs and prove completeness results for both the strictness and the totality-type entailment relations. We also study the interactions between strictness and totality analyses, showing that the information obtainable by a system that combines the two analyses, even though more refined than the information given by the two separate systems, cannot be effectively used. A main feature of our approach is that all the results are proved by relying directly on the operational semantics of the programming language considered. This leads to a rather direct presentation which involves relatively little mathematical overhead.

Strictness, totality, and non-standard type inference

COPPO, Mario;DAMIANI, Ferruccio;
2002-01-01

Abstract

In this paper we present two non-standard-type inference systems for conjunctive strictness and totality analyses of higher-order-typed functional programs and prove completeness results for both the strictness and the totality-type entailment relations. We also study the interactions between strictness and totality analyses, showing that the information obtainable by a system that combines the two analyses, even though more refined than the information given by the two separate systems, cannot be effectively used. A main feature of our approach is that all the results are proved by relying directly on the operational semantics of the programming language considered. This leads to a rather direct presentation which involves relatively little mathematical overhead.
2002
272 (1-2)
69
112
http://www.sciencedirect.com/science/article/pii/S0304397500003480
Program analysis; Strictness; Totality; Non-standard-type inference; Intersection types
COPPO M; DAMIANI F; GIANNINI P
File in questo prodotto:
File Dimensione Formato  
TCS-2002.pdf

Accesso riservato

Descrizione: Articolo principale (rivista)
Tipo di file: PDF EDITORIALE
Dimensione 331.31 kB
Formato Adobe PDF
331.31 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/124737
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 6
social impact