Syntax and semantics of low level languages
associated with LICS
People realized in the late 1960s that the tools developed in logic and more specifically in proof theory could be smoothly adapted to write better and safer code in high level programming languages. In a sharp contrast, compilation of a high level language into a low level one (typically into machine code) was still considered in the early 1990s as a symbolic process living outside the realm of logic.
Hence, one fundamental discovery of this past decade has been that low level languages are also governed by logical principles. From this key observation emerged a very active and fascinating research area at the frontier of logic and computer science. One main difficulty indeed is to understand what kind of logic should reflect the specific structure of these low level languages, this including pointers, heaps, and registers.
We believe that these developments should go hand in hand with the most advanced contemporary researches in proof theory – in particular topics like classical realizability and forcing, double orthogonality, parametricity, linear logic, game semantics, uniformity, categorical semantics, explicit substitutions, abstract machines, implicit complexity and sublinear programming.
More information can be found here.