LOLA 2018 - Syntax and Semantics of Low-Level Languages (LOLA 2018)

Since the late 1960s it has been known that tools and structures arising in mathematical logic and proof theory can usefully be applied to the design of high-level programming languages, and to the development of reasoning principles for such languages. Yet low-level languages, such as machine code, and the compilation of high-level languages into low-level ones have traditionally been seen as having little or no essential connection to logic.
However, a fundamental discovery of the past two decades has been that low-level languages are also governed by logical principles. From this key observation has emerged an active and fascinating new research area at the frontier of logic and computer science. The practically-motivated design of logics reflecting the structure of low-level languages (such as heaps, registers and code pointers) and low-level properties of programs (such as resource usage) goes hand in hand with some of the most advanced contemporary research in semantics and proof theory, including classical realizability and forcing, double orthogonality, parametricity, linear logic, game semantics, uniformity, categorical semantics, explicit substitutions, abstract machines, implicit complexity and resource bounded programming.
The LOLA workshop, affiliated with LICS at FLoC 2018, will bring together researchers interested in the relationships and connections between logic and low-level languages and programs. Topics of interest include, but are not limited to:
Typed assembly languages
Certified assembly programming
Certified and certifying compilation
Proof-carrying code
Program optimization
Modal logic and realizability in machine code
Realizability and double orthogonality in assembly code
Parametricity, modules and existential types
General references, Kripke models and recursive types
Continuations and concurrency
Resource analysis and implicit complexity
Closures and explicit substitutions
Linear logic and separation logic
Game semantics, abstract machines and hardware synthesis
Monoidal and premonoidal categories, traces and effects