Workshop on Higher Order Computation:
Types, Complexity, Applications

Institut Henri Poincaré, 16-18 June 2014

In the context of the IHP thematic trimester Semantics of proofs and certified mathematics, we organize an informal workshop on "Higher-order computation: types, complexity, applications", which will be focused on the development of logical and type-based methods for quantitative properties of computation: (implicit) computational complexity, higher-order languages for non-deterministic and probabilistic computation, with their applications to program certification, security, etc.

The idea is to organize a true workshop, focusing primarily on discussing ideas and developing new collaborations, rather than on talks. It is also thought as an occasion to participate to the other events of the IHP trimester. In fact, the workshop falls just after the Semantics of proofs and programs week and just before the Abstraction and Verification in Semantics week. Of the main workshops of the trimester, these are the ones that are thematically closer to the subject of our workshop.

Financial support is provided by the Agence Nationale de la Recherche (ANR), via the Logoi project.

Logistic details

The workshop will be held in Paris, at the Institut Henri Poincaré.

There is no attendance fee.

Coffee breaks will be provided but participants will have to pay for their meals and accommodation.

For lunch, the custom of IHP meetings is to let participants wander off from the Institute and eat in one of the neighboring restaurants.

A few useful links from the IHP website:


Monday, June 16amphi Perrin, Laboratoire de Chimie Physique (just in front of IHP)
9:00-9:45Beniamino Accattoli: Beta-reduction is invariant, indeed
9:45-10:30Ulrich Schöpp: Call-by-Value in a Basic Logic for Interaction
10:30-11:00Coffee break
11:00-11:45Simona Ronchi Della Rocca: Intersection Types and Computational Complexity
11:45-12:30Robin Cockett: Kleene's minimalization as a construction: linking implicit complexity settings to Turing categories
14:00-14:40Marc Bagnol: Unification and Logarithmic space
14:40-15:20Thomas Seiller: Graphings and Complexity
15:20-16:00Damiano Mazza: The infinitary affine lambda-calculus and bounded depth circuits
16:00-16:30Coffee break
16:30-18:00Free discussion
Tuesday, June 17amphi Darboux, IHP
9:00-9:45Norman Danner: Ramified structural recursion and corecursion
9:45-10:30Aleš Bizjak: Step-indexed logical relations for probability
10:30-11:15Jan Hoffmann: End-to-End Verification of Stack-Space Bounds for C Programs
11:15-11:45Coffee break
11:45-12:30Bruce Kapron: Type-2 Polynomial Time and Composability
14:00-16:15Free discussion
16:15-16:45Coffee break
16:45-18:00Free discussion
Wednesday, June 18amphi Darboux, IHP
9:00-9:45Akitoshi Kawamura: Iteration in computable analysis
9:45-10:30Kazushige Terui: Models of linear logic for higher order real computation
10:30-11:15Marco Gaboardi: Type checking linear dependent types for sensitivity
11:15-11:45Coffee break
11:45-12:30Ugo Dal Lago/Patrick Baillot: Subrecursive linear dependent types and computational security
14:00-15:45Free discussion
15:45End of workshop
Financially supported by
Project Logoi


Planned participants: