An important problem in theoretical computer science is to determine whether two programs are equivalent. For instance, this is needed to determine whether the optimizations performed by a compiler actually preserve the meaning of the input programs. For lambda calculi, it has become standard to consider two programs as equivalent whenever they can be plugged in any context without noticing any difference in their behavior. Such notion of equivalence depends on the behavior one is interested in observing. We provide syntactic and semantic characterizations of the equivalence arising by taking as observables the beta normal forms, corresponding to completely defined values. As a byproduct we obtain characterizations of the different degrees of extensionality in the theory of Böhm trees.

We present ReLoC: a logic for proving refinements of programs in a language with higher-order state, fine-grained concurrency, poly- morphism and recursive types. The core of our logic is a judgement e ≾ e' : τ, which expresses that a program e refines a program e' at type τ. In contrast to earlier work on refinements for languages with higher-order state and concurrency, ReLoC provides type- and structure-directed rules for manipulating this judgement, whereas previously, such proofs were carried out by unfolding the judgement into its definition in the model. These more abstract proof rules make it simpler to carry out refinement proofs. Moreover, we introduce logically atomic relational specifications: a novel approach for relational specifications for compound expressions that take effect at a single instant in time. We demonstrate how to formalise and prove such relational specifications in ReLoC, allowing for more modular proofs. ReLoC is built on top of the expressive concurrent separation logic Iris, allowing us to leverage features of Iris such as invariants and ghost state. We provide a mechanisation of our logic in Coq, which does not just contain a proof of soundness, but also tactics for interactively carrying out refinements proofs. We have used these tactics to mechanise several examples, which demonstrates the practicality and modularity of our logic.

In Chapter 5 of Henning’s thesis, we find a formulation of coinductive variant of first-order intuitionistic logic, named FOL▶. This logic is suggested as a suitable framework for proofs of equality (bisimulation) between infinite streams. The core of this coinductive extension is the Löb rule, originating in the provability logic.

At the same time, my PhD student Yue Li and I have recently proposed a coinductive extension to uniform proofs. Uniform proofs, too, are known for being a fragment of intuitionistic logic. They are a family of proof calculi formulated by Dale Miller et al. for proofs in Horn clause / Hereditary Harrop clause logics. Similarly to Henning’s logic FOL▶, our coinductive extension is based upon one additional coinductive rule COFIX (that however, differs from the Löb rule). Again in line with Henning’s thesis, the motivation behind the coinductive uniform proofs is to provide a general proof-theoretic framework for proofs of coinductive properties of theories (in our case, expressed in Horn Clause logic).

In this talk, I will show connections between these two recently proposed logics; and in particular I will compare the properties of the Löb rule of Henning’s logic and the COFIX rule of the coinductive uniform proofs.

Quantitative typing generalizes ordinary, linear and affine typing and well-known program analyses such as strictness and dead code detection. Recently, Conor McBride and Bob Atkey have each presented dependent quantitative type theories that properly integrate linearity and dependency. In this talk, I will present my own version of quantitative type theory and discuss its semantics. I will also touch on potential applications, such as free theorems from linearity. This is very much work in progress.

Much recent work in type theory, and in homotopy type theory (HoTT) especially, concerns equality. Martin-Löf’s Type Theory has two kinds of equality: judgmental (also: definitional) and propositional. HoTT starts from a novel interpretation of propositional equality as a space of paths and has lead to a much better understanding of propositional equality. In this talk I will argue that one thing that recent work in HoTT has shown, is that it is feasible to completely eliminate judgmental equality in favour of propositional equality and state all computation rule as propositional equalities. In this talk, I wish to present such a purely propositional type theory, reminiscent of “A Logical Framework with Explicit Conversions” by Geuvers and Wiedijk, and discuss its properties (some of which will probably still be in the form of conjectures, as this is still very much work in progress).

In this talk, I will give a brief overview over what the status of mixed inductive-coinductive reasoning is, what we are able to do with ease and what we should be able to do. Just like my thesis, this overview will focus on properties that shall be automatically verified by computers, like static correctness properties of programs and the correctness of mathematical proofs.

One can view the simple types (from the simply typed λ calculus) and their inhabitants not only as propositions and their proofs, but also—and perhaps more interestingly—as data types and their instances. Indeed, while given a ground type 0 the type (0→0)→(0→0) offers a rather trivial proposition, its inhabitants—being the Church-numerals λfx.x, λfx.fx, λfx.ffx, λfx.fffx, … (up to βη-equivalence)—represent the natural numbers. Other examples include:

(0→(0→0))→(0→0) —  binary trees
(0→0)→((0→0)→(0→0)) — words over a two-letter alphabet
(((0→0)→0)→0)→(0→0)  — ~ words over a countable alphabet
0 — the empty set
0→0 — a one-element set
0→(0→0) — a two-element set
0→(0→(0→0)) — a three-element set
...

In fact, this exhausts all possible examples in the following sense. If we say that type A *reduces* to a type B when there is a λ-definable injection from (the set of inhabitants of) A to B, and that A and B are *equivalent* when A reduces to B and B reduces to A, then every type A built from → and a single ground type 0 is equivalent to one of the countably many canonical types mentioned above. Moreover, no two of these canonical types are equivalent, but instead they form a chain of order type ω+3 with the binary trees, (0→(0→0))→(0→0), on top and the empty set, 0, at the bottom.

These facts are part of Statman’s Hierarchy Theorem for which we've recently published a new proof. In this talk I’ll show some of the tricks we used to create our constructive, shorter, and more direct proof.

Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. Up until now, a description of the free model that corresponds to the CKA axioms was missing. Using a fixpoint construction, we show that the free model of the fragment of CKA with bounded parallelism consists of pomset languages that are downward-closed under the subsumption (linearisation) order.

A graph is represented by a word over the set of nodes if there is an edge from u to v if and only in the word restricted to the symbols u,v, these symbols alternate. Many graphs can be represented in this way, but not all. SMT solving shows to be powerful to find a representing word for a given graph. We give some equivalent characterizations, show how to encode the properties in SMT and present some new results and open problems.

We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type F(A) of ``finite sets over type A’' à la Kuratowski without assuming that A has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.
On the foundational side, we use F to define the notions of ``Kuratowski-finite type'' and ``Kuratowski-finite subobject'', which we contrast with established notions, e.g. Bishop-finite types and enumerated types. We argue that Kuratowski-finiteness is the most general and flexible one of those and we define the usual operations on finite types and subobjects.
From the computational perspective, we show how to use F(A) for an abstract interface for well-known finite set implementations such as tree- and list-like data structures. This implies that a function defined on a concrete finite sets implementation can be obtained from a function defined on the abstract finite sets F(A) and that correctness properties are inherited. Hence, HoTT is the ideal setting for data refinement. Beside this, we define bounded quantification, which lifts a decidable property on A to one on F(A).

Syntaxes with binding are omnipresent in Programming Languages research but also in the more practical setting of Embedded Domain Specific Languages. The advanced features available in some languages' type systems has made it possible to statically enforce well-scopedness and sometimes even well-typedness. However the user still has to write a lot of boilerplate code to get common scope-and-type safe programs (e.g. renaming, substitution, normalisation by evaluation, or various compilation passes) and the proofs that they are well-behaved.
Building on an abstract but nonetheless expressive notion of semantics and a universe of syntaxes with binding, we demonstrate how to implement these traversals once and for all by generic programming, and how to derive their properties by generic proving. All of this work has been fully formalised in Agda and is available on github at generic-syntax.

Arrays and streams seem to be fundamentally at odds: arrays require their size to be known in advance, streams are dynamically growing; arrays offer direct access to all of their elements, streams provide direct access to the front elements only; the list goes on. Despite these differences, many computational problems at some point require shifting from one paradigm to the other. The driving forces for such a shift can be manifold. Typically, it is a shift in the task requirements at hand or it is motivated by efficiency considerations. In this talk, we present a basis for a unified framework for dealing with arrays and streams alike. We introduce an applied lambda calculus whose fundamental data structure is a new form of array, named "Transfinite Array". Transfinite arrays maintain properties from finite array calculi yet incorporate support for infinite arrays. As it turns out, it is even possible to maintain recursive specifications as they are typically found in a traditional stream / list-based setting.

We show that all higher inductive types can be constructed from coequalizers, path coequalizers and homotopy colimits. The proof is inspired by Adámek's theorem which constructs inductive types as a colimit of a functor. This way one can reason about all higher inductive types by instead studying a small number of examples. This is joint work with Andrej Bauer.

In this talk, I will present a logic the behavioural equivalence of inductive-coinductive programs. Crucially, the logic's proof system features no explicit induction nor coinduction principle. Instead, equivalences can be proven in that proof system by recursive proofs, that is, by proofs that may refer to themselves. However, we need to restrict the use of such references, since arbitrary self-references would temper with the soundness of the proof system. In the presented system, this will be achieved by using the so-called later modality. A crucial difference to cyclic proof systems is that the later modality gives rise to a local correctness condition, that is, every application of a proof rule produces only a correct proof tree with valid back-references. This enables simple proof checking and allows for a compositional soundness proof, as I will demonstrate. As the logic is tailored for reasoning about programs in the copattern calculus by Abel et al., I will briefly introduce this calculus. Building on this, we can motivate and introduce the logic, and demonstrate its use on some examples.

Parser combinator libraries represent parsers as functions and, using higher-order functions, define a DSL of combinators allowing users to quickly put together programs capable of handling complex grammars. When moving to total functional languages such as Agda, these programs cannot be directly ported: there is nothing in the original definitions guaranteeing termination.

In this talk, we will introduce a 'guarded' modal operator acting on types and show how it allows us to give more precise types to existing combinators thus guaranteeing totality.

The resulting library is available online together with various usage examples at https://github.com/gallais/agdarsec .

Sometimes you run into a situation where you are not entirely happy with a model, but it is difficult to explain why. I had this problem when introducing (in 2002) hybrid transition systems as a semantic model for the behavior of cyber physical systems. It worked, but I thought it was terribly inelegant. Somewhere in the last six years, I have slowly figured out a different approach to dealing with the mix of continuous and discrete behavior, which I would like to share with you. Instead of 'combining' modeling elements from the discrete and the continuous world, I have been focusing on what the different worlds we try to combine have in common: they all have a notion of execution. But what is more important, these notions of execution all come with a natural prefix order that tells us how executions develop "over time".

In this talk, I would like to show you how much you can still achieve if you only look at the prefix order on the set of executions of a system. I would like to show you an example of how to model a system by observing its prefix order; I would like to show you how the category of prefix orders and history preserving maps gives rise to the products and unions one expects; I would like to show you how a limit can be defined for sequences of behavioral models, and why I think approximate bisimulations are not a good idea; And I would like to show you how branching bisimulation can be captured categorically, even when you have continuous time (so without a notion of 'step').

Whether I manage to do all this in the time allotted... we'll see. Of course, I can focus on whatever you would like to hear!

Branching bisimilarity and branching bisimilarity with explicit divergences are typically used in process algebras with silent steps when relating implementations to specifications. When an implementation fails to conform to its specification, i.e. when both are not related by branching bisimilarity [with explicit divergence], pinpointing the root cause can be challenging. In this talk I will present a Spoiler-Duplicator game that exactly characterises branching bisimilarity [with explicit divergence], offering an operational understanding of both relations. We show how such a game can be used to assist in diagnosing the non-conformance between an implementation and specification. Moreover, I will show how we can generalise and parameterise our Spoiler-Duplicator game so that it can be made to also characterise weak, eta, and delay bisimulation.

This is joint work with David de Frutos Escrig and Jeroen Keiren.

Higher inductive types allow the programmer to simultaneously add equalities while defining an inductive type. This way one can define quotient types in type theory, but it also is possible to give straightforward definitions of the integers, the integers modulo 2, and finite sets with elements from a certain type.

In this talk we will present work by Herman, Henning and myself where we look more closely at some specific higher inductive types. We show how to implement them in Coq, and in addition we give some surprising results.

In this talk we will examine Lawvere's fixed point theorem, which is a generalisation of the Cantor-Russell-Turing-Gödel argument in a categorical setting. By boiling down the argument to the bare minimum, Lawvere really puts the "diagonal" in the "diagonal argument". We will see how Lawvere's theorem can be used to prove various "negative" results, such as Cantor's theorem and Russell's paradox, as well as "positive" results, such as existence of fixed point combinators in λ-calculus.

A DFA is called synchronizing if a word w exists, such that processing w from any state yields one single result state. It was conjectured by Cerny in 1964 that for every synchronizing DFA on n states the shortest such w has length at most (n-1)^2, and he gave a sequence of DFAs for which this bound is reached. This conjecture is still open.

In 2006 Trahtman conjectured that apart from Cerny's sequence only 8 DFAs exist attaining the bound. He gave an investigation of all DFAs up to certain size for which the bound is reached, and which do not contain other synchronizing DFAs. Here we extend this analysis in two ways: we drop this latter condition, and we drop limits on alphabet size. For n <= 4 we do the full analysis yielding 19 new DFAs with smallest synchronizing word length (n-1)^2, refuting Trahtman's conjecture. For n > 4 we prove that none of the known examples admit non-trivial extensions keeping the same smallest synchronizing word length (n-1)^2.

This is joined work with Henk Don from the mathematics department of our university; this work was initiated by Henk's talk at the Brouwer seminar half a year ago.

When using a proof assistant to reason in an embedded logic - like separation logic - one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic.

In this talk, I will introduce IPM: Interactive Proof Mode for embedded logics in Coq, a novel method for extending the Coq proof assistant with (spatial and non-spatial) named proof contexts for the object logic. Thanks to these contexts we have been able to implement high-level tactics for introduction and elimination of all connectives of the object logic, and thereby made reasoning in the embedded logic as seamless as reasoning in the meta logic of the proof assistant. We have applied our method to Iris: a state of the art higher-order impredicative concurrent separation logic.

This majority of this talk will consist of a demonstration in which I show how to use IPM for formalizing correctness proofs of (concurrent) algorithms. Apart from that, I will give an overview of other applications of IPM: formalizing the Rust type system, formalizing the Iris meta theory, and proving contextual refinement of fine-grained concurrent algorithms.

This is joint work with Amin Timany and Lars Birkedal.

Implicit Computational Complexity Theory aims to characterize complexity classes by putting restrictions on the kind of algorithms and functions involved rather than explicitly putting bounds on time and space. We will discuss one such characterization of the class of Polytime Functions, due to Brunel and Terui. They set up a type system in which functions are polytime if and only if they are of type Church => Scott. In the process we will investigate an intuitive measure of time cost for the weak call-by-value lambda calculus.

In type theories like Martin-Löf type theory one often assumes that there is only one proof for an equality, namely reflexivity. In homotopy type theory this assumption is dropped and non-trivial identity proofs are allowed. This becomes especially powerful if one can add identities to the theory, as then, for example, quotient types can be represented. A controlled way to add identity proofs are higher inductive types. These are like inductive types in classical type theories, only that we are not just allowed to specify constructors for elements of a type but also for identity proofs on that type.

Currently, many examples of higher inductive types are known but a general definition is missing. In this talk, we rectify this situation and introduce a general syntax for higher inductive types, which also allows constructors for higher paths. Moreover, we give the corresponding elimination and computation rules, and show that computations preserve types. Finally, we show how to interpret a subclass of these higher inductive types over categories, an instance of which is the category of topological spaces.

From the perspective of classical logic, the meaning of a logical connective is given by its truth table. Constructive logic takes a different point of view: a connective is explained by explaining what a proof involving that connective is. We take a different approach and derive natural deduction rules, both for constructive and for classical reasoning, from the truth table. An obvious advantage is that this yields rules for all connectives, for example we find constructive rules for the ternary connective "if-then-else". We show that, if we also have "false" and "true", "if-then-else" is functionally complete for constructive proposition logic. Our procedure also yields new rules for well-known connectives that — as we will argue — are better than the well-known rules. Finally, constructive proofs have a computational interpretation and the constructive derivation rules are sound and complete for Kripke semantics.

This is joint work with Tonny Hurkens.

Nominal automata are a generalization of deterministic automata that allow for infinite alphabets. Despite being infinite, these automata admit finite representations and are closely related to register automata. The natural notion of size seems to be the number of orbits of such an automaton. It can be shown, however, that the number of orbits can grow quite big, even for seemingly simple languages. In this talk I will present some abstract ways to reduce the state space, similar to how non-deterministic automata can be smaller than their deterministic counterpart.

This is very much work in progress which started in London when I visited Alexandra Silva.

A deterministic finite automaton is synchronizing if there exists a word that sends all states of the automaton to the same state. Cerny conjectured in 1964 that a synchronizing automaton with n states has a synchronizing word of length at most (n - 1)^2.

In this talk I will first explain this conjecture and give some examples. Then an overview of some upper bounds for the general case will be provided. After this introduction, I will define aperiodically 1-contracting automata and prove that in these automata all subsets of the state set are reachable, so that in particular they are synchronizing. Furthermore, I will give a sufficient condition under which the Cerny conjecture holds for aperiodically 1-contracting automata.

The talk will not require any specific knowledge about automata, I will just start from the basics.

In this talk we will introduce Π-Ware, a Domain-Specific Language embedded in Agda for the modelling, simulation, verification and synthesis of hardware circuits. Circuits are described in architectural fashion, and thus geared to physical implementation. The depedent type system of Agda allows us to write *type-safe* circuits and circuit generators, while keeping these descriptions modular and generic. By induction, we can write *modular* proofs about whole classes of circuits, generically over size, number of inputs, etc. Furthermore, a notion of of circuit equivalence allows us to talk about semantics-preserving circuit transformations. Considering the tradition enjoyed by the study of coalgebras in Nijmegen, we also present our simple coalgebraic semantics for stateful circuits, with some corresponding examples and correctness proofs.

Further information and accompanying code can be found at http://piware.alvb.in.

After an introduction to term graphs we will present two natural ways to apply term rewrite rules on term graphs, and show the difference. We will show how for both flavors we can automatically prove termination of the resulting term graph rewrite systems by transforming them to graph transformation systems and applying the termination tool we developed for that.

This is joined work with Dennis Nolte and Barbara Koenig from Duisburg.

We first prove that solving Mahjong Solitaire boards with peeking is NP-complete, even if one only allows isolated stacks of the forms aab and abb. We subsequently show that layouts of isolated stacks of heights one and two can always be solved with peeking, and that doing so is in P, as well as finding an optimal algorithm for such layouts without peeking.

Next, we describe a practical algorithm for solving Mahjong Solitaire boards with peeking, which is simple and fast. The algorithm uses an effective pruning criterion and a heuristic to find and prioritize critical groups. The ideas of the algorithm can also be applied to solving Shisen-Sho with peeking.

In this talk, I will present a type theory that is based solely on inductive and coinductive dependent types. All inductive (coinductive) types come with the corresponding constructors (destructors) and recursion (corecursion) principles. I will show how we can represent logical connectives, and the corresponding introduction and elimination rules in this type theory. Most notably, we can encode existential quantification as inductive type and universal quantification (and hence the function space) as coinductive type.

This talk is based on a joint paper with Herman Geuvers, which we recently submitted. In that paper we also prove subject reduction and strong normalisation for the calculus I will present.

November 1st, 2015, Arjen P. de Vries joined iCIS as professor of "Information Retrieval" (IR). While the rise of the internet has helped strengthen the field, the area stretches far beyond plain web search, as a discipline situated between information science and computer science. IR takes the notion of "relevance" as its core concept. As the scope of IR is limited to those cases where computers try to identify the relevance of information objects given a user's information need (as opposed to humans doing that, the common scenario in information science), perhaps "Computational Relevance" would have been a better term for the research in this area.

I will introduce some of the main research questions that arise in IR, with a slight bias to my own personal interests in this domain.

This is a workshop co-located with Robbert Krebbers' defense. It takes place one day after. Details, abstracts etc. can be found at http://robbertkrebbers.nl/verification_workshop/.

A subset S of the natural numbers N is said to be k-automatic if there is a finite automaton that takes n, expressed in base k, as an input, and accepts if n is in S and rejects otherwise. What is the "right" definition of k-automatic for subsets of the rational numbers Q?

In this talk I will discuss one possible answer, and relate the solution to various (hard) questions of number theory and logic.

Homotopy Type Theory refers to a new interpretation of Martin-Löf's system of intensional, constructive type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, constructive type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos. The Univalent Foundations program aims to provide a comprehensive, computational foundation for mathematics based on the homotopical interpretation of type theory. Voevodsky's subtle Univalence Axiom, relates propositional equality on the universe with homotopy equivalence of small types. Coquand's cubical set model gives a computational interpretation of the univalence axiom. I will present the model and its implementation.

We will argue that a natural way to transform streams is by finite state transducers, that is, finite automata with output. If feeding a stream A to a finite state transducer yields a stream B as output, then we write A >= B. In this pre-order the smallest streams are the ultimately periodic streams. The structure of streams with respect to this pre-order raises many questions, most of which are open. A stream A is called atomic if for every stream B with A >= B we either have B >= A or B is ultimately periodic. The stream 1101001000100... in which the sizes of consecutive groups of zeros are consecutively 0,1,2,3,4,... was known to be atomic. Recently we proved that this also holds for the stream 11010000100.. in which the sizes of consecutive groups of zeros are the consecutive squares 0,1,4,9,...

This is joined work with Joerg Endrullis and others.

This talk is about automata with infinite alphabets, decidability, variables, data and symmetry.

Languages with infinite alphabets model resource generation, e.g., object-orientation, cryptograpy, service-oriented computing, dynamic networks.

Acceptors of (regular) languages with infinite alphabets have been defined as finite state automata with memory registers, that is, state variables, retaining good decidability properties. When composing such machines, some registers may be synchronised by pulling wires between them. Minimization is even possible, and as a side effect, symmetry groups are computed, that compress languages even exponentially.

Everything seems nice so far. But some of these "finite state automata with registers" are not even finite, and do not even have registers; in this case state variables do not exist, and synchronisation happens by pure magic.

This apparent contradiction is solved by an equivalence of models, that can be travelled in both directions, leading us to the conclusion that data does not exist either. We argue that this dual perspective actually helps.

The current technology for formalizing mathematical proofs in a computer has been developed by computer scientists, primarily with applications in computer science in mind. These systems can also be used for the formalization of mathematics, with impressive results, but the question remains whether the "style" of these systems is optimal for mathematics, and whether systems for formalization of computer science and systems for formalization of mathematics should be differentiated.

In this talk I will use a duality result between equations and coequations for automata, proved by Ballester-Bolinches, Cosme-Llopez, and Rutten, to characterize nonempty classes of deterministic automata that are closed under products, subautomata, homomorphic images, and sums. One characterization is as classes of automata defined by regular equations and the second one is as classes of automata satisfying sets of coequations called varieties of languages. I'll show how the results are related to Birkhoff's theorem for regular varieties.

Starting a new formalization in a proof assistant, one often needs to reprove theorems already found in the libraries of other provers. In some cases the knowledge is even already formalized in the same prover, just uses different definitions or concepts. In this reproving process, the available infrastructure may be different, so the proof is often not straightforward. Still, a human can take inspiration from the information already available in the other prover or library.

In this paper we propose and implement a methodology to automate this process. Similar concepts in the formalizations are automatically recognized based on their common properties to form a combined library. AI-ATP methods can use this combined library to more accurately predict needed dependencies and prove more goals. % using hammer technology. To measure the performance of the proposed approach, we define a number of knowledge-sharing scenarios and evaluate it on the HOL Light and HOL4 libraries. We evaluate the scenarios by reproving theorems from one library using the knowledge from the other.

Sorting networks are a very simple model of data-independent sorting algorithms, suitable for implementation in hardware. Proving optimality of a sorting network, whether in terms of number of necessary gates or execution steps, remains however a daunting task, as it requires showing that no smaller arrangements of gates can sort all inputs. Due to the huge combinatorial explosion, after the initial results obtained in the 60s there was almost no advance in this field for nearly fifty years. In this talk, I will introduce the topic and the problems we are most interested in addressing, and show how a novel combination of new theoretical insights and advances in computer-science has led to a number of computer-assisted proofs of new results about sorting networks during the last two years.

I will present a type theory that is suitable for writing and reasoning about algorithms for quantum computers. After a crash course in quantum theory and quantum computation, I will present the type theory and verify properties of one or two quantum algorithms. The system has these properties:

1. The type theory is affine: Weakening holds, but Contraction does not. So information can be destroyed, but cannot be duplicated.
2. The law of excluded middle holds, but the distributivity law fails: P & (Q v R) is not equivalent to (P & Q) v (P & R).
3. Perhaps the most famous feature of quantum theory: measuring a property of a system changes the state of the system. Thus, propositions have side effects.

I assume no prior knowledge of quantum theory.

In this talk, I will discuss how coalgebras can be used to establish equivalences and predicates for lazy programming languages, and how to use up-to techniques make the resulting proof methods tractable.

More specifically, we will use a variation of the copattern language introduced by Andreas Abel et al., and show how to characterise a notion of observational equivalence and productivity for this language. Moreover, we will introduce some interesting up-to techniques to simplify proofs of productivity. Finally, we use these techniques to obtain decision procedures for a fragment of the language.

In this talk I will present the indexed equality type, a generalization of the usual equality type that makes it easy to express equalities of dependent types. The construction is based on the homotopy interval, a higher inductive type consisting of two points and a path between them.

I will then take this indexed equality as a primitive notion for an observational type theory, that is, a type theory where equality is defined inductively on the structure of types. This type theory will support computation, as well as functional extensionality and univalence.

In automated theorem proving, the choice of search strategy heavily impacts the performance of the prover. Figuring out when to use which search strategy is a long standing problem in the automated reasoning community. The standard approach is to use strategy scheduling, i.e. running several different search strategies after each other. One method for determining which strategies to include in the schedule is to apply machine learning.

Four typical strategy scheduling algorithms for automated theorem provers both with and without machine learning will be presented and their performance on the TPTP problem library will be compared. Some of the typical problems of implementing learning-based strategy scheduling algorithms as well as their solutions will be shown. The theoretical discussions are illustrated with experiments with the automated theorem prover E, using the novel scheduling system VanHElsing.

VanHElsing 1.0 is a general strategy scheduling framework for ATPs. It can be seen as an ATP-tuning program. Given an ATP and some training data it creates a strategy scheduler. This scheduler can then try to find the strategies, time limits and order that is most likely to solve given problems in as little time as possible. VanHElsing is designed to work with arbitrary ATPs. It competed in the FOF and THF division of CASC-J7, and was awarded first prize in the THF division.

This is joint work with Daniel Kuehlwein, Frank Dorssers and Sil van de Leemput. The relevant paper was submitted to CADE-25 and is pending review.

Petri Nets are a well-known formalism to describe concurrent computations. An interesting aspect is that they allow for the representation of causal dependencies among actions. In this talk we describe an approach to derive compact (often finite state) operational models for causality in Petri nets. First, we provide a set-theoretic model in the form of a causal case graph, that is a labelled transition system where states and transitions represent markings and firings of the net, respectively, and are equipped with causal information. Causal case graphs may have infinitely-many states and transitions, but an equivalent, finitely-branching model can be derived, which admits a minimal, often finite-state, representative. Then we recast these models in a category-theoretical setting, where some constructions become more natural. We exploit the fact that events can be represented as names, and event generation as name generation. Thus we can apply the Turi-Plotkin framework, where the semantics of nominal calculi are modelled as coalgebras over presheaves. We model causal relations as a suitable category of posets with action labels, and generation of new events with causal dependencies as an endofunctor on this category. Presheaves indexed by labelled posets represent the functorial association between states and their causal information. Then we define a well-behaved category of coalgebras. Our coalgebraic model is still infinite-state, but we exploit the equivalence between coalgebras over a class of presheaves and History Dependent automata to derive a compact representation, which is equivalent to our set-theoretical compact model. Remarkably, state reduction is automatically performed along the equivalence.

Formal verification of hardware designs is difficult and sometimes even impossible in practical settings. Difficulties arise in industrial designs where cycles, open wires, inout wires, and multiple assignments are common. Work arounds and ad hoc solutions exist to overcome these issues. We give a general mathematical foundation supporting the encoding of such hardware in terms of Boolean formulas. The practical implication of this work is to ease the application of verification tools – like SAT solvers – to general hardware designs.

In order to make the formalization of mathematical proofs more commonly practiced, the availability of a comprehensive library of formalized mathematics is essential. Despite some notable attempts in this direction, a truly successful realization still seems a long way off. As noted by F. Wiedijk, one of the difficulties lies in maintaining a library that both has many contributors and at the same time remains well-organized.
In this talk, I will begin to discuss a couple of requirements which I believe are necessary to solve this "sociological puzzle", and why for example the often proposed wiki-model is lacking in this regard. Next, I will sketch an alternative model for mass collaboration, which is aimed at satisfying these requirements better. I will end with some final remarks concerning the concrete application of this model in the context of formalizing mathematical knowledge.

Over the years many techniques and strong tools have been developed for automatically proving termination of rewrite systems. For proving non-termination until now most techniques focus on searching for particular patterns of infinite reductions. However, there are extremely simple rewrite systems like the S rule a(a(a(S,x),y),z) → a(a(x, z), a(y, z)), for which infinite reductions are known (the first one found by Henk Barendregt), but for which all existing techniques fail to find this automatically. A similar observation holds for the even simpler delta rule a(a(d,x),y) → a(y,a(x,y)).

It is easy to see that non-termination follows from the existence of a non-empty set of terms that is closed under rewriting and does not contain normal forms. We present a technique to find tree automata by SAT solving for which the language of accepted terms satisfies the above criteria, hence proving non-termination. By this technique non-termination of the S rule and the delta rule, and many more examples, can be proved fully automatically.

This is joined work with Joerg Endrullis from VU Amsterdam.

CH2O is the PhD project of Robbert Krebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fundamentally inconsistent.

There are three versions of the CH2O semantics: a (small step) operational semantics, an executable semantics, and an axiomatic semantics (a separation logic for C). The most important properties -- soundness and completeness results, subject reduction and progress, correctness of the type checker -- have all been proved. All definitions and proofs have been fully formalized in Coq, without any axioms and on top of a non-trivial support library.

The CH2O project has two abstract C-like languages. A significant subset of C called "CH2O abstract C" is translated into a simplified language called "CH2O core C". This translation is written in Coq and implicitly gives a semantics to CH2O abstract C. The rest of the formalization is all about CH2O core C.

The executable CH2O semantics has been extracted to OCaml and combined with the CIL parser to a standalone "interpreter". This tool can be used to explore all behaviors of a program according to the C standard. Although the CH2O semantics does not yet support I/O (nor the exit function), a small hack allows the CH2O interpreter to still explore programs that call printf.

The CH2O semantics has been specifically designed to be compatible with the CompCert semantics for C. Significant differences between CompCert and CH2O are that the CH2O semantics has explicit typing judgments for everything, and that CH2O applies to any ISO compliant compiler.

Learning-assisted automated reasoning systems provide a tool-chain for automatically proving theorems in ITPs. This tool-chain consists of proof translation, premise selection and proof reconstruction. The HOL(y)Hammer system has implemented such a tool-chain for HOL Light and has been evaluated extensively with Flyspeck. In this talk we show how big parts of its infrastructure can be used for other interactive theorem provers. We discuss in detail the adaptation of HOL(y)Hammer to HOL4 and compare the results with HOL Light, devising comparable accessiblity relations and treatment of conjunctions. We also give an outlook on the combining of the two standard libraries and the further extension of HOL(y)Hammer towards other provers.

I will show how to use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata. If time permits I will discuss connections to determinization procedures and Brzozowski's minimization algorithm.

This is joint work with Bartek Klin.

I will describe a framework for game semantics that combines operational and denotational accounts. I'll illustrate the framework with an example of substitution within a lambda-calculus.

This is joint work with Paul Levy, presented at CSL-LICS 2014. http://www.cs.ru.nl/~sstaton/papers/lics2014-games.pdf

The question addressed in this talk is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, dataypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible non-termination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types. This is based on joint work with A. Kurz, A. Pardo, P. Severi and F.J. De Vries.

Rational trees are potentially infinite trees having finitely many distinct subtrees. In this talk, I will present various characterisation of rational trees and discuss the challenges of their mechanisation in proof assistants based on dependent type theory (Coq, Agda, ...). Finally, I will conclude with various applications.

We study a propositional variant of Hoare logic that can be used for reasoning about programs that exhibit both angelic and demonic nondeterminism. Our logical formalism is compositional and it subsumes the non-compositional formalism of safety games on finite graphs. We present sound and complete Hoare-style calculi that are useful for establishing partial correctness assertions, as well as for synthesizing implementations. The computational complexity of the Hoare theory of dual nondeterminism is investigated using operational models.

In 1987, Hagino introduced an extremely simple type system that only had type constructors for functions, and certain initial and final dialgebras. In this type system, sums and products could be represented, by using that they are respectively left and right adjoint to the diagonal functor C → C × C.

In this talk, we are going to extend this idea to dependent types. The type system we develop, has constructors that mimic initial and final dialgebras for functors on fibres of a fibration, generalising the functors used by Hagino. To make the theory more accessible, we develop it on vectors, a typical example of dependent types. Vectors are examined in two different fibrations, one giving possible set-based semantics and another being purely syntactic. We will be able to represent dependent sums and products in the resulting type system as adjoints to reindexing, which amounts to substitution in the syntax. In fact, the type system subsumes the dependent algebraic data types of Agda and presumably Coq.

In my PhD project I am developing a formal semantics of a significant fragment of the C programming language as described by the C11 standard. In this talk I will give a brief overview of the main parts of this semantics.

• A structured memory model based on trees to capture subtleties of C11 that have not been addressed by others.
• A core C language with a small step operational semantics. The operational semantics is non-deterministic due to unspecified expression evaluation order.
• An explicit type system for the core language that enjoys type preservation and progress.
• A type sound translation of actual C programs into the core language.
• An executable semantics that is proven to be sound and complete with respect to the operational semantics.
• Extensions of separation logic to reason about subtle constructs in C like non-determinism in expressions, and gotos in the presence of block scope variables.

All proofs are fully formalized using the Coq proof assistant. To explore all defined and undefined behaviors of actual C programs, we use Coq's extraction mechanism to obtain an interpreter that can compute a stream of finite sets of reachable states for a given program.

We define a simply typed lambda calculus with positive recursive types in which we study the less well-known Scott encoding of data types. Scott data types have "case distinction" as a basic feature. We shed a different light on the Scott data types, by viewing the different cases as "continuations". As Scott data types do not have iteration (or recursion) built in, we add as primitives a "call-by-name iterator" and a "call-by-value iterator" with appropriate reduction rules. We show that the calculus is strongly normalizing.

This talk will be a continuation of my talk of last week, but somewhat more technical. I will present the completeness result of Anderson et al. (POPL 2014) showing that the NetKAT axioms are deductively complete for the equational theory of the standard packet-switching model. I will also discuss the coalgebraic theory of NetKAT and present the bisimulation-based decision procedure for the equational theory from Foster et al. (POPL 2015).

NetKAT is a relatively new language and logic for reasoning about packet switching networks. The system was introduced quite recently by Anderson et al. (POPL 2014) and further developed by Foster et al. (POPL 2015). In this talk I will present a survey of this recent work and its role in the emerging area of software-defined networking.

We present a (co)algebraic treatment of dynamic modal logics such as Propositional Dynamic Logic (PDL) and Game Logic (GL), both without iteration. The main observation is that the program/game constructs of PDL/GL arise from monad structure, and the axioms of these logics correspond to certain compatibility requirements between the modalities and this monad structure. Our main contribution is a general soundness and strong completeness result for PDL-like logics for T-coalgebras where T is a monad and the program constructs are given by sequential composition, test, and pointwise extensions of operations of T. (Joint work wih Clemens Kupke.)

Modern automotive and aircraft industry faces the problem of designing and verifying reliable, secure and trustworthy on-board computers. As these systems must be able to control safety-critical systems such as the breaks of a car and the airbags, their certification occurs according to the highest levels set by the European governments. EUROMILS is a project funded by a European consortium with as aim a highly certified on-board chip architecture for future cars and planes. We present our part of this effort, namely the formal verification of such a chip architecture. This concerns security related properties such as non-interference between domains that may not interfere each other. For the verification we use the Isabelle theorem prover.

In a Latin square of size n every number from 1 to n occurs exactly once in every row and every column. Two neighbors (straight or diagonal) in a Latin square are connected by an edge if their values differ at most 1. We investigate Latin squares for which this underlying graph has typical graph properties, like being connected, being a tree or being Hamiltonian. Searching for such Latin squares shows up combinatorial explosion. Nevertheless, by exploiting current SAT/SMT solving, we explicitly find instances for several variants, or prove that they do not exist.

The study of programming languages proceeds along two lines, one syntactical and one denotational. On the syntactical side we have formal type theories and proof systems, while on the denotational side we have abstract mathematical objects. Many type theories are not Turing complete, so to serve as a basis for programming languages which have this property, different constructs can be added to the type theories to make them Turing complete.

In a recent dissertation, Venanzio Capretta has shown how to represent general recursion in a type theory by using the data type of coinductive natural numbers. We study the denotational side by analyzing the relation between the domains of the lazy and the coinductive natural numbers. In particular we show that there exists a mediating embedding-projection pair between the final coalgebras of the functors 1+X and 1+X+X in the category of complete, pointed partial orders. The construction is then generalized to show that arbitrary polynomial functors can be augmented with computation steps in a similar way.

The talk will first provide some background information about the challenges of operating-system verification and the results achieved so far. I will then present FireEye's approach for improving cyber security. Finally, I introduce the new research and development center at Dresden and talk about our goal to use formal methods to further improve FireEye's products.

A logical framework is a formal language for specifying formal languages. The idea of a canonical logical framework - a framework in which every term is in normal form - is an idea whose time has come. It was invented independently several times in the early 2000s (Aczel's TF, Harper and Pfenning's Canonical LF, Plotkin's DMBEL). Many problems - such as proving the correctness of a type-checking algorithm, or the conservativity of adding coercive subtyping - become insultingly easy in a canonical framework. Prove the equivalence of your canonical framework with your original framework - a one-time cost - and you get all those results for free.

That equivalence is trickier than it looks at first sight. As type theories, Logical frameworks are the most well-behaved and boring of systems, containing essentially only predicative function types. We expect the result to be a dry technical proof. But something seems to "happen" at order 3: third-order logical frameworks behave very differently from second-order logical frameworks. This difficulty may show that we do not understand the most well-studied features of type theories as well as we think we do.

One can check at http://www.cs.ru.nl/~herman/ccalc, that the CC program

goto.E → E
twice.G.E → G.(G.E)

evaluates the term twice.(twice.goto).end in 7 steps to end. It contains two terms of the form twice.goto.E which evaluate in 3 steps to Z.

A Call by Need evaluation avoids this as follows:

1. replace the subterm twice.goto by a new constant twicegoto
2. add the program rule twicegoto.E → twice.goto.E
3. before the first use of a rule, allow rewriting the body as far as possible In this case, the modified rule is twicegoto.E → E.

A circular definition like loop -> loop can be avoided by adding arguments: loop -> omega.omega omega.O -> O.O In this way, each CC program and start term can by defined just using application and pure combinators.

CC terms do not use lambda-abstraction (only application) and are only rewritten at top level. Typing CC programs and terms does not guarantee termination, but the right number of arguments at top level. The typing system for CC presented by Herman uses mu-abstraction to define recursive types. Just like in simply typed lambda calculus, each type is either

1. a base type (say Falsum, the type of top level terms in CC)
2. a function type F = A → B

In fact, omega could be type by allowing a type Omega = Omega → Falsum. It is sufficient to represent each type by a constant and treat a function type as a rule F → A → B to type applications: if f:F and a:A then f.a:B.

Streams are the simplest possible infinite objects: just infinite sequences. The simplest streams are periodic, up to an initial part. The one but simplest are morphic streams: fixed points of particular morphisms. These morphic streams can also easily be defined by rewriting. The simplest way to visualize a stream is by a turtle curve: for every alphabet symbol fix an angle, and then proceed the stream elements by drawing unit segments and turn the corresponding angle. Often the resulting picture is a complete mess, but sometimes the result is finite, or shows up fractal = self-similar behaviour: it contains an upscaled copy of itself. In the talk we give criteria on turtle curves for being finite or self-similar, providing a guide to generate amazing pictures that we show for very simple morphic stream definitions. Moreover, we show how the Thue-Morse stream may yield the Koch curve.

Data in the lambda calculus is usually represented using the "Church encoding", which gives closed terms for the constructors and which naturally allows to define functions by "iteration". A problem is that primitive recursion is not directly available: it can be coded in terms of iteration at the cost of efficiency (e.g. a predecessor with linear run-time). The much less well-known Scott encoding has case distinction as a primitive. We will present a unification of the Church and Scott presentation of data types, which has primitive recursion as basic. We show how these can be typed in the polymorphic lambda calculus extended with recursive types and we show that all terms are strongly normalizing. We also show that this works for the dual case, co-inductive data types, and we show how programs can be extracted from proofs in second order predicate logic.

Quantum computing and quantum communication are exciting areas of research at the intersection of physics and computer science, which have great potential for influencing the future development of information processing systems. Quantum cryptography, in particular, is well developed. Commercial Quantum Key Distribution systems are easily available and several QKD networks have been built in various parts of the world. However, the security of the protocols rely on information-theoretic proofs, which may or may not reflect actual system behaviour, and testing of the implementations. We present a novel framework for modelling and proving quantum protocols using the proof assistant Coq. We provide a Coq library for quantum bits (qubits), quantum gates, and quantum measurement. We implement and prove a simple quantum coin flipping protocol. As a step towards verifying practical quantum communication and security protocols, such as Quantum Key Distribution, we support multiple qubits, communication and entanglement. We further illustrate these concepts by modelling the Quantum Teleportation Protocol, which communicates the state of an unknown quantum bit using only a classical channel.

As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This talk shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda's reflection mechanism provides a first-class proof search tactic for first-order Agda terms. Furthermore, the same mechanism may be used in tandem with Agda's instance arguments to implement type classes in the style of Haskell. As a result, writing proof automation tactics need not be different from writing any other program.

Cryptographic software is different from most other software in various ways. It is typically relatively small pieces of code that are executed many times. This is why it is often carefully hand-optimized on the assembly level for various (micro-)architectures. Also, it is operating on secret data and information about this data must not leak through timing information. Finally, it is highly security critical and bugs are not only triggered by accidently choosing a certain input but by attackers choosing such inputs on purpose. In my talk I will give an introduction to highly optimized cryptographic software and the challenges in ensuring the correctness and security of such software. I will conclude the talk with recent results on verifying the correctness of hand-optimized cryptographic software written in AMD64 assembly.

The schedule is as follows:

• 13:30 – 14:15, Sjaak Smetsers: Bialgebraic semantics in PVS
• 14:15 – 15:00, Joost Winter: TBA
• 15:15 – 16:00, Enric Cosme-Llopez & Jan Rutten: The dual equivalence of equations and coequations for automata

Streams over a set A together with the head and tail operations are the standard representation of the final A × (-) coalgebra. Perhaps less known is the fact that streams also form a final A × (-)^k coalgebra, that is, a final deterministic automaton on alphabet k with output in A. In this talk, I will show how this final coalgebra of streams yields a coalgebraic characterisation of k-automatic and k-regular sequences, together with coinductive specification formats in the form of behavioural differential equations using the zip-operations.

Nominal calculi are formalisms for modeling systems that feature resource allocation. They represent resources as names, that are atoms characterized only by their identity, and express resource allocation via name generation primitives. Names and related primitives require non-standard notions of bisimulations, and may yield infinitely-branching and infinite-state transition systems. These issues have been tackled by introducing ad-hoc operational models. In this seminar I will present two of them, namely coalgebras over presheaves and History-Dependent Automata. The former equip coalgebras with name generation capabilities, the latter are finite-state automata suitable for verification. These models are tightly related: HD-automata can be derived from coalgebras over presheaves via a categorical construction. I will provide some examples from my thesis and ongoing work.

Separation algebras are a well-known abstraction to capture common structure of both permissions and memories in programming languages, and form the basis of models of separation logic. As part of the development of a formal version of an operational and axiomatic semantics of the C11 standard, we present a variant of separation algebras that is well suited for C formalization.

Our variant of separation algebras has been fully formalized using Coq, and we present a library of concrete implementations of these algebras. This leads to instances for a complex permission system, and our memory model that captures the strict aliasing restrictions of C.

The proof assistant Isabelle/HOL has recently been extended with codatatypes (cf. my December 2012 Brouwer seminar). They are equipped with corecursors, which can be used to specify arbitrary primitively corecursive functions. The "primcorec" command lets user enter specifications in a flexible format and synthetizes the arguments to the corecursors [1]. We also have a prototype of a "corec" command that provides corecursion "up to" and have some ideas on how to go further with a "cofun" command that allows combinations of recursion and corecursion via a limit construction.

The talk is expected to last about 30 minutes, followed by a short break and a discussion for those interested.

[1] Blanchette et al., Truly Modular (Co)datatypes for Isabelle/HOL, accepted at ITP 2014.

This joint work with Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel

Preliminary schedule:

• 10:00 Welcome + Coffee
• 10:15 Marcos Cramer (University of Luxembourg): The Naproche system: Proof-checking mathematical texts in controlled natural language
• 11:15 Stephan Schulz (TU Munich): Less Brain, More Data - Strategy Scheduling for E 1.8
• 12:00 - 13:00 Lunch Break
• 13:00 Josef Urban (RU Nijmegen): Lemma Mining in Flyspeck
  
• 13:45 Daniel Kuehlwein (RU Nijmegen): How to characterize higher order problems and new machine learning algorithms for improving ATPs
• 14:30 - 14:45 Coffee
• 14:45 Jasmin Blanchette (TU Munich): Machine Learning for Sledgehammer, the Story So Far
• 15:30 End

We present a type system for reasoning about extensional equality. The system is an extension of the type-in-type PTS lambda-*, hence inconsistent. We expect however that stratifying the universe into levels (with *_n : *_n+1) results in a normalizing system which, in contrast to classical extensional type theory, has decidable type checking.

The system has three types of equality relations:

• "type equalities" e : A ≈ B, where A,B : *;
• "dependent equalities" æ : a ~e b, where a:A, b:B, and e:A≈B;
• "extensional equality" a* : a ≈A a', where a,a' : A for A : *.

There is a reflexivity operator: r(a) : a ≈A a, which creates a redex whenever a is reduced to a constructor.

The system has two kinds of substitutions

1. the usual one, where

   x : A |- M : B     |- a : A

   |- M[a/x] : B[a/x]

2. the substitution of equalities, or "path substitution":

   x : A |- M : B     |- a* : a ≈A a'

   |- M[a*//x] : M[a/x] ~B[a*//x] M[a'/x]

These constructs satisfy the following identities:

M[a*//x]	= r(M) if x is not in FV(M)
a ≈A a'	= a ~r(A) a'
A ≈ B	= A ≈* B

We will present the above system and discuss ongoing work on extending it with homotopy operations so that extensional equality becomes a higher-dimensional equivalence relation.

I will talk about some questions Hans Zantema and I have been thinking about.

A subset L of the streams over {0,1} is called clopen when one can decide whether a stream σ is in L or not by inspecting only a finite part of σ. The language L is called Borel when it can be formed by countable union and countable intersection starting from the clopen subsets. These Borel sets can be organised in a hierarchy with the `simplest' Borel sets at the bottom. This hierarchy has been studied at the start of the 20th century. I will place some languages of streams in this hierarchy. I will show that any language of streams that is recognised by a Buchi automaton is Borel, but surprisingly there is a context-free language L of words over {0,1} such that the language of streams

L^ω := { w₁ w₂ w₃ ... : w₁, w₂, ... in L }

is not Borel!

Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such statements is named and re-used in later proofs by formal mathematicians. In this work, we suggest and implement criteria defining the estimated usefulness of the HOL Light lemmas for proving further theorems. We use these criteria to mine the large inference graph of the lemmas in the HOL Light and Flyspeck libraries, adding up to millions of the best lemmas to the pool of statements that can be re-used in later proofs. We show that in combination with learning-based relevance filtering, such methods significantly strengthen automated theorem proving of new conjectures over large formal mathematical libraries such as Flyspeck.

This is joint work with Cezary Kaliszyk.

Continuation Calculus (CC), as defined in [1] (see also the master thesis of Bram Geron), is a model for functional computations that aims at (1) being simple (simpler than lambda calculus and term rewriting), (2) remaining close to actual implementations and (3) being generic (incorporating various evaluation strategies). The original system is untyped, but there is a standard procedure for defining data in CC and writing functions over this data. In the talk we present a typing system for CC and compare it with the typing of data in lambda calculus. In lambda calculus, one has the iterative representation of data (e.g. the Church numerals), but also the less well-known recursive representation (e.g. the so called "Scott numerals"). In CC, the recursive data are the "standard" ones and we show how to type them, compute with them and reason over them.

[1] Bram Geron and Herman Geuvers -- Continuation calculus, Proceedings First Workshop on Control Operators and their Semantics, 2013, edited by: Ugo de'Liguoro and Alexis Saurin, EPTCS 127, pp 66-85.

As a preparation for a planned formalization of the notion of higher inductive type (HIT), we will present the text "semantics of higher inductive types" by Peter LeFanu Lumsdaine and Michael Shulman: the authors depart from the idea of W-types and give a strict- and a weak (i.e. homotopical) categorical semantics by way of a transfinite construction of free algebars, where the induction goes over the list of constructors of the type to be constructed. An inductive type W is understood as a higher inductive type if not only terms and terms of identity types between them but also terms of iterated identity types are constructed with the type W; where the authors restrict to the case where the iteration stops at stage 1 and where domains and codomains of 1 costructors are "strictly natural" (as opposed to "coherently natural"). They provide no type theoretical syntax for their notion of higher inductive type but remain entirely inside category theory. After discussing the special case of a higher inductive set and and giving the general description of HITs with only 0-constructors (for terms) and 1-constructors (for paths between terms), they show that any locally presentable, locally cartesian closed, right proper, cofibrantly generated, simplicial model category whose cofibrations are the monomorphisms admits HITs. In particular every infinity-topos can be presented in a way admitting HITs.

The goal of this talk is to relate the work in Abel et al. [1,2], Santocanale [3,7] and Ghani et al. [4,5]. As starting point for the connection, we choose a slight variation of the calculus from [2] which has fixed point types and terms for them. We organise these types A, B, ... into a category with arrows being terms of type A → B. This category is built in such a way that types with free variables define endofunctors that have initial algebras and final coalgebras for interpreting fixed point types.
Such categories are called μ-bicomplete by Santocanale [8], and he uses these in [7] to give semantics to circular proofs for the μ-calculus. In the spirit of the Curry-Howard correspondence between logic and programming, we find a relation between, on the one hand, propositions of the μ-calculus and their proofs and, on the other hand, fixed point types and terms. For the last link we establish a topology on the sets T (A) of terms of type A. This topology shall specialise to existing topologies (e.g. induced by prefixes in the case of streams). Furthermore we expect that terms t : A → B give rise to continuous maps T (A) → T (B). This establishes the connection to [4, 5] where it is demonstrated how continuous maps on final coalgebras can be programmed. The work presented is still in progress, so some topics are subject to change.

References
[1] A. Abel and B. Pientka. Wellfounded recursion with copatterns: a unified approach to termination and productivity. In ICFP, 2013.
[2] A. Abel, B. Pientka, D. Thibodeau, and A. Setzer. Copatterns: Programming infinite structures by observations. In POPL, 2013.
[3] J. Fortier and L. Santocanale. Cuts for circular proofs: semantics and cut-elimination. In CSL, 2013.
[4] N. Ghani, P. Hancock, and D. Pattinson. Continuous functions on final coalgebras. In Electr. Notes Theor. Comput. Sci., 249, 2009.
[5] N. Ghani, P. Hancock, and D. Pattinson. Representations of stream processors using nested fixed points. In LMCS, 5(3), 2009.
[6] J. Rutten. Behavioural differential equations: a coinductive calculus of streams, automata, and power series. In Theor. Comput. Sci., 308, 2003.
[7] L. Santocanale. A calculus of circular proofs and its categorical semantics. In FoSSaCS, 2002.
[8] L. Santocanale. μ-bicomplete categories and parity games. In RAIRO - ITA, 36(2), 2002.

I will give a summary of my PhD research on applying machine learning to improve automated reasoning systems. The focus will be (mainly) on the premise selection problem: Given a set of premises (e.g. library of axioms, definitions and already proved theorems) and a new conjecture, predict which premises are useful to prove the conjecture. The results of this research have been integrated in the ITP Isabelle. Depending on the domain, up to 20% more problems can now be solved fully automatic.

I will show a simple and elegant way to handle variable binding in a formalization. As a running example I will give a definition of the untyped lambda calculus in the proof assistant Agda. It turns out that the terms form a monad, which gives us substitution for free. Depending on the time I will work out an evaluator and/or a proof of confluence.

Automata learning is a known technique to infer a finite state machine from a set of observations. In this paper, we revisit Angluin's original algorithm from a categorical perspective. This abstract view on the main ingredients of the algorithm lays a uniform framework to derive algorithms for other types of automata. We show a straightforward generalization to Moore and Mealy machines, which yields an algorithm already know in the literature, and we discuss generalizations to other types of automata, including weighted automata.

This is joint work with Bart Jacobs.

Many structures are algebras of some functor. For instance, a group can be represented by a map G x G + G + 1 ---> G. But not every map G x G + G + 1 ---> G represents a group (it needs to heed the group axioms). Groups can be more truly represented as algebras of monad. In fact, the category of groups is isomorphic to the category of algebras of some monad T. This approach has its limitations: the category of fields is not equivalent to the category of algebras of any monad (although fields can be represented as algebras of a functor).

Similarly, many systems are coalgebras of a functor. I will explain what a comonad is, what a coalgebra of a comonad is, and how these can be used to represent systems with certain behavior. I will show that the category Top' of open and continuous maps between topological spaces is a subcategory of coalgebras of some functor, but that there is no comonad T such that Top' is equivalent to the category of coalgebras for T.

So topological spaces not susceptible to abstract coalgebraic reasoning in much the same way that fields are not suited for abstract algebraic reasoning.

Ugo Montanari (University of Pisa), Static and Dynamic Connectors
Recent years have witnessed an increasing interest about a rigorous modelling of (different classes of) connectors. Among the various contributions we can mention the algebra of stateless connectors by Bruni, Lanese and Montanari, the tile model, Reo, BIP, Petri nets with boundaries and the wire calculus. More recently, the diffusion of reconfigurable and adaptive systems has motivated the foundational study of models of connectors that can evolve dynamically, as opposed to the better understood notion of static connectors. In the talk we present some recent results about a novel banking semantics for (static) Petri nets with boundaries. Then we consider the BIP (Behavior, Interaction, Priority) component framework, by Sifakis et al., here denoted BI(P), as we disregard priorities. We introduce two extensions of BIP: 1) reconfigurable BI(P) allows to reconfigure the set of admissible interactions, while preserving the set of interacting components; 2) dynamic BI(P) allows to spawn new components and interactions during execution. Our main technical results show that reconfigurable BI(P) is as expressive as BI(P), but possibly with a much smaller number of states, while dynamic BI(P) allows to deal with infinite state systems. Still, reachability remains decidable for dynamic BI(P). (Joint work with Roberto Bruni, Hernan Melgratti and Pawel Sobocinski)

Filippo Bonchi (ENS Lyon), Unobservable transitions via Elgot Monads
The operational behaviour of computing devices is usually expressed through state machines whose transitions are labeled with different kind of information: symbols from an alphabet (in automata theory), substitutions of terms (in logic programming), elements of a lattice (in constraint programming), syntactical contexts (in process calculi), arrows of a category (in tile systems).
While states machines can be conveniently modeled as coalgebras, their labels usually form algebras. In this talk, we show that the standard coalgebraic perspective on state-based systems fails to model the underlying algebraic structures of the labels and we propose a solution based on Elgot monads. In particular, we show how the classical elimination of unobservable (epsilon) transitions from automata can be conveniently modeled in terms of Elgot monads. The benefit of such model are two-fold: on the one hand, we obtain a more abstract proof for the well-known soundness of elimination of unobservable transitions; on the other, the proof generalizes the results to several other kind of semantics, amongst which we consider Mazurkiewicz traces.

Georgiana Caltais, Coalgebraic Tools for Bisimilarity and decorated Trace Semantics
One of the research areas of great importance in Computer Science is the study of the semantics of concurrent reactive systems. Examples of such systems range from rather simple devices such as calculators and vending machines, to programs controlling mechanical devices such as cars, subways or spaceships. In light of their widespread deployment and complexity, the application of rigorous methods for the specification, design and reasoning on the behaviour of reactive systems has always been a great challenge.
In this presentation I will provide a brief overview on a coalgebraic framework for modelling and reasoning on the behavior of reactive systems, as introduced in my PhD thesis entitled "Coalgebraic Tools for Bisimilarity and decorated Trace Semantics". More precisely, we shall discuss the main ideas behind a uniform coalgebraic handling of a series of semantics on transition systems, obtained by employing a generalisation of the classical powerset construction for determinising non-deterministic automata. In particular, this approach deals with decorated trace equivalences for labelled transition systems and probabilistic systems and, (the so-called "must" and "may") testing semantics for divergent non-deterministic systems.

LCF-style proof assistants like Coq, HOL, and Isabelle have been traditionally tied to a sequential READ-EVAL-PRINT loop, with linear refinement of proof states via proof scripts. This limits both the user and the system to a single spot of interest. Already 10-15 years ago, prover front-ends like Proof General (with its many clones such as CoqIDE) have perfected this command-line interaction, but left fundamental questions open. Is interactive theorem proving a necessarily synchronous and sequential process? Is step-by-step command-line execution inherent to the approach? Or are these merely accidental limitations of historic implementations?

The PIDE (Prover IDE) approach to interactive theorem proving puts a conceptual Document-Model at the center of any proof development activity. It is the formal text that the user develops with the help of the system (including all background libraries). The editor front-end and prover back-end are smoothly integrated, in order to provide a metaphor of continuous proof checking of the whole formalization project (not just a single file). As the user continues editing text, the system performs formal checking in the background (usually in parallel on multiple cores), and produces output in the form of rich markup over the sources, with hints, suggestions etc. This may involve arbitrarily complex proof tools, such as ATPs and SMTs via Isabelle/Sledgehammer.

The combination of asynchronous editing by the user and parallel checking by the prover poses some challenges to the overall architecture, with many technical side-conditions. To cope with this, Isabelle/PIDE is implemented as a hybrid of Isabelle/ML and Isabelle/Scala. This enables the pure logical environment to reach out into the JVM world, where many interesting frameworks for text editors, IDEs, web services etc. already exist. Scala allows to continue the manner and style of ML on the JVM, with strongly-typed higher-order functional programming and pure values. This helps to achieve good performance and reliability in a highly concurrent environment.

The main example application of the PIDE framework is Isabelle/jEdit, which has first become available for production use with Isabelle2011-1 (October 2011). The underlying concepts and implementations have been refined significantly in the past 2 years, such that Isabelle/jEdit is now the default user interface of Isabelle2013-2 (December 2013). Recent improvements revisit the old READ-EVAL-PRINT model within the new document-oriented environment, in order to integrate long-running print tasks efficiently. Applications of such document query operations range from traditional proof state output (which may consume substantial time in interactive development) to automated provers and dis-provers that report on existing proof document content (e.g. Sledgehammer, Nitpick, Quickcheck in Isabelle/HOL).

So more and more of the parallel hardware resources are employed to assist the user in developing formal proofs, within a front-end that presents itself like well-known IDEs for programming languages. Thus we hope to address more users and support more advanced applications of our vintage prover technology.

Pure Type Systems (PTS) aim at forming a generic basis for various type theories. It captures a variety of systems (simple types, polymorphic types, dependent types, higher order types) but does not include e.g. inductive types, type inclusion and identity types.

Since PTSs have been introduced, various properties of them have been proved and variations on them have been studied. At the same time, various questions have remained unanswered. In the talk, we will overview some known "classic" results, some recent developments and some open problems. Topics we will treat are:

• proving subject reduction
• the problem with adding eta
• context free presentation
• the power of the conversion rule and making conversion explicit
• weak normalization and strong normalization
• inconsistent Pure Type Systems and the looping combinator

The C11 standard of the C programming language does not specify the execution order of expressions. Besides, to make more effective optimizations possible (eg delaying of side-effects and interleaving), it gives compilers in certain cases the freedom to use even more behaviors than just those of all execution orders.

Widely used C compilers actually exploit this freedom given by the C standard for optimizations, so it should be taken seriously in formal verification. This paper presents an operational and axiomatic semantics (based on separation logic) for non-determinism and sequence points in C. We prove soundness of our axiomatic semantics with respect to our operational semantics. This proof has been fully formalized using the Coq proof assistant.

The Flyspeck Project, a massive international collaborative effort to formalise the proof of the Kepler Conjecture, is approaching completion. The main part, known as the "text formalisation", was completed in August. It involved the work of 11 contributors, totalling around 450,000 lines of HOL Light proof script. The proofs process through HOL Light, but how understandable is this work to outsiders? Unfortunately, many of the proof scripts are many thousand lines long, have neither comments nor formatting, and prove various already-proved or unused lemmas.

In this talk, I will give an overview of Tactician, a utility that will be employed to clean up these proof scripts. Its features include proof script refactoring, identification of redundancy and inefficiency, and visualisation of the structure of a proof and the dependencies between lemmas. I will demonstrate its use on some of the more challenging of Flyspeck's proof scripts.

I will summarize what I learned during my visit to Cambridge about the CakeML project of Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens, and the related verification of the HOL Light kernel.

Linear Circuits represent systems of linear stream equations (recurrences) graphically. We develop an algebra which precisely characterises classes of circuits. The algebras are based on polynomials and fractions, allowing to effectively compare the behaviour of circuits. The result shows a nice interplay between algebra and coalgebra.

Algebra and coalgebra can be done abstracly in category theory, but also in second order logic (SOL). The additional advantage is that one can use the Curry-Howard isomorphism to extract programs from proofs. For algebra this has been shown in detail by Krivine and Parigot, in the system AF2 that allows to write correct programs over algebraic data types by extraction them from proofs in SOL. We will show how to extend this to coalgebraic data types, like streams. In the talk we start by showing how to do initial algebra's and final coalgebras in SOL and remember the encodings of some well-known data types. We extend this by defining the "canonical equality relations" on these data types, which for streams turns out to be bisimulation.

Moessner's Theorem describes a construction of the sequence of powers (1^n, 2^n, 3^n, ...), by repeatedly dropping and summing elements from the sequence of positive natural numbers. The theorem was presented by Moessner in 1951 without a proof and later proved and generalized in several directions. More recently, a coinductive proof of the original theorem was given by Niqui and Rutten. We present a formalization of their proof in the Coq proof assistant. This formalization serves as a non-trivial illustration of the use of coinduction in Coq. In the process of formalizing the original proof we discovered that Long and Salié's generalization of Moessner's Theorem could also be proved using (almost) the same bisimulation.

A string rewrite system (SRS) consists of rules l -> r in which l and r are strings. String rewriting means that a substring of the shape l is replaced by r, for some rule l -> r. Applied on strings this is well studied. However, from the perspective of graph transformation it is natural also to apply this on graphs, in particular on cycles, that can be seen as strings in which the left end is connected to the right end. Surprisingly, by this change of semantics, basic properties like termination drastically change. For instance, as an SRS the single rule ab -> ba is terminating in the string semantics, but not in the cycle semantics since as a cycle the strings ab and ba are equal.

In this talk we collect some basic observations on cycle rewriting. In particular, most techniques for proving termination of string rewriting fail to prove termination of cycle rewriting. We investigate some techniques for proving termination of cycle rewriting.

In recent work (to appear), Masahiko Sato and his co-authors have developed a canonical representation of name-carrying lambda terms based on a novel datastructure for representing binding, the so-called "map/skeleton" representation.

Their paper leaves as future work the challenging problem of how to give an adequate representation of the important judgments of interest (reduction, typing, ...) one might wish to define on such terms.

I have proposed to them a modest (indeed: conservative) extension to their language which appears to solve this problem (and formalised the proof of conservativity in Isabelle). Inter alia, the extension is based on a generalisation of Kleene's notion of "pure variable proof" (IMM, \S 78, p451), and the proof of conservativity on a modified version of McKinna-Pollack style reasoning (TLCA1993, JAR1999).

In this talk I'll try to sketch the map/skel representation and the proof of conservativity for typing and reduction for my extension of it.

For a datatype of real functions a representation is required. Several representations exist, for example the polynomial representation. We discuss this representation and prove it's the strongest continuous representation of real functions. This makes it suitable for exact real arithmetic.

HOL Zero is a basic theorem prover with a carefully designed architecture and concrete syntax that avoids various potential trustworthiness problems. It's implementation is simple, written in a clear style and heavily commented, with the intention of being understandable to a relatively wide audience, further boosting trustworthiness. It is, or so I claim, the most trustworthy theorem prover in the world!

In this talk, I'll give an overview of the HOL Zero system. I'll also cover some flaws found in other HOL systems, and show how HOL Zero manages to avoid these. $100 is rewarded to anyone who manages to find a flaw, so come along and crack the uncrackable if you can!

In automata theory, a machine transitions from one state to the next when it reads an input symbol. It is common to also allow an automaton to transition without input, via an ε-transition. These ε-transitions are convenient, e.g., when one defines the composition of automata. However, they are not necessary, and can be eliminated. Such ε-elimination procedures have been studied separately for different types of automata, including non-deterministic and weighted automata. It has been noted by Hasuo that it is possible to give a coalgebraic account of ε-elimination for some automata using trace semantics (as defined by Hasuo, Jacobs and Sokolova). Alexandra Silva and I have simplified the work of Hasuo and shown that it can be applied to weighted automata over the positive reals (and certain other semirings).

This talk is a rehearsal of the presentation of our work at CALCO.

Michael Nahas previously wrote code for high-performance distributed systems. He came to Radboud University for the summer and spent the last 3 months learning how to write formal proofs in Coq. One proof was the correctness of Dijkstra's famous paper in distributed algorithms. He frankly describes the experience along with the good and bad points of the Coq proof assistant. (Parental Advisory: This talk may contain profanity.)