Università di Torino

Research on "Formal Methods in Computing"

Strictness, totality, and non-standard type inference

Mario COPPO , Ferruccio DAMIANI , and Paola GIANNINI

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.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


   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}

["Formal Methods in Computing" group] [Department's HOME]

Last update: Mar 14, 2007