The talk will be based on joint work with Lê Thành Dũng (Tito) Nguyễn (https://arxiv.org/pdf/2008.01050.pdf).

This work is part of an exploration of the expressiveness of the simply-typed λ-calculus (STLC) and related substructural variants (linear, affine, planar) using Church encodings of datatypes. More specifically, we are interested in the connection with automata theory for string transductions and languages.

After introducing and motivating the problems using Hillebrand and Kanellakis' result stating that the classes of STLC-definable and regular languages coincide, I will discuss refinements we obtained for linear λ-calculi. I will focus on a correspondence with functions computed by copyless streaming string transducers (SSTs), and particularly on the ingredients of a completeness proof translating λ-terms to transducers. This will involve the notions of categorical automata as introduced by Colcombet and Petrisan, categorical models of linear logic and free completions, as well as automata-theoretic techniques related to the composition and determinization of SSTs.

A capability machine is a kind of CPU which supports fine-grained privilege separation using capabilities (a pointer carrying a certain amount of authority). In this talk, I will present a methodology for verifying the functional correctness of capability machine programs that call (or are called by) unknown and potentially malicious code. The key aspects to the approach is a program logic for reasoning about known code, and a logical relation which provides a specification for unknown code. I will then hint at how we extend this methodology to reason about a secure calling convention enforcing a secure stack policy and the well-bracketedness of function calls.

This work has been entirely mechanized in Coq using the Iris framework:

https://github.com/logsem/cerise
https://github.com/logsem/cerise-stack