Retour à la page du séminaire

8/06/2000 : Stefano Berardi (Turin)
Useless code Analysis: a position paper of Turin Logical Framework team.


we introduce the work done in the past ten years in Turin, concerning the use of type inference to isolate program properties.In particular, we explain how a program may be cluttered with useless code when it is obtained by indirect means (like program extraction from proofs, or extensive reuse of libraries), and how types may help in detecting and removing such useless code.