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

                           JEUDI 20 février, 14h00

                                 ------------
                                 Eelco Visser
                                 ------------

                        Delft University of Technology

            =====================================================
            Statix: Type Checkers from Declarative Specifications
            =====================================================

In this talk I present the design of Statix, a new constraint-based language
for the executable specification of type systems. Statix specifications
consist of predicates that define the well-formedness of language constructs
in terms of built-in and user-defined constraints. Statix has a declarative
semantics that defines whether a model satisfies a constraint. The operational
semantics of Statix is defined as a sound constraint solving algorithm that
searches for a solution for a constraint. The aim of the design is that Statix
users can ignore the execution order of constraint solving and think in terms
of the declarative semantics.

A distinctive feature of Statix is its use of scope graphs, a language
parametric framework for the representation and querying of the name binding
facts in programs. Since types depend on name resolution and name resolution
may depend on types, it is typically not possible to construct the entire
scope graph of a program before type constraint resolution. In (algorithmic)
type system specifications this leads to explicit ordering of the construction
and querying of the type environment (class table, symbol table). Statix
automatically stages the construction of the scope graph of a program such
that queries are never executed when their answers may be affected by future
scope graph extension. In the talk, I will explain the design of Statix by
means of examples and discuss the distinction between its declarative and
operational semantics.

The design of Statix is based on the following publications:

  Scopes as types.
  Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser.
  PACMPL 2(OOPSLA) 2018 https://doi.org/10.1145/3276484

  A constraint language for static semantic analysis based on scope graphs.
  Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser,
  Guido Wachsmuth. PEPM 2016.

  A Theory of Name Resolution.
  Pierre Néron, Andrew P. Tolmach, Eelco Visser, Guido Wachsmuth.
  ESOP 2015.

Eelco Visser is Professor of Computer Science and chair of the Programming
Languages Group at Delft University of Technology. His current research is on
the foundation and implementation of declarative specification of programming
languages. The results of the research are integrated in the Spoofax Language
Workbench (http://metaborg.org). For more information see
http://eelcovisser.org.