Jan 1, 1500 Comments Off on Organizers

## Organizers

- Akitoshi Kawamura, University of Tokyo, Japan
- Jean-Yves Marion, Lorraine University, France
- David Nowak, JFLI, CNRS & University of Tokyo, France and Japan

Jan 1, 1500 Comments Off on Organizers

- Akitoshi Kawamura, University of Tokyo, Japan
- Jean-Yves Marion, Lorraine University, France
- David Nowak, JFLI, CNRS & University of Tokyo, France and Japan

Jan 1, 1400 Comments Off on Participants

- Roberto Amadio, Department of Computer Science, University Paris Diderot (Paris 7)
- Patrick Baillot, LIP, CNRS & ENS Lyon
- Guillaume Bonfante, LORIA & University of Lorraine
- Olivier Bournez, LIX, École Polytechnique
- Ugo Dal Lago, Department of Computer Science and Engineering, University of Bologna
- Hugo Férée, LORIA & University of Lorraine
- Marco Gaboardi, School of Computing, University of Dundee
- Nao Hirokawa, School of Information Science, Japan Advanced Institute of Science and Technology
- Bruce Kapron, Department of Computer Science, University of Victoria
- Akitoshi Kawamura, Department of Computer Science, University of Tokyo
- Jean-Yves Marion, LORIA & University of Lorraine
- Damiano Mazza, LIPN, University of Paris North (Paris 13)
- Paul-André Melliès, PPS, CNRS & University Paris Diderot (Paris 7)
- Georg Moser, Institute of Computer Science, University of Innsbruck
- Jean-Yves Moyen, LIPN, University of Paris North (Paris 13)
- David Nowak, LIFL, CNRS & Lille 1 University
- Isabel Oitavem, CMAF-UL & FCT-UNL
- Carsten Rösnick, Department of Mathematics, Darmstadt University of Technology
- Jim Royer, Syracuse University
- Ulrich Schöpp, Institute of Computer Science, Ludwig Maximilian University of Munich
- Dieter Spreen,?Department of Mathematics, University of Siegen & Department of Decision Sciences, University of South Africa, Pretoria
- Klaus Weihrauch, Faculty of Mathematics and Computer Science, University of Hagen
- Ning Zhong, Department of Mathematical Sciences, University of Cincinnati
- Martin Ziegler, Department of Mathematics, Darmstadt University of Technology &?JSPS BRIDGE program

Jan 1, 1300 Comments Off on Overview

Computational complexity theory aims at classifying computational problems according to their inherent difficulty. The standard way to achieve this classification consists in formalizing a precise execution model (e.g., a Turing machine) and posing explicit bounds on time and memory resources. On the other hand, Implicit Computational Complexity (ICC) 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. The area of ICC has grown out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g., polynomial time, logarithmic space computation). ICC methods include, among others, linear logic, typed programming language, second order logic, term ordering. The last decades have seen the development of logical formalisms that characterize functions computable in various complexity classes (polynomial or elementary in time, logarithmic in space).

The goal of the proposed meeting is to explore foundational as well as practical interconnections between formal logic and computational complexity, such as it is done in ICC. The main outcome of this meeting will be to trigger new interactions and enrich the various approaches. In particular, and aside from traditional ICC approaches, we would like to focus on computation involving real numbers and topological spaces, thereby providing a deeper understanding of computational complexity in non-discrete realms of mathematics. By bringing together experts in implicit complexity and in complexity in analysis, we will promote new interaction between the two fields. People in those two fields are currently working separately, but there is enough common ground between them to make it worth having those two communities talking and working together. The meeting would also foster discussions about applications, i.e., the design of methods based on ICC and suitable for static verification of program resource consumption and of security.

Research topics for discussion on the various aspects described above would include, among others, the following topics:

- types for controlling complexity
- logical systems for computational complexity
- linear logic
- semantics of complexity-bounded computation
- rewriting and termination orderings
- interpretation-based methods for implicit complexity
- programming languages for complexity-bounded computation
- application of implicit complexity to the analysis of resource consumption
- application of implicit complexity to security
- complexity over reals and non-discrete spaces
- type-two complexity
- resource bounds in computable analysis and algorithmic randomness
- analog and continuous-time computation
- theory and implementation of efficient validated numerical algorithms

We briefly describe below two topics that we would like to promote. Although they originate from two different communities, they share the same interest in implicit characterization of complexity and they both have applications to formal validation of computer systems.

Very recently ICC methods have been applied to security methods and conversely security methods have been used as a new approach in ICC context. In the context of security proofs, the computational power of adversaries has to be limited so that their potential attacks are feasible. An adversary with unlimited computational power could indeed break most cryptographic schemes (e.g., RSA by efficiently factoring large integers). It is usual to rely on Cobham’s thesis identifying feasibility with computability in polynomial time. Hence the particular interest in the class of functions computable in polynomial time and its implicit characterization with a programming language that can be used to construct adversaries. Conversely, type systems to control the information flow, which are traditionally used for certifying security policies like confidentiality or integrity, are related to the notion of data stratification. As a result, type systems for imperative programming languages have been developed to control resource consumption.

The other proposed focus is on computation over the reals. Computable analysis, the study of abilities and limitations of digital computers applied to problems in mathematical analysis, has originally evolved from computability theory, but there is increasing interest in computational complexity with bounded time and space. The goals here are to analyze the computational costs of algorithms for problems involving real numbers and to explore the principles and structures of computational complexity in this context, providing a foundation of validated numerical methods for problems arising in physical sciences and engineering. Broader perspectives in computational complexity, including those from implicit complexity theory, have high potential to help here, as can be already seen, for example, in recent studies of computational power of dynamical systems and analog computers, or in the application of type-two complexity theory to time-bounded computable analysis.

Jan 1, 1100 Comments Off on Program

**November 3rd (Sunday)**

15:00~19:00 Hotel check-in (early check-in from 12:00 is possible)

19:00~21:00 Welcome Banquet

**November 4th (Monday)**

07:30~09:00 Breakfast (Cafetaria “Oak”)

09:00~09:10 Introduction of NII Shonan Meeting

09:10~12:00 Session 1:

Patrick Baillot

An introduction to light logics, or Implicit complexity by taming the duplication (Introductory talk on ICC)

Jean-Yves Moyen

*Interpretation methods in ICC*?(Introductory talk on ICC)

12:00~13:30 Lunch (Cafetaria “Oak”)

13:30~14:00 Group photo shooting

14:00~18:00 Session 2:

Martin Ziegler

Real complexity theory: a numerical view on “P vs. NP”?(Introductory talk on complexity in analysis)

Akitoshi Kawamura

*Type-two complexity classes in computable analysis*?(Introductory talk on complexity in analysis)

Carsten Rösnick

*About representations of and operators on subsets of R^d*

Hugo Férée

*Higher order complexity and application in computable analysis*

18:00~19:30 Dinner (Cafetaria “Oak”)

**November 5th (Tuesday)**

07:30~09:00 Breakfast (Cafetaria “Oak”)

09:00~12:20 Session 3

Roberto Amadio (joint work with Yann Régis-Gianas)

*Certifying and reasoning about cost annotations of functional programs*

Olivier Bournez

*On the complexity of solving ordinary differential equations. Towards a complexity theory for the General Purpose Analog Computer of Claude Shannon*

Isabel Oitavem

*Recursion schemes for P, NP and Pspace*

Klaus Weihrauch (joint work with Robert Rettinger)

*Products of effective topological spaces and a uniformly computable Tychonoff Theorem*

12:20~13:30 Lunch (Cafetaria “Oak”)

13:30~18:30 Session 4

Patrick Baillot

*Characterizing polynomial and exponential complexity classes in elementary lambda-calculus*

Georg Moser (joint work with Martin Hofmann)

*Amortised resource analysis and typed term rewriting*

Jim Royer (joint work with Norman Danner)

*Ramified structural recursion and corecursion*

Ulrich Schöpp

*Towards a primitive logic for computation by interaction*

Jean-Yves Moyen (joint work with Guillaume Bonfante and Pierre Boudes)

*Expressive power and algorithms*

Bruce Kapron

*Computational soundness of symbolic security and implicit complexity*

18:30~19:30 Dinner (Cafetaria “Oak”)

**November 6th (Wednesday)**

07:30~09:00 Breakfast (Cafetaria “Oak”)

09:00~12:30 Session 5

Ugo Dal Lago

*Infinitary lambda calculi from a linear viewpoint*

Marco Gaboardi

*Differential privacy: a type-based approach*

Nao Hirokawa

*Leftmost outermost and innermost strategies*

Dieter Spreen

*The continuity problem, once again*

Martin Ziegler (joint work with Akitoshi Kawamura and Florian Steinberg)

*The computational complexity of Laplace’s equation*

12:30~13:30 Lunch (Cafetaria “Oak”)

13:30~19:00 Excursion (Kamakura)

18:00~20:00 Main banquet

**November 7th (Thursday)**

07:00~10:00 Check-out

07:30~09:00 Breakfast (Cafetaria “Oak”)

09:00~12:30 Session 6

Damiano Mazza

*Infinitary lambda calculi and computational complexity*

Guillaume Bonfante (joint work with?Reinhard Kahle, Jean-Yves Marion?and Isabel Oitavem)

*Characterizing NC^k: from words to trees and back to words*

Paul-André Melliès

*Duplication and sharing in tensorial logic*

David Nowak (joint work with Sylvain Heraud and Yu Zhang)

*Formal Security Proofs with ICC*

Jean-Yves Marion (joint work with Daniel Leivant)

*Evolving graph structures, non-interference, and complexity*

12:30~13:30 Lunch (Cafetaria “Oak”)

Jan 1, 1000 Comments Off on Photos