@inproceedings{XiLICS00,
author = "Hongwei Xi",
title = {{Imperative Programming with Dependent Types}}
booktitle = "Proceedings of 15th IEEE Symposium on Logic in Computer Science",
year = 2000,
month = "June",
address = "Santa Barbara",
pages = "375--387",
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 {\em Xanadu}, forming both
static and dynamic semantics and then establishing the type soundness
theorem. We also present realistic programming examples in support of
the practicality of Xanadu. We claim that the language design of
Xanadu is novel and it serves as an informative example to demonstrate
a means to combine imperative programming with dependent types.
}}
}