@comment{{This file has been generated by bib2bib 1.96}}

@comment{{Command line: /usr/bin/bib2bib -c topic:"linksem" -ob topic.linksem.bib sewellbib2.bib}}

@inproceedings{kell_missing_2016,
author = {Stephen Kell and Dominic P. Mulligan and Peter Sewell},
conf = {OOPSLA 2016},
booktitle = {Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
series = {OOPSLA 2016},
year = {2016},
month = nov,
location = {Amsterdam, The Netherlands},
numpages = {17},
publisher = {ACM},
address = {New York, NY, USA},
abstract = {Beneath the surface, software usually depends on complex \emph{linker
behaviour} to work as intended.  Even linking
\texttt{hello\_world.c} is surprisingly involved, and systems software
such as \texttt{libc} and operating system kernels rely on a host of
programmers and has largely been neglected by language researchers.

In this paper we survey the many use-cases that linkers support and
the poorly specified \emph{linker speak} by which they are controlled:
language.  We provide the first validated formalisation of a realistic
executable and linkable format (ELF), and capture aspects of the
Application Binary Interfaces for four mainstream platforms (AArch64,
AMD64, Power64, and IA32).  Using these, we develop an executable
small C programs (we use the example of \textsf{bzip2}) into a correctly
running executable.  We
provide our specification in Lem and Isabelle/HOL forms.  This is the
first formal specification of mainstream linking.  We have used the
Isabelle/HOL version to prove a sample
correctness property for one case of AMD64 ABI relocation,
demonstrating that the specification supports formal proof, and as a
first step towards the much more ambitious goal of verified linking.
Our work should enable several novel strands of research, including
linker-aware verified compilation and program analysis, and better