Imperative Programming with Dependent Types (Extended Abstract)

• Main Author: Hongwei Xi
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Published: 2000
• Subjects: DML
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.7329; http://www.ececs.uc.edu/~hwxi/header/./academic/papers/lics00.ps

) Hongwei Xi University of Cincinnati [e-mail] Abstract In this paper, we enrich imperative programming with a form of dependent types. We start with explaining some motivations for this enrichment and mentioning some major obstacles that need to be overcome. We then present the design of a source level dependently typed imperative programming language Xanadu, forming both static and dynamic semantics and then establishing the type soundness theorem. We also present realistic examples, which have all been verified in a prototype implementation, in support of the practicality of Xanadu. We claim that the language design of Xanadu is novel and it serves as an informative example that demonstrates a means to combine imperative programming with dependent types. 1 Introduction In [16, 8], the functional programming language ML is extended with a restricted form of dependent types. This extension yields a dependently typed functional programming language DML, in which the pro.