Implicit Computational Complexity and applications: Resource control, security, real-number computation

Icon

NII Shonan Meeting Seminar 033

Organizers

Participants

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

 

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.

Access

See Shonan Village Center website.

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”)

Photos

Photo contributed by Shonan Village Center

Photos contributed by the tour guides

IMG_1155IMG_1158

Photos contributed by Martin Ziegler

0752076307700774077707900791