Jan 22, 2018 Comments Off on Organizers

## Organizers

Roberto Giacobazzi (U. of Verona and IMDEA SW Institute)

Dusko Pavlovic (U. of Hawaii)

Tachio Terauchi (Waseda University)

Jan 22, 2018 Comments Off on Organizers

Roberto Giacobazzi (U. of Verona and IMDEA SW Institute)

Dusko Pavlovic (U. of Hawaii)

Tachio Terauchi (Waseda University)

Jan 22, 2018 Comments Off on Participants

The (*) mark means a planned talk

Dr. | Sebastien | Bardin | CEA (French Alternative Energies and Atomic Energy Commission) |

Prof. | Roberto | Bruni (*) | University of Pisa |

Prof. | Silvia | Ghilezan (*) | University of Novi Sad |

Prof. | Roberto | Giacobazzi (*) | University of Verona and IMDEA SW Institute |

Prof. | Roberta | Gori | University of Pisa |

Dr. | Chris | Heunen (*) | University of Edinburgh |

Prof. | Nao | Hirokawa (*) | JAIST |

Prof. | Martin | Hoffmann (*) | University of Munchen |

Dr. | Amar | Hadzihasanovic (*) | Kyoto University |

Prof. | Barry | Jay (*) | School of Software / University of Technology Sydney |

Prof. | Neil | Jones (*) | Cornell University |

Prof. | Bruce | Kapron (*) | University of Victoria |

Dr. | Alex | Kissinger (*) | Radboud University Nijmegen |

Prof. | Jean-Yves | Marion (*) | Nancy University |

Prof. | Simone | Martini (*) | University of Bologna |

Prof. | Stefan | Milius (*) | Friedrich-Alexander Universität Erlangen-Nürnberg |

Prof. | Ugo | Montanari (*) | University of Pisa |

Prof. | Mizuhito | Ogawa | JAIST |

Prof. | Dusko | Pavlovic (*) | University of Hawaii at Manoa |

Prof. | Xavier | Rival (*) | INRIA |

Prof. | Andre | Scedrov (*) | University of Pennsylvania |

Prof. | Tachio | Terauchi (*) | Waseda University |

Prof. | Martin | Ziegler | KAIST |

Jan 22, 2018 Comments Off on Overview

Models of computation branched into **extensional** and **intensional** in 1936, almost as soon as they were invented: Alonzo Church’s negative solution of the *Entscheidungsproblem* was based on his lambda calculus, whereas Alan Turing’s solution was based on his machines. For Church, function abstraction was given as a basic operation, the lambda abstraction. For Turing, program abstraction was a process of constructing a machine for some required function, and then describing that machine as a program to be fed to a universal machine. There are, of course, many different machines implementing the same function, and many different programs describing the same machine to different universal machines. So there are many programs for every function; in fact infinitely many. Much later, the binary relation identifying the programs that describe the same set-theoretic function came to be called the *extensional equivalence*. The terminology goes back to Hermann Grassmann, who construed sets as the *extensions* of mathematical objects. On the other hand, theory and practice of computation where the differences between the various algorithms or programs that implement the same function do matter (e.g. because some take longer time, or require longer programs) came to be called *intensional*. The term goes to Grassman again, but the meaning that he assigned to it was different from the present use.

The simple distinction between the extensional and the intensional views of computation is thus that in the extensional view there is a single program for each function, whereas in the intensional view there are many. To add a wrinkle, Alonzo Church initially did not impose on his abstraction operation the conversion rule that precludes the possibility that, besides the lambda-abstraction of a function, there might be other lambda terms whose applications yield the same function. The *extensionality* rule that identifies all such terms was imposed later, leading to what is now known as the *extensional lambda calculus*. The *non-extensional lambda calculus*, lacking the extensionality rule, is sometimes used as a model of intensional computation. While such uses are surely justified by the interesting results that they make possible, the mere presence of an operation that selects an abstraction, albeit one among many, factors out many intensional properties. A sequence of results from 1980s (Scott, Koymans, Hayashi…) shows that this is unavoidable, since every non-extensional model contains an extensional model as a computable retract. On the other hand, identifying the extensionally equivalent programs is, of course, not computable in general.

But just like lambda calculus factors out the intensional properties of computations, the intensional models factor out the extensional properties. Which extensional properties of computations can be recognized on the corresponding programs? Only the trivial ones, says Rice’s Theorem, assuming that “recognized” is taken to mean “decided”. Only the finitely approximable ones, say the theorems by Myhill-Shepherdson, Rice-Shapiro, and Kreisel-Lacombe-Schoenfield, assuming that “recognized” is taken to mean “computable”.

Hence the gap between the extensional and intensional models of computation: **neither subsumes the other**. Hence the schism between the Western and the Eastern Theory of Computation: algorithmics vs semantics — as diagnosed by Yuri Gurevich in the mid 1990s.

A schism is not necessarily a bad thing. Scott’s domain theory used the negative result that computable extensional properties must be finitely approximable as a fulcrum to lift the world of denotational semantics of programming languages. Cousot’s abstract interpretation extended it further into extensional semantics of programs. On the other hand, the problems of capturing the intensional properties, like time complexity or precision of program analysis and verification, in extensional models, generated solutions that enriched both sides of the gap, both technically, and conceptually.

Yet the bridge has not been built. Program semantics is still high level and abstract, algorithmics is still low level, and very concrete. Is this the way it should be, or are we missing something by keeping the Church-Turing legacies so far apart?

Jan 22, 2018 Comments Off on Schedule

**Monday, Jan. 22 (Theory)**

**09:00 – 09:15 Introduction**- 09:15 – 10:00 Neil:
*Intensions, extensions and game semantics* - 10:00 – 10:30 Dusko:
*Intensional and extensional computations* **10:30 – 11:00 Break**- 11:00 – 11:30 Simone:
*A mathematical theory of computation — the big theoretical synthesis of the early sixties* - 11:30 – 12:00 Barry:
*Beyond Lambda-Calculus: Intensional Computation* **12:00 – 14:00 Lunch**- 14:00 – 15:30 Nao:
*Basic Normalization* - 14:30 – 15:00 Silvia:
*Preciseness of Subtyping: from extensional to intensional aspects* - 15:00 – 15:30 Jean-Yves:
*A “theory” of reflexive computation based on soft intuitionistic logic* **15:30 – 16:00 Break**- 16:00 – 16:30 Bruce:
*Query-restricted oracle polynomial time* **16:30 – 17:30 Discussion of day 1**

**Tuesday, Jan. 23 (Analysis, Verification and Models)**

- 09:00 – 09:30 Roberto G:
*Intensional Aspects in**Program Analysis* - 09:30 – 10:00 Xavier:
*Semantic Directed Clumping of Disjunctive Abstract States* - 10:00 – 10:30 Sebastien:
*Formal methods: from source-level safety to binary-level security* **10:30 – 11:00 Break**- 11:00 – 11:30 Tachio:
*Compositional synthesis of leakage resilient programs* **12:00 – 14:00 Lunch**- 14:00 – 15:30 Roberto B:
*Code Obfuscation Against Abstract Model Checking Attacks* - 14:30 – 15:00 Martin Z:
*Formal Verification in Imperative Multivalued Programming over Continuous Data Types* - 15:00 – 15:30 Chris:
*Tensor topology* **15:30 – 16:00 Break**- 16:00 – 16:30 Aleks:
*Causal structure for black-box processes* - 16:30 – 17:00 Amar:
*Bringing compositionality to rewriting theory via polygraphs* **17:00 – 18:00 Discussion of day 2**

- 09:00 – 09:30 Ugo M:
*Decomposition Structures for Soft Constraint Evaluation Problems* - 09:30 – 10:00 Roberto B:
*Branching Cell Decomposition, Confusion Freeness and Probabilistic Nets* - 10:00 – 10:30 Andre:
*Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems* **10:30 – 11:00 Break**- 11:00 – 11:30 Stefan:
*Efficient Coalgebraic Partition Refinement* **11:30 – 12:00 Discussion day 3****12:00 – 13:30 Lunch****13:30 – 19:00 Excursion****19:00 – 21:30 Banquet**

- 9:00 – 10:30 Open slots for new ideas
**10:30-11:00 Break**- 11:00 – 12:00 Closing
**12:00 – 13:30 Lunch**