A calculus for link-time compilation

Elena Machkasova, Franklyn A. Turbak

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 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 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.

Original languageEnglish (US)
Title of host publicationProgramming 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
EditorsGert Smolka
PublisherSpringer Verlag
Pages260-274
Number of pages15
ISBN (Print)3540672621, 9783540672623
DOIs
StatePublished - 2000
Externally publishedYes
Event9th 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 2000Apr 2 2000

Publication series

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

Conference

Conference9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000
CountryGermany
CityBerlin
Period3/25/004/2/00

Fingerprint Dive into the research topics of 'A calculus for link-time compilation'. Together they form a unique fingerprint.

Cite this