Re: typed-based analysis and applications
Jens Palsberg wrote:
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> To the Types Community,
> Please send me references to papers on type-based analysis and applications.
some members of the the Turin group on Semantics and Logic of
Computation are specifically interested in type based program
analysis. Here is a short presentation of the activities and an
exhaustive list of the publications in the field. Most of the papers
are available from the home page of the group
The activity, up to now, has been mainly focused on strictness
and useless code analysis for higher order functional programs.
Type systems for strictness analysis have been proposed in [CF93]
(for an untyped language) and [CDG97], [CDG0X] for a typed language.
In these last two papers the relations with totality analysis are
also considered. In [DG97] an inference algorithm for strictness is
The investigations of useless code started with the work of
S. Berardi [Ber96] (see also [Boe94], [BerBoe95] and [BerBoe97]).
This approach was further developed in [CDG96], [DG00] and [D99].
The use of intersection types for useless code analysis has been
especially considered in [DP98] and [D00]. An overview of type based
useless code analysis can be found in [BCDG00].
[CF93] M Coppo, A. Ferrari, Type Inference, Abstract Interpretation
and Strictness Analysis, Theoretical Computer Science, 121:113-145,
[Boe94] L. Boerio. Extending Pruning Techniques to Second Order
Lambda Calculus. In ESOP'94, LNCS 788, pages 120-134, 1994.
[BerBoe95] S. Berardi and L. Boerio. Using Subtyping In Program
Optimization. In TLCA95, LNCS 902. Springer, 1995.
[Boe95] L. Boerio. Optimizing Programs Extracted from Proofs. PhD
thesis, Dipartimento di Informatica, UniversitÓ di Torino, Italy,
[Ber96] S. Berardi. Pruning Simply Typed Lambda Terms. Journal of
Logic and Computation, Vol.6 No 5, pages 663-681, 1996.
[CDG96] M. Coppo, F. Damiani, and P. Giannini. Refinement types for
program analysis. In SAS'96, LNCS 1145, pages 143-158. Springer,
[BerBoe97] S. Berardi and L. Boerio. Minimum Information Code in a
Pure Functional Language with Data Types. In TLCA 97, LNCS 1210,
pages 30-45. Springer, 1997.
[CDG97] M. Coppo, F. Damiani, and P. Giannini. On Strictness and
Totality. In TACS'97, LNCS 1281, pages 138-164. Springer, 1997.
[DG97] F. Damiani and P. Giannini. An Inference Algorithm for
Strictness. In TLCA'97, LNCS 1210, pages 129-146. Springer, 1997.
[CDG98] M. Coppo, F. Damiani, and P. Giannini. Inference based
analysis of functional programs: dead-code and strictness. In
MSJ-Memoir Vol. 2 ``Theories of Types and Proofs'', pages 143-176.
Mathematical Society of Japan, 1998.
[D98] F. Damiani. Non-standard type inference for functional
programs. PhD thesis, Dipartimento di Informatica, UniversitÓ di
Torino, Italy, February 1998.
[DP98] F. Damiani and F. Prost. Detecting and Removing Dead-Code
using Rank 2 Intersection. In International Workshop TYPES'96,
Selected Papers, LNCS 1512, pages 66-87. Springer, 1998.
[D99] F. Damiani. Useless-code detection and elimination for PCF
with algebraic Datatypes. In TLCA'99, LNCS 1581, pages 83-97.
[BCDG00] S. Berardi, M. Coppo, F. Damiani, and P. Giannini.
Type-based useless-code elimination for functional programs. In PLI
Workshop - SAIG'00, LNCS 1924, pages 172-189. Springer, 2000.
[D00] F. Damiani. Conjunctive types and useless-code elimination
(extended abstract). In ICALP Workshops, volume 8 of Proceedings in
Informatics, pages 271-285. Carleton-Scientific, 2000.
[DG00] F. Damiani and P. Giannini. Automatic useless-code detection
and elimination for hot functional programs. Journal of Functional
Programming, 10(6):509-559, 2000.
[CDG0X] M. Coppo, F. Damiani, and P. Giannini. Strictness, totality,
and non-standard type inference. Theoretical Computer Science, to
Prof. Mario Coppo
Dipartimento di Informatica
Universita' di Torino
C. Svizzera 185 - 10149 TORINO - ITALY
tel: +11 670 6738 fax +11 75 16 03
e-mail : email@example.com