LOLA 2010: July 9

Syntax and semantics of low level languages

associated with LICS

Overview

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.

Programme

Program Chairs

Nick Benton, Microsoft Research, United Kingdom
Paul-André Melliès, CNRS, France

Program Committee:

Amal Ahmed, Indiana Universtiy, United States
Nick Benton, Microsoft Research, United Kingdom
Lars Birkedal, IT University of Copenhagen, Denmark
Dan Ghica, university of birmingham, United Kingdom
Paul-André Melliès, CNRS, France
Francois Pottier, INRIA, France
Ulrich Schoepp, LMU Munich, Germany
Hayo Thielecke, University of Birmingham, United Kingdom