ABSTRACT. Multi-agents games are extensively used for modelling settings in which different entities share resources. For example, the setting in which entities need to route messages in a network is modelled by network-formation games: the network is modelled by a graph, and each agent has to select a path satisfying his reachability objective. In practice, the objectives of the entities are often more involved than reachability. The need to specify and reason about rich specifications has been extensively studied in the context of verification and synthesis of reactive systems. The talk describes a lifting of ideas from formal methods to multi-agent games. For example, in network-formation games with regular objectives, the edges of the graph are labeled by alphabet letters and the objective of each player is a regular language over the alphabet of labels. Thus, beyond reachability, a player may restrict attention to paths that satisfy certain properties, referring, for example, to the providers of the traversed edges, the actions associated with them, their quality of service, security, etc.

The talk assumes no previous knowledge in game theory. We will introduce the basic concepts and problems, describe how their extension to games with more expressive specification of objectives poses new challenges, and study the resulting games.

Joint work with Guy Avni and Tami Tamir.

ABSTRACT. Ramsey Theorem for pairs is a combinatorial result that cannot be intuitionistically proved. In this paper we present a new form of Ramsey Theorem for pairs we call H-closure Theorem. H-closure is a property of well founded relations, intuitionistically provable, informative, and possibly simpler to use in intuitionistic proofs. Using our intuitionistic version of Ramsey Theorem we intuitionistically prove the Termination Theorem by Poldenski and Rybalchenko. This theorem concerns an algorithm inferring termination for while-programs, and was originally proved from the classical Ramsey Theorem, then intuitionistically, but using a intuitionistic version of Ramsey Theorem different from our one. Our long-term goal is to extract effective bounds for the while-programs from the proof of Termination Theorem, and our new intuitionistic version of Ramsey Theorem is designed for this goal.

ABSTRACT. String rewriting can not only be applied on strings, but also on cycles and even on general graphs. In this paper we investigate ter- mination of string rewriting applied on cycles, shortly denoted as cycle rewriting, which is a strictly stronger requirement than termination on strings. Most techniques for proving termination of string rewriting fail for proving termination of cycle rewriting, but match bounds, arctic ma- trices and tropical matrices can be applied. Further we show how any terminating string rewriting system can be transformed to a terminating cycle rewriting system, preserving derivational complexity.

ABSTRACT. This paper discusses the method of formative rules for first-order rewriting, which was previously defined for a class of higher-order rewriting. Dual to the well-known notion of usable rules, this technique allows for further simplifications of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, we can obtain significant improvements in the first-order setting, with or without types.

ABSTRACT. Monotone algebras are frequently utilized to generate reduction orders in automated termination- and complexity-proofs. To be able to certify these proofs, we formalized several kinds of interpretations in the proof assistant Isabelle/HOL. Here, we report on our integration of matrix interpretations, arctic interpretations, and non-linear polynomial interpretations over various domains, including the reals.

ABSTRACT. This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination analyzer for term rewrite systems. The tool is special for its power due to the implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the deep cooperation with SMT solvers. We present some new ideas that contribute to the efficiency and the power of the tool.

ABSTRACT. Voevodsky's Univalent Foundations of Mathematics programme seeks to develop a new approach to the foundations of mathematics, based on dependent type theories extended with axioms inspired by homotopy theory. The most remarkable of these new axioms is the so-called Univalence Axiom, which allows us to treat isomorphic types as if there were equal. 

Quillen's homotopical algebra, instead, provides a category-theoretic framework in which it is possible to develop an abstract version of homotopy theory, giving a homogeneous account of several situations where objects are identified up to a suitable notion of `weak equivalence'. The central notion here is that of a model category, examples of which arise naturally in several different areas of mathematics. 

The aim of this talk is to explain how the type theories considered in Univalent Foundations and the categorical structures considered in homotopical algebra are different but related, and to describe categorically the common core of Univalent Foundations and homotopical algebra, thus allowing a simoultaneous development of the two subjects. The axiomatisation will be based on work of several authors, including Awodey, van den Berg, Garner, Joyal, Lumsdaine, Shulman and Warren.

ABSTRACT. We introduce a novel resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the runtime complexity. We relate the thus obtained amortised resource analysis to polynomial interpretations and obtain the perhaps surprising result that whenever a rewrite system R can be well-typed, then their exists a polynomial interpretation that orients R. For this we suitable adapt the standard notion of polynomial interpretations to the typed setting.

ABSTRACT. We revisit lambda encodings of data, proposing new solutions to several old problems, in particular dependent elimination with lambda encodings. We start with a type assignment form of the Calculus of Constructions, restricted recursive definitions and Miquel’s implicit product. We add a type construct \iota x . T, called a self type, which allows T to refer to the subject of typing. We show how the resulting System S with this novel form of dependency supports dependent elimination with lambda encodings, including induction principles. Strong normalization of S is established by defining an erasure from S to a version of F-omega with positive recursive type definitions, which we analyze. We also prove type preservation for S.

ABSTRACT. We investigate possible extensions of arbitrary given Pure Type Systems with additional sorts and rules which preserve the normalization property. In particular we identify the following interesting extensions: the disjoint union P+Q of two PTSs P and Q, the PTS ∀P.Q which intuitively captures the "Q-logic of P-terms'' and Ppoly which intuitively denotes the "predicative polymorphism" extension of P.

These results suggest a new approach to the study of the meta-theory of PTSs, by examination of the relationships between different calculi and "predicative extensions" which allow more expressiveness with equivalent logical strength.

ABSTRACT. Inductive data such as finite lists and trees can elegantly be defined by constructors which allow programmers to analyze and manipulate finite data via pattern matching. Dually, coinductive data such as streams can be defined by observations such as head and tail and programmers can synthesize infinite data via copattern matching. This leads to a symmetric language where finite and infinite data can be nested. In this paper, we compile nested pattern and copattern matching into a core language which only supports simple non-nested (co)pattern matching. This core language may serve as an intermediate language of a compiler. We show that this translation is conservative, i.e., the multi-step reduction relation in both languages coincides for terms of the original language. Furthermore, we show that the translation preserves strong normalisation: a term of the original language is strongly normalising in one language if and only if it is so in the other.