Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                           Vendredi 12 avril, 10h30

                                  Irene Yoon
                                 Inria Paris

                 Modular and executable semantics for LLVM IR

LLVM is an industrial-strength compiler framework (used in Apple's iOS
development tools) and a popular research tool (winning the ACM Software
Systems Award in 2012).

The core of LLVM is an intermediate representation (IR) equipped with
various analysis and optimization passes, and is the target of a broad range
of front-ends (such as C/C++/Objective C, Rust, Haskell, Ruby, and
JavaScript) and backends (such as x86-64, ARM, and WebAssembly).

This talk is an introduction to a formal semantics of Vellvm (Verified
LLVM), which models a large, sequential subset of the LLVM IR, mechanized in
the Coq proof assistant.

In contrast to previous approaches which use relationally-specified
operational semantics, this semantics is based on monadic interpretation of
Interaction Trees, a data structure that provides a compositional approach
to defining language semantics while retaining the ability to extract an
executable interpreter. We will discuss how we model some subtleties in the
LLVM IR semantics in a modular way via composing monadic interpreters, and
how this semantics admits compositional reasoning principles derived from
the equational theory of Interaction Trees.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.