Research on "Formal Methods in Computing"

Strictness, totality, and non-standard type inference

ABSTRACT. 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. In particular we show that (wrt the possibility of replacing safely a non-strict application with a strict one) the strictness and totality types inferred by a combined system (extending the combined systems proposed by Solberg et al) give the same information given by the strictness types and the totality types inferred by the two separate systems: one for strictness and one for totality. 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.

• pdf

BIBTEX.

@article{Coppo-Damiani-Giannini:TCS-02,
   author    = {M. Coppo and F. Damiani and P. Giannini},
   title     = {Strictness, totality, and non-standard type inference},
   year      = {2002},
   volume    = {272},
   number    = {1-2},
   pages     = {69--112},
   journal   = {Theoretical Computer Science},
   publisher = {Elsevier}
}