We introduce a computational interpretation for Hubert's choice operator ( ε). This interpretation yields a typed foundation for dynamic linking in software systems. The use of choice leads to interesting difficulties-some known from proof theory and others specific to the programming-language perspective that we develop. We therefore emphasize an important special case, restricting the nesting of choices. We define and investigate operational semantics. Interestingly, computation does not preserve types but it is type-sound. © Springer-Verlag 2004.
CITATION STYLE
Abadi, M., Gonthier, G., & Werner, B. (2004). Choice in dynamic linking. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2987, 12–26. https://doi.org/10.1007/978-3-540-24727-2_3
Mendeley helps you to discover research relevant for your work.