Choice in Dynamic Linking Export

@incollection{citeulike:1743125, abstract = {We introduce a computational interpretation for Hilbert\&\#8217;s choice operator\&\#160;( e). This interpretation yields a typed foundation for dynamic linking in software systems. The use of choice leads to interesting difficulties\&\#8212;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.}, author = {Abadi, Mart\'{\i}n and Gonthier, Georges and Werner, Benjamin}, citeulike-article-id = {1743125}, citeulike-linkout-0 = {http://www.springerlink.com/content/11m0bcrmg00nrwqv}, journal = {Foundations of Software Science and Computation Structures}, keywords = {epsilon, natural\_deduction, proof\_theory}, pages = {12--26}, posted-at = {2007-10-08 20:02:28}, priority = {2}, title = {Choice in Dynamic Linking}, url = {http://www.springerlink.com/content/11m0bcrmg00nrwqv}, year = {2004} }

TY - CHAP ID - citeulike:1743125 L3 - citeulike-article-id:1743125 N2 - We introduce a computational interpretation for Hilbert’s choice operator ( e). 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. JF - Foundations of Software Science and Computation Structures EP - 26 TI - Choice in Dynamic Linking SP - 12 KW - epsilon KW - natural_deduction KW - proof_theory AU - Abadi, Martín AU - Gonthier, Georges AU - Werner, Benjamin PY - 2004/// UR - http://www.springerlink.com/content/11m0bcrmg00nrwqv ER -