It has been understood since the late 1960s 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 a low level ones have traditionally been seen as having little or no essential connection to logic.
However, a fundamental discovery of this past decade 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 the some of the most advanced contemporary researches 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 sublinear programming.
Game semantics has been developed since the 90's as a denotational paradigm capturing observational equivalence of functional languages with imperative features. While initially introduced for PCF variants, the theory can nowadays express real-life languages ranging from ML fragments and Java programs to C-like code. In this talk we present recent advances in devising game models for effectful computation, and describe an emerging correspondence with trace models which departs from the denotational view of games towards a more low-level, operational one.
SML# is a variant of Standard ML being developed at RIEC, Tohoku University. One of its goal is to provide an ML-style language equipped with system programming functionalities found in C including direct invocation of system service libraries, native multithread support, and true separate compilation on modern multi-core platforms. To achieve this, the SML# compiler generates native codes that are compatible with those produced by C. Its major challenge has been to compile polymorphic functions to low-level codes that embodies their polymorphic behavior. To meet this challenge, we have developed a series of compilation techniques, including bitmap compilation for unboxed data structures and type-directed dynamic calling convention selection. With these techniques, the SML# compiler generates LLVM-IR code for the x64 platform. In this talk, I will introduce the SML# features through examples, describe the code generation phases of the SML# compiler backend, and outline our technical developments underlying the code generation.
The LOLA workshop, affiliated with LICS, will bring together researchers interested in many aspects of the relationship between logic and low level languages and programs. Topics of interest include, but are not limited to:
LOLA is an informal workshop aiming at a high degree of useful interaction amongst the participants, welcoming proposals for talks on work in progress, overviews of larger programmes, position presentations and short tutorials as well as more traditional research talks describing new results. The programme committee will select the workshop presentations from submitted proposals, which may take the form either of a two page abstract or of a longer (published or unpublished) paper describing completed work.
Authors are invited to submit an abstract to the LOLA 2015 EasyChair page.