Room 206 (2nd floor, badged access)
11 December 2025 - 14h00
Compiling types and other high-level language features for performance or security
by Thaïs Baudon from University of Kent (UK)
Abstract: The first part of this talk will present the Ribbit language and compiler, which aim to combine the convenience and safety of Algebraic Data Types (ADTs) with the fine control over memory representation required in high-performance applications. ADTs provide nice data abstractions and an elegant way to express functions through pattern matching. Unfortunately, ADTs remain seldom used in low-level programming. One reason is that their increased convenience comes at the cost of abstracting away the exact memory layout of values, whereas high-performance applications often require finely optimised, custom memory representations. Ribbit lets programmers specify custom memory layouts for ADTs in a flexible and expressive way, while still enjoying high-level programming constructs (pattern matching) to manipulate this data.
Since the compilation of high-level language constructs is heavily influenced by memory representation, traditional pattern matching compilation approaches, which are geared towards a rather uniform data layout, are not suitable for compiling Ribbit programs, for which data layout is arbitrarily complex and variable. Aside from pattern matching, even compiling simple expressions becomes particularly challenging when data pieces are broken and scattered in memory (as with many low-level representations such as network packets, instruction sets, etc.). To address this, we propose a compilation algorithm for Ribbit providing full synthesis of bijections between different memory types. Our compilation algorithms are proven correct and implemented in the Ribbit compiler prototype.
The second part of this talk will cover work on secure compilation of the Declassification Core Calculus (DeCC) [1], a recent modal type theory for reasoning about rich security properties with deliberate information disclosure, a.k.a. declassification. In this work, we look at the problem of compiling DeCC to a calculus with nonmodal information flow types which only supports vanilla noninterference (and no declassification). We show that our compilation preserves both types and semantics. Additionally, we also show that relaxed semantic declassification (soundness criteria for the source, DeCC) can be recovered from noninterference (soundness criteria of the target), along with additional properties of our compilation scheme. This work is being mechanized in the HOL4 theorem prover.
[1] V. Rajani, A. Coleman and H. Kanabar, A Graded Modal Approach to Relaxed Semantic Declassification,
in 2025 IEEE 38th Computer Security Foundations Symposium (CSF), Santa Cruz, CA, USA, 2025, pp. 268-283, doi: 10.1109/CSF64896.2025.00032
Candidate potentielle au concours CR CNRS
