Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E

                   ______                __    _               
                  / ____/___ _____ ___  / /_  (_)_  ______ ___ 
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/ 

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                          Lundi 28 septembre, 10h30

                                --------------
                                Léo Stefanesco
                                --------------

                                 Inria Paris

    =====================================================================
    Scala Step-by-step: Soundness for DOT with a logical relation in Iris
    =====================================================================


I will present gDOT, a new variant of the Dependent Object Type (DOT)
calculus, and its proof of soundness. DOT is a calculus designed to provide
foundations to the Scala language, and is the basis for Scala 3, whose
soundness has been notoriously difficult to establish. Our approach is to
first give a realizability model using the Iris logic, and then deduce a sound
type system from the model.

This is joint work with Paolo Giarrusso, Amin Timany, Lars Birkedal and
Robbert Krebbers.