Dependent Types in Practical Programming
Abstract
Programming is a notoriously error-prone process, and a great deal of evidence in practice has demonstrated that the use of a type system in a programming language can effectively detect program errors at compile-time. Moreover, some recent studies have indicated that the use of types can lead to significant enhancement of program performance at run-time. For the sake of practicality of type-checking, most type systems developed for general purpose programming languages tend to be simple and coarse, and this leaves ample room for improvement. As an advocate of types, this thesis addresses the issue of designing a type system for practical programming in which a notion of dependent types is available, leading to more accurate capture of program invariants with types.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 06, 1998
- Accession Number
- ADA597740
Entities
People
- Hongwei Xi
Organizations
- Carnegie Mellon University