Name
Abstract | ||
|---|---|---|
Type specialisation, like partial evaluation, is an approach to specialising programs. But type specialisation works in a very different way, using a form of type inference. Previous articles have described the method and demonstrated its power as a program transformation, but its correctness has not previously been addressed. Indeed, it is not even clear what correctness should mean: type specialisation transforms programs to others with different types, so clearly cannot preserve semantics in the usual sense. In this paper we explain why finding a correctness proof was difficult, we motivate a correctness condition, and we prove that type specialisation satisfies it. Perhaps unsurprisingly, type-theoretic methods turned out to crack the nut. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/3-540-46425-5_14 | European Symposium on Programming |
Keywords | Field | DocType |
type specialisation work,type inference,correctness condition,program transformation,type specialisation,previous article,different type,specialising program,correctness proof,partial evaluation | Program transformation,Correctness proofs,Programming language,Partial evaluation,Computer science,Correctness,Type inference,Theoretical computer science,Semantics | Conference |
Volume | ISSN | ISBN |
1782 | 0302-9743 | 3-540-67262-1 |
Citations | PageRank | References |
3 | 0.43 | 10 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| John Hughes | 1 | 1573 | 174.22 |