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
Jan 1, 1400 Comments Off on Participants
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:
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