Paper Info
Title
Choice in Dynamic Linking
Abstract
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.
Year
DOI
Venue
2004
10.1007/978-3-540-24727-2_3
LECTURE NOTES IN COMPUTER SCIENCE
Keywords
Field
DocType
operational semantics,programming language,proof theory,software systems
Operational semantics,Computer science,Proof theory,Theoretical computer science,Software system,Operator (computer programming),Artificial intelligence,Software architecture,Type variable,Software development,Distributed computing,Special case
Conference
Volume
ISSN
Citations 
2987
0302-9743
7
PageRank 
References 
Authors
0.52
13
3
Name
Order
Citations
PageRank
Martín Abadi1120741324.31
Georges Gonthier22275195.06
Benjamin Werner328922.50