[Prev][Next][Index][Thread]

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.

Dear Jens
  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
         http://www.di.unito.it/~lambda/g1/
  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
proposed.
   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].
 Greetings
                                        Mario Coppo



[CF93] M Coppo, A. Ferrari, Type Inference, Abstract Interpretation
and Strictness Analysis, Theoretical Computer Science, 121:113-145,
1993.

[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,
1995.

[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,
1996.

[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.
Springer, 1999.

[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
appear.


--
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 : coppo@di.unito.it