Logic in Computer Science (LICS 2000)

Paper: Imperative Programming with Dependent Types (at LICS 2000)

Authors: Hongwei Xi

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.

BibTeX

  @InProceedings{Xi-ImperativeProgrammi,
    author = 	 {Hongwei Xi},
    title = 	 {Imperative Programming with Dependent Types},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {375--387},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }