Thursday, 3 December 2009, 13:00 (note the unusual time!)
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: In this talk, I present type systems for flow-sensitive pointer analysis, live stack-heap (variables) analysis, and program optimization and correction. The type system for live stack-heap analysis is an enrichment of that for pointer analysis; the enrichment has the form of a second component being added to types of the latter system. Results of pointer analysis are proved useful via their use in the type system for live stack-heap analysis. The type system for program optimization and correction is also an augmentation of that for live stack-heap analysis, but the augmentation takes the form of a transformation component being added to inference rules of the latter system. The form of program optimization being achieved is that of dead-code elimination. The program correction results directly from removing statements that dispose memory cells being used latter in the program and indirectly from eliminating faulty code (causing the program to abort) that is dead. Therefore program optimization can result in program correction and vice versa. Our type systems have the advantage of being compositional and relatively-simply structured.