[TYPES/announce] DICE @ ETAPS 2010: call for participation

[Patrick Baillot]

======================================================
                 Call for participation

                   International  Workshop on
     Developments in Implicit Computational complExity
                           (DICE 2010)

               http://www.ens-lyon.fr/LIP/DICE2010/

         March 27-28, 2010, Paphos, Cyprus
                 as part of ETAPS 2010
======================================================


REGISTRATION

    http://www.etaps10.cs.ucy.ac.cy/

    * normal registration: between February 16 and February 28
    * late registration:   after March 1


PROGRAMME

Saturday, march 27.
===================

  9:30-10:30  (invited talk) A.Ben-Amram. On decidable growth-rate  
properties of imperative programs.

  10:30-11:00 coffee break

  11:00-12:30 U. Dal Lago, S. Martini and M. Zorzi. General Ramified  
Recurrence is Sound for Polynomial Time.
              G. Bonfante. Non confluence in implicit complexity  
characterizations.

  14:00-16:00 M. Lasson. Controlling program extraction in Elementary  
Linear Logic.
              P. Boudes, D. Mazza, L. Tortora de Falco. A Categorical  
Construction for Linear Logic by Levels.
              S. Ronchi Della Rocca. TBA.
              M. Gaboardi, M. Pagani. Can Resource Calculus Be  
Resource Conscious?

  16:00-16:30 coffee break

  16:30-17:30 B. Redmond. PTIME + a distributive law = PSPACE.
              U. Dal Lago, U. Sch ?pp. Experiments on  
logspace-programming with IntML.
                                   o
Sunday, march 28.
=================

  9:30-10:30  (invited talk) S. Martini. Implicit computational  
complexity in the small.

  10:30-11:00 coffee break
              Alois Brunel, K. Terui. Church ? Scott= Ptime: an  
application of resource sensitive realizability.

  11:00-12:30
              L. Roversi, L. Vercelli. Safe Recursion on Notation into  
a light logic by levels.

  14:00-15:00 Y. Zhang, D. Nowak. A calculus for game-based security proofs.
              J.-Y. Marion. Non-interference types and tier recursion.


SCOPE AND TOPIC:

The area of Implicit Computational Complexity (ICC) has grown out from
several proposals to use logic and formal methods to provide languages
for complexity-bounded computation (e.g. Ptime, Logspace
computation). It aims at studying computational complexity without
referring to external measuring conditions or a particular machine
model, but only by considering language restrictions or
logical/computational principles implying complexity properties.

  This workshop focuses on ICC methods related to programs (rather than
descriptive methods).  In this approach one relates complexity classes
to restrictions on programming paradigms (functional programs, lambda
calculi, rewriting systems), such as ramified recurrence, weak
polymorphic types, linear logic and linear types, and interpretative
measures. The two main objectives of this area are:
- to find natural implicit characterizations of various complexity
  classes of functions, thereby illuminating their nature and importance;
- to design methods suitable for static verification of program complexity.
  Therefore  ICC is related on the one hand to the study of complexity
classes, and on the other hand to static program analysis.

The workshop will be open to contributions on various aspects of ICC
including (but not exclusively):
- types for controlling complexity,
- logical systems for implicit computational complexity,
- linear logic,
- semantics of complexity-bounded computation,
- rewriting and termination orderings,
- interpretation-based methods for implicit complexity.
- application of implicit complexity to other programming paradigms
   (e.g. imperative or object-oriented languages)