Loading...
Please wait, while we are loading the content...
Similar Documents
Dependent Types With Subtyping and Late-Bound Overloading (1999)
| Content Provider | CiteSeerX |
|---|---|
| Author | Chen, Gang Castagna, Giuseppe |
| Abstract | We present a calculus with dependent types, subtyping and late-bound overloading. Besides its theoretical interest this work is motivated by several practical needs that range from the definition of logic encodings, to proof specialization and reuse, and to object-oriented extension of the SML module system. The theoretical study of this calculus is not straightforward. While confluence is relatively easy to prove, subject reduction is much harder. We were not able to add overloading to any existing system with dependent types and subtyping, and prove subject reduction. This is why we also define here as by-product a new subtyping system for dependent types that improves previous systems and enjoys several properties (notably the transitivity elimination property). The calculus with overloading is then obtained as a conservative extension of this new system. Another difficult point is strong normalization, which is a necessary condition to the decidability of subtyping and typing relat... |
| File Format | |
| Publisher Date | 1999-01-01 |
| Access Restriction | Open |
| Subject Keyword | Necessary Condition New Subtyping System Dependent Type Late-bound Overloading Several Property Theoretical Study Logic Encoding Object-oriented Extension Theoretical Interest Difficult Point Several Practical Need Transitivity Elimination Property Strong Normalization Subject Reduction Sml Module System New System Previous System Conservative Extension |
| Content Type | Text |
