kirancodes.me
To Proof Maintenance & Beyond!

The missing link: explaining ELF static linking, semantically

Stephen Kell, Dominic P. Mulligan, Peter Sewell

Abstract

Beneath the surface, software usually depends on complex linker behaviour to work as intended. Even linking hello_world.c is surprisingly involved, and systems software such as libc and operating system kernels rely on a host of linker features. But linking is poorly understood by working programmers and has largely been neglected by language researchers.

Related papers