~~NOCACHE~~
/* DO NOT EDIT THIS FILE             */

[[seminaires:types:index|Théorie des types et réalisabilité]]\\
Mercredi 16 décembre 2020, 14 heures 30, Online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7)\\
**Pierre Pradic** (University of Oxford) //Implicit automata in λ-calculi//
<button type="link" size="xs" collapse="b17-3366">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3366" collapsed="true">
<well size="sm">
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.
</well>
</collapse>


[[seminaires:types:index|Théorie des types et réalisabilité]]\\
Lundi 14 décembre 2020, 14 heures, Online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7)\\
**Armaël Guéneau** (Aarhus University) //Mechanized Program Verification on a Capability Machine in the Presence of Untrusted Code//
<button type="link" size="xs" collapse="b17-3367">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b17-3367" collapsed="true">
<well size="sm">
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
</well>
</collapse>