Dependent Types for Program Understanding

Abstract. Weakly-typed languages such as Cobol often force programrepresent distinct data abstractions using the same low-level physical type. In this paper, we describe a technique to recover implicitlydata abstractions from programs using type inference. We present a novel system of dependent types which we call guarded types, a pathsensitive algorithm for inferring guarded types for Cobol programs, and a semantic characterization of correct guarded typings. The results of our inference technique can be used to enhance program understanding for legacy applications, and to enable a number of type-based program transformations.

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Raghavan Komondoor, Ganesan Ramalingam, Satish Chandra, John Field
• Keywords: Algorithms, Correct Guarded Typings, Distinct Data Abstractions, Low-level Physical Type, TACAS 2005