A calculus for link-time compilation

Elena Machkasova; Franklyn A. Turbak

doi:10.1007/3-540-46425-5_17

A calculus for link-time compilation

Elena Machkasova, Franklyn A. Turbak

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

22 Scopus citations

Abstract

We present a module calculus for studying a simple model of link-time compilation. The calculus is stratified into a term calculus, a core module calculus, and a linking calculus. At each level, we show that the calculus enjoys a computational soundness property: if two terms are equivalent in the calculus, then they have the same outcome in a small- step operational semantics. This implies that any module transformation justified by the calculus is meaning preserving. This result is interesting because recursive module bindings thwart confluence at two levels of our calculus, and prohibit application of the traditional technique for showing computational soundness, which requires confluence. We introduce a new technique, based on properties we call lift and project, that uses a weaker notion of confluence with respect to evaluation to establish computational soundness for our module calculus. We also introduce the weak distributivity property for a transformation T operating on modules D₁ and D₂ linked by⊕: T(D₁ ⊕ D₂) = T(T(D₁) ⊕ T(D₂)). We argue that this property finds promising candidates for link-time optimizations.

Original language	English (US)
Title of host publication	Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings
Editors	Gert Smolka
Publisher	Springer Verlag
Pages	260-274
Number of pages	15
ISBN (Print)	3540672621, 9783540672623
DOIs	https://doi.org/10.1007/3-540-46425-5_17
State	Published - 2000
Externally published	Yes
Event	9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 - Berlin, Germany Duration: Mar 25 2000 → Apr 2 2000

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1782
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000
Country/Territory	Germany
City	Berlin
Period	3/25/00 → 4/2/00

Bibliographical note

Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2000.

Access

10.1007/3-540-46425-5_17

OpenUrl availability

Full text

Cite this

Machkasova, E., & Turbak, F. A. (2000). A calculus for link-time compilation. In G. Smolka (Ed.), Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings (pp. 260-274). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1782). Springer Verlag. https://doi.org/10.1007/3-540-46425-5_17

A calculus for link-time compilation. / Machkasova, Elena; Turbak, Franklyn A.
Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings. ed. / Gert Smolka. Springer Verlag, 2000. p. 260-274 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1782).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Machkasova, E & Turbak, FA 2000, A calculus for link-time compilation. in G Smolka (ed.), Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1782, Springer Verlag, pp. 260-274, 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, 3/25/00. https://doi.org/10.1007/3-540-46425-5_17

Machkasova E, Turbak FA. A calculus for link-time compilation. In Smolka G, editor, Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings. Springer Verlag. 2000. p. 260-274. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-46425-5_17

Machkasova, Elena ; Turbak, Franklyn A. / A calculus for link-time compilation. Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings. editor / Gert Smolka. Springer Verlag, 2000. pp. 260-274 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7692c35a5d504e468d951180b1f2cda6,

title = "A calculus for link-time compilation",

abstract = "We present a module calculus for studying a simple model of link-time compilation. The calculus is stratified into a term calculus, a core module calculus, and a linking calculus. At each level, we show that the calculus enjoys a computational soundness property: if two terms are equivalent in the calculus, then they have the same outcome in a small- step operational semantics. This implies that any module transformation justified by the calculus is meaning preserving. This result is interesting because recursive module bindings thwart confluence at two levels of our calculus, and prohibit application of the traditional technique for showing computational soundness, which requires confluence. We introduce a new technique, based on properties we call lift and project, that uses a weaker notion of confluence with respect to evaluation to establish computational soundness for our module calculus. We also introduce the weak distributivity property for a transformation T operating on modules D1 and D2 linked by⊕: T(D1 ⊕ D2) = T(T(D1) ⊕ T(D2)). We argue that this property finds promising candidates for link-time optimizations.",

author = "Elena Machkasova and Turbak, {Franklyn A.}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2000.; 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 ; Conference date: 25-03-2000 Through 02-04-2000",

year = "2000",

doi = "10.1007/3-540-46425-5_17",

language = "English (US)",

isbn = "3540672621",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "260--274",

editor = "Gert Smolka",

booktitle = "Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings",

}

TY - GEN

T1 - A calculus for link-time compilation

AU - Machkasova, Elena

AU - Turbak, Franklyn A.

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2000.

PY - 2000

Y1 - 2000

N2 - We present a module calculus for studying a simple model of link-time compilation. The calculus is stratified into a term calculus, a core module calculus, and a linking calculus. At each level, we show that the calculus enjoys a computational soundness property: if two terms are equivalent in the calculus, then they have the same outcome in a small- step operational semantics. This implies that any module transformation justified by the calculus is meaning preserving. This result is interesting because recursive module bindings thwart confluence at two levels of our calculus, and prohibit application of the traditional technique for showing computational soundness, which requires confluence. We introduce a new technique, based on properties we call lift and project, that uses a weaker notion of confluence with respect to evaluation to establish computational soundness for our module calculus. We also introduce the weak distributivity property for a transformation T operating on modules D1 and D2 linked by⊕: T(D1 ⊕ D2) = T(T(D1) ⊕ T(D2)). We argue that this property finds promising candidates for link-time optimizations.

AB - We present a module calculus for studying a simple model of link-time compilation. The calculus is stratified into a term calculus, a core module calculus, and a linking calculus. At each level, we show that the calculus enjoys a computational soundness property: if two terms are equivalent in the calculus, then they have the same outcome in a small- step operational semantics. This implies that any module transformation justified by the calculus is meaning preserving. This result is interesting because recursive module bindings thwart confluence at two levels of our calculus, and prohibit application of the traditional technique for showing computational soundness, which requires confluence. We introduce a new technique, based on properties we call lift and project, that uses a weaker notion of confluence with respect to evaluation to establish computational soundness for our module calculus. We also introduce the weak distributivity property for a transformation T operating on modules D1 and D2 linked by⊕: T(D1 ⊕ D2) = T(T(D1) ⊕ T(D2)). We argue that this property finds promising candidates for link-time optimizations.

UR - http://www.scopus.com/inward/record.url?scp=84947287126&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84947287126&partnerID=8YFLogxK

U2 - 10.1007/3-540-46425-5_17

DO - 10.1007/3-540-46425-5_17

M3 - Conference contribution

AN - SCOPUS:84947287126

SN - 3540672621

SN - 9783540672623

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 260

EP - 274

BT - Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings

A2 - Smolka, Gert

PB - Springer Verlag

T2 - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000

Y2 - 25 March 2000 through 2 April 2000

ER -

A calculus for link-time compilation

Abstract

Publication series

Conference

Bibliographical note

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this