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

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                          Lundi 6 décembre, 10h30

                               --------------
                               Martin Hofmann
                               --------------

                                    LMU

         ==========================================================
         Automatic amortised resource inference for class-based OOP
         ==========================================================

We describe a type system for the discovery of static bounds on resource
usage of class-based object-oriented programs. The type system is based on
amortised analysis: the types define a potential function mapping heap
configurations to nonnegative numbers. The typing rules are such that the
potential of a pre-heap (before execution) is always greater or equal to
the potential of the post-heap plus the actual resource consumption. Thus,
the potential of the initial heap furnishes an upper bound on the total
resource consumption.

The type system and its soundness date back to 2006 (ESOP) and 2009 (CSL).
We now tackle type inference using a constraint-based approach. There are
still some sticky points which I will explain during the talk. So some
parts of what I will present are still work in progress.

This is joint work with Dulma Rodriguez.