Loading...
Please wait, while we are loading the content...
Similar Documents
Imperative Programming with Dependent Types (Extended Abstract)
| Content Provider | Semantic Scholar |
|---|---|
| Author | Xi, Hongwei |
| Copyright Year | 2000 |
| 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 languageXanadu, 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. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.bu.edu/~hwxi/academic/papers/XanaduAbs.ps |
| Alternate Webpage(s) | http://www.ececs.uc.edu/~hwxi/academic/papers/XanaduAbs.ps |
| Alternate Webpage(s) | http://www.cs.bu.edu/~hwxi/academic/papers/lics00.ps |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
