Séminaire Cambium, Inria Paris
                                  Salle BJ09
                           Lundi 14 octobre, 10h30

                                Denis Carnier
                                  KU Leuven

                            Type Inference Logics

Type inference is essential for statically typed languages such as
OCaml and Haskell. It can be decomposed into two (possibly
interleaved) phases: a generator converts programs to constraints; a
solver decides whether a constraint is satisfiable. Elaboration, the
task of decorating a program with explicit type annotations, can also
be structured in this way. Unfortunately, most machine-checked
implementations of type inference do not follow this phase-separated,
constraint-based approach. Those that do are rarely executable, lack
effectful abstractions, and do not include elaboration.

To close the gap between common practice in real-world implementations
and mechanizations inside proof assistants, we propose an approach
that enables modular reasoning about monadic constraint generation in
the presence of elaboration. Our approach includes a domain-specific
base logic for reasoning about metavariables and a program logic that
allows us to reason abstractly about the meaning of constraints. To
evaluate it, we report on a machine-checked implementation of our
techniques inside the Coq proof assistant. As a case study, we verify
both soundness and completeness for three elaborating type inferencers
for the simply typed 𝜆-calculus with Booleans. Our results are the
first demonstration that type inference algorithms can be verified in
the same form as they are implemented in practice: in an imperative
style, modularly decomposed into constraint generation and solving,
and delivering elaborated terms to the remainder of the compiler
chain.

This is joint work with Steven Keuchel and François Pottier.

            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.