Loading...
Please wait, while we are loading the content...
Similar Documents
A graphical presentation of $ML^{F}$ types with a linear-time unification algorithm
| Content Provider | ACM Digital Library |
|---|---|
| Author | Rémy, Didier Yakobowski, Boris |
| Abstract | $ML^{F}$ is a language that extends ML and System SF and combines the benefits of both. We propose a dag representation of $ML^{F}$ types that superposes a term-dag, encoding the underlying term-structure with sharing, and a binding tree encoding the binding-structure. Compared to the original definition, this representation is more canonical as it factors out most of the notational details; it is also closely related to first-order terms. Moreover, it permits a simpler and more direct definition of type instance that combines type instance on first-order term-dags, simple operations on dags, and a control that allows or rejects potential instances. Using this representation, we build a linear-time unification algorithm for MLF types, which we prove sound and complete with respect to the specification. |
| Starting Page | 27 |
| Ending Page | 38 |
| Page Count | 12 |
| File Format | |
| ISBN | 159593393X |
| DOI | 10.1145/1190315.1190321 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2007-01-16 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Types Unification Graphs System sf Mlf Binders |
| Content Type | Text |
| Resource Type | Article |
