View: session overviewtalk overviewside by side with other conferences
08:45  FLoC Plenary Talk: From Reachability to Temporal Specifications in Game Theory SPEAKER: Orna Kupfermann ABSTRACT. Multiagents 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 networkformation 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 multiagent games. For example, in networkformation 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. 
10:45  Ramsey Theorem as an intuitionistic property of well founded relations SPEAKER: unknown 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 Hclosure Theorem. Hclosure 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 whileprograms, and was originally proved from the classical Ramsey Theorem, then intuitionistically, but using a intuitionistic version of Ramsey Theorem different from our one. Our longterm goal is to extract effective bounds for the whileprograms from the proof of Termination Theorem, and our new intuitionistic version of Ramsey Theorem is designed for this goal. 
11:15  Termination of Cycle Rewriting SPEAKER: unknown 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. 
11:45  FirstOrder Formative Rules SPEAKER: Cynthia Kop ABSTRACT. This paper discusses the method of formative rules for firstorder rewriting, which was previously defined for a class of higherorder rewriting. Dual to the wellknown 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 higherorder definition, we can obtain significant improvements in the firstorder setting, with or without types. 
12:15  Formalizing monotone algebras for certification of termination and complexity proofs SPEAKER: René Thiemann ABSTRACT. Monotone algebras are frequently utilized to generate reduction orders in automated termination and complexityproofs. 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 nonlinear polynomial interpretations over various domains, including the reals. 
12:45  Nagoya Termination Tool (System Description) SPEAKER: Akihisa Yamada 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. 
14:30  A unified approach to Univalent Foundations and Homotopical Algebra SPEAKER: Nicola Gambino 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 socalled Univalence Axiom, which allows us to treat isomorphic types as if there were equal. Quillen's homotopical algebra, instead, provides a categorytheoretic 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.

15:30  Amortised Resource Analysis and Typed Polynomial Interpretations SPEAKER: unknown ABSTRACT. We introduce a novel resource analysis for typed term rewrite systems based on a potentialbased 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 welltyped, then their exists a polynomial interpretation that orients R. For this we suitable adapt the standard notion of polynomial interpretations to the typed setting. 
16:30  Self Types for Dependently Typed Lambda Encodings SPEAKER: Peng Fu 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 Fomega with positive recursive type definitions, which we analyze. We also prove type preservation for S. 
17:00  The Structural Theory of Pure Type Systems SPEAKER: Floris van Doorn 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 "Qlogic of Pterms'' and Ppoly which intuitively denotes the "predicative polymorphism" extension of P. These results suggest a new approach to the study of the metatheory of PTSs, by examination of the relationships between different calculi and "predicative extensions" which allow more expressiveness with equivalent logical strength. 
17:30  Unnesting of Copatterns SPEAKER: unknown 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 nonnested (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 multistep 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. 
19:00  VSL Public Lecture: Gödel in Vienna SPEAKER: Karl Sigmund 