Please contact the organizers , Niels van der Weide or Freek Wiedijk in case you are interested in giving a talk.

Winter 2019 Time Room Speaker Institute Title
Tu 26 Feb 13:30-14:15 HG00.622 Giulio Manzonetto Université Paris Nord Degrees of extensionality in the Böhm tree semantics
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.
Spring 2018 Time Room Speaker Institute Title
Mo 23 Apr 13:30-14:30 HG01.058 Dan Frumin RU ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
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.
Workshop on Mixed Inductive-Coinductive Reasoning Time Room Speaker Institute Title
Th 19 Apr 10:00-10:30 LIN 1 Ekaterina Komendantskaya Heriot-Watt University Coinductive Uniform Proofs

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.

Th 19 Apr 10:30-11:00 LIN 1 Jurriaan Rot RU Combining GSOS and coGSOS (for streams)
Th 19 Apr 11:30-12:00 LIN 1 Andreas Abel Chalmers On the Syntax and Semantics of Quantitative Typing
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.
Th 19 Apr 12:00-12:30 LIN 1 Tarmo Uustalu Tallinn University of Technology Coalgebraic Bar Recursion and Bar Induction
Th 19 Apr 13:30-14:00 LIN 1 Benno van den Berg Universiteit van Amsterdam Homotopy Type Theory with Explicit Conversions
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).
Th 19 Apr 14:00-14:30 LIN 1 Henning Basold ENS Lyon Inductive-Coinductive Reasoning: Past and Future
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.
Winter 2018 Time Room Speaker Institute Title
Tu 27 Feb 13:30-14:30 HG01.058 Bram Westerbaan RU Statman’s Hierarchy Theorem

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.

Fr 26 Jan 10:30-11:30 HG00.310 Tobias Kappe UCL Concurrent Kleene Algebra: Free Model and Completeness
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.
Tu 16 Jan 13:30-14:30 HG00.217 Hans Zantema RU, TU/e Word Representations of Graphs
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.
Autumn 2017 Time Room Speaker Institute Title
We 20 Dec 14:30-15:30 HG01.057 Dan Frumin RU Finite Sets in Homotopy Type Theory
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).
Tu 28 Nov 13:30-14:30 HG00.310 Guillaume Allais RU A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
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.
Th 16 Nov 15:00-16:00 HG00.065 Sven-Bodo Scholz Heriot-Watt University A Lambda-Calculus for Transfinite Arrays - Towards Unifying Streams and Arrays
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.
Tu 14 Nov 13:30-14:30 HG01.057 Niels van der Weide RU The Three-HITs Theorem
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.
Tu 31 Oct 13:30-14:30 HG00.633 Henning Basold CNRS, ENS de Lyon A Recursive Logic for the Equivalence of Inductive-Coinductive Programs
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.
Spring 2017 Time Room Speaker Institute Title
Tu 2 May 13:30-14:30 - Cancelled - -
Tu 18 April 11:30-12:30 - Easter - -
Tu 4 April 11:30-12:30 HG00.310 Guillaume Allais RU A Library of Total Parser Combinators

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 .

Tu 21 Feb 13:30-14:30 HG01.058 Pieter Cuijpers TUE Prefix Orders as a Generic Model for Behavioral Systems

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!

Tu 17 Jan 13:30-14:30 HG00.058 Tim Willemse TUE Games for Bisimulation and Abstraction
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.

Autumn 2016 Time Room Speaker Institute Title
Tu 20 Dec 13:30-14:30 HG00.065 Niels van der Weide RU Programming with Higher Inductive Types
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.

Tu 22 Nov 13:30-14:30 HG03.632 Dan Frumin RU One diagonal to prove them all
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.
Tu 25 Oct 13:30-14:30 HG00.058 Hans Zantema TUE/RU DFAs with maximal shortest synchronizing word length
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.

Tu 11 Oct 13:30-14:30 HG00.023 Robbert Krebbers Delft University of Technology Interactive Proofs in Higher-Order Concurrent Separation Logic
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.

Spring 2016 Time Room Speaker Institute Title
Tu 19 Jul 13:30-14:30 HG00.086 Rik de Kort RU A Type-Theoretic Characterization of Polytime Functions
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.
Tu 14 Jun 13:30-14:30 HG00.086 Niels van der Weide RU Higher Inductive Types
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.

Tu 17 May 13:30-14:30 HG00.058 Herman Geuvers RU Deriving natural deduction rules, both constructively and classically, from truth tables
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.

Tu 10 May 13:30-14:30 HG00.058 Joshua Moerman RU Succinct nominal automata
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.

Tu 19 Apr 13:30-14:30 HG01.028 Henk Don RU The Cerny conjecture and 1-contracting automata
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.

Tu 29 Mar 13:30-14:30 HG01.058 João Pizani Universiteit Utrecht Π-Ware: A Hardware Description Language embedded in Agda
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

Tu 22 Mar 13:30-14:30 LIN 4 Hans Zantema RU Term graph rewriting
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.

Tu 16 Feb 13:30-14:30 HG01.028 Michiel de Bondt RU Solving Mahjong Solitaire boards with peeking
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.

Tu 26 Jan 13:30-14:30 HG01.058 Henning Basold RU Dependent Inductive and Coinductive Types as Foundation for Logic
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.

Tu 12 Jan 13:30-14:30 HG01.058 Arjen de Vries RU Information Retrieval, or, "Computational Relevance"
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.

Fall 2015 Time Room Speaker Institute Title
Wed 02 Dec 10:00-16:00 HG00.071 Xavier Leroy, Wouter Swierstra, Lars Birkedal, Yves Bertot, Robbert Krebbers Several Workshop on Realistic Program Verification
This is a workshop co-located with Robbert Krebbers' defense. It takes place one day after. Details, abstracts etc. can be found at
Tue 03 Nov 13:30-14:30 HG00.062 Jeffrey O. Shallit U Waterloo Automatic Subsets of Rational Numbers
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.

Fr 23 Oct 13:30-14:30 HG00.058 Bas Spitters Århus U. The cubical set model of homotopy type theory
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.
Tue 20 Oct 13:30-14:30 HG02.028 Hans Zantema TUE/RU Comparing streams by finite state transducers
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.

Spring 2015 Time Room Speaker Institute Title
Wed 17 jun 13:30-14:30 HG00.068 Vincenzo Ciancia ISTI-CNR, Pisa State variables do not exist
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.
Tue 9 jun 13:30-14:30 HG00.086 Freek Wiedijk RU Formal proof between mathematics and computer science
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.
Tue 2 jun 13:30-14:30 HG00.308 Henning Basold RU Trip report TYPES'15
Tue 26 may 13:30-14:30 HG00.086 Julian Salamanca CWI Regular Varieties of Automata and Coequations
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.
Tue 19 may 13:30-14:30 HG00.308 Thibault Gauthier U. of Innsbruck Combining HOL4 and HOL Light libraries to improve proof advice
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.
Tue 12 may 13:30-14:30 No Seminar
Tue 5 may 13:30-14:30 Bevrijdingsdag
Tue 28 apr 13:30-14:30 HG02.028 Luís Cruz-Filipe Syddansk U. Advances in sorting networks
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.
Tue 21 apr 13:30-14:30 HG00.086 Robin Adams RU A Type Theory for Quantum Computing
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.
Tue 14 apr 13:30-14:30 HG00.086 Henning Basold RU Using Coalgebras to Find the Productive Among the Lazy
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.
Tue 7 apr 13:30-14:30 HG00.058 Twan van Laarhoven RU Indexed equality with the interval type
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.
Tue 31 mar 13:30-14:30 HG00.308 Wouter Geraedts RU Strategy Scheduling for Automated Theorem Provers
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.
Tue 24 mar 13:30-14:30 HG01.028 Matteo Sammartino RU A coalgebraic semantics for causality in Petri nets
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.
Tue 17 mar 13:30-14:30 HG00.108 Bas Joosten TUE/RU On Circuits and Boolean Formulas
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.
Wed 11 mar 11:00-12:00 M1.00.02 Victor Pessers KU Leuven Conceiving a new way of managing mathematical knowledge
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.
Tue 3 mar 13:30-14:30 HG00.086 Hans Zantema TUE/RU Proving non-termination automatically
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.
Tue 24 feb 13:30-14:30 HG00.633 Freek Wiedijk RU The CH2O project: making sense of the C standard
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.
Tue 17 feb Carnaval
Wed 11 feb 11:00-12:00 HG01.060 Cezary Kaliszyk U. of Innsbruck HOL(y)Hammer: Beyond HOL Light
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.
Tue 10 feb 13:30-14:30 HG01.028 Jurriaan Rot LIACS Coalgebraic trace semantics via forgetful logics
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.
Tue 3 feb 13:30-14:30 HG01.028 Sam Staton Cambridge Transition systems over games
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.
Tue 27 jan 13:30-14:30 HG01.029 Daniela Petrisan RU Approximation of Nested Fixpoints -- A Coalgebraic View of Parametric Datatypes
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.
Fall 2014 Time Room Speaker Institute Title
Tue 9 dec 13:30-14:30 HG00.065 Régis Spadotti IRIT Rational trees
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.
Tue 2 dec 14:00-15:00 HG00.065 Prakash Panagaden McGill U. Approximate minimization of weighted automata
Tue 25 nov 13:30-14:30 HG00.065 Konstantinos Mamouras Cornell Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism
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.
Tue 18 nov 13:30-14:30 HG00.065 Henning Basold RU Fibrational Dialgebras as Foundation for Dependent Data Types
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.
Tue 11 nov 14:15-15:15 HG00.137 Robbert Krebbers RU Formalizing C in 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.
Tue 4 nov 13:30-14:30 HG00.065 Herman Geuvers RU/TUE A typed lambda-calculus with call-by-name and call-by-value iteration
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.
Tue 28 oct No seminar
Tue 21 oct 13:30-14:30 HG00.065 Dexter Kozen Cornell NetKAT II: Completeness and Complexity.
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).
Tue 14 oct 13:30-14:30 HG00.065 Dexter Kozen Cornell NetKAT: A Formal System for the Verification of Networks.
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.
Tue 7 oct 13:30-14:30 HG00.065 Helle Hansen RU A Coalgebraic View on PDL and Game Logic.
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.)
Tue 30 sep No seminar
Tue 23 sep No seminar
Tue 16 sep 13:30-14:30 HG00.065 Freek Verbeek OU/RU EUROMILS: Certification of an industrial Separation Kernel
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.
Tue 9 sep No seminar
Tue 2 sep 13:30-14:30 HG00.071 Hans Zantema TUE/RU Latin Squares with Graph Properties
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.
Tue 26 aug 13:30-14:30 HG00.065 Markus Klinik RU Domains for Algebraic Data Types with Computation Steps
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.
Mon 25 aug 13:30-14:30 HG00.071 Hendrik Tews FireEye Utilisation of formal methods for cyber security at FireEye
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.
Spring 2014 Time Room Speaker Institute Title
Tue 24 jun 13:30-14:30 HG00.065 Robin Adams RU Canonical Logical Frameworks
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.
Tue 17 jun 13:30-14:30 HG00.065 Tonny Hurkens Deloitte Continuation Calculus (Continued): Call by Need and Type by Rule
One can check at, 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.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.
Tue 10 jun 13:30-14:30 HG00.065 Hans Zantema TUE/RU Turtle visualization of morphic streams
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.
Tue 3 jun 13:30-14:30 HG00.065 Herman Geuvers RU/TUE The Church-Scott representation of inductive and coinductive data in typed lambda calculus
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.
Tue 27 may 13:30-14:30 HG00.065 Jaap Boender MDX Verification of Quantum Protocols using Coq
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.
Fri 23 may 13:30-14:30 HG00.065 Wouter Swierstra UU Auto in Agda: Programming proof search
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.
Tue 20 may 13:30-14:30 HG00.065 Peter Schwabe RU Verifying Crypto -- many questions and the beginning of an answer
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.
Thu 15 may 13:30-16:00 HG00.307 Smetsers, Winter, Cosme-Llopez, Rutten Various COIN seminar
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
Tue 13 may No seminar TYPES meeting in Paris
Tue 6 may No seminar Formalization of mathematics in proof assistants workshop in Paris
Tue 29 apr 13:30-14:30 HG00.065 Helle Hansen RU The final deterministic automaton of streams
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.
Fri 25 apr 11:00-12:00 HG00.310 Matteo Sammartino U. of Pisa Coalgebras and automata for nominal calculi
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.
Tue 22 apr 13:30-14:30 HG00.065 Robbert Krebbers RU Separation algebras for C verification in Coq
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.
Wed 16 apr 15:00-16:00 HG00.086 Jasmin Blanchette TU Munich Corecursion in Isabelle/HOL
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
Tue 15 apr 10:00-15:30 LIN 7 Cramer, Schulz, Blanchette, Kuehlwein, Urban Various Workshop on Machine Learning for Automated Reasoning
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
Tue 8 apr 13:30-14:30 HG01.060 Andrew Polonsky VU Toward a decidable formulation of extensional type theory
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.
Tue 1 apr 13:30-14:30 HG01.058 Bram Westerbaan RU Languages of Streams
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ω := { w1 w2 w3 ... : w1, w2, ... in L }

is not Borel!
Tue 25 mar No seminar
Tue 18 mar 13:30-14:30 HG01.028 Josef Urban RU Learning-assisted Theorem Proving with Millions of Lemmas
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.
Tue 11 mar 13:30-14:30 HG01.060 Herman Geuvers RU/TUE Types and Data types in Continuation Calculus and lambda calculus
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.
Tue 4 mar No seminar Carnaval
Tue 25 feb 13:30-14:30 HG01.028 Stephan Spahn RU Towards a general definition of higher inductive types
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.
Tue 18 feb 13:30-14:30 HG00.633 Henning Basold RU Programming on initial algebras/final coalgebras
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.

[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.
Tue 11 feb 13:30-14:30 HG01.028 Daniel Kuehlwein RU Machine Learning for Automated Reasoning
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.
Tue 4 feb 13:30-14:30 HG01.028 Twan van Laarhoven RU Beautiful variable binding with monads
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.
Tue 28 jan 13:30-14:30 HG01.058 No seminar
Tue 21 jan 13:30-14:30 HG01.058 No seminar
Tue 14 jan 14:15-15:15 HG01.058 Alexandra Silva RU Automata learning: a categorical perspective
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.
Tue 7 jan 13:30-14:30 HG00.068 Bram Westerbaan RU Are Topological Spaces Coalgebraic ?
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.
Fall 2013 Time Room Speaker Institute Title
Tue 17 dec 12:30-14:30 Aula Carst Tankink RU Thesis defense
Mon 16 dec 15:45-17:30 HG00.068 Montanari, Bonchi, Caltais Various Symposium PhD defense Georgiana Caltais
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.
Mon 16 dec 10:45-11:45 HG00.308 Makarius Wenzel U. Paris-Sud/LRI Document-oriented Prover Interaction with Isabelle/PIDE
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.
Tue 10 dec 13:30-14:30 HG01.058 No seminar
Tue 3 dec 13:30-14:30 HG01.058 Herman Geuvers RU/TUE Pure Type Systems revisited
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
Tue 26 nov 13:30-14:30 HG01.058 Robbert Krebbers RU An Operational and Axiomatic Semantics for Non-determinism and Sequence Points in C
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.
Tue 19 nov 13:30-14:30 HG00.086 Mark Adams Proof Technologies Cleaning up the Flyspeck Project
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.
Tue 12 nov 13:30-14:30 No seminar (COIN at CWI)
Tue 5 nov 13:30-14:30 No seminar
Tue 29 oct 13:30-14:30 HG02.702 Freek Wiedijk RU (Co)verifying a compiler and a prover: the CakeML project
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.
Tue 22 oct 13:30-14:30 HG02.702 Henning Basold RU (Co)Algebraic Characterisations of Linear Circuits
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.
Tue 15 oct 13:30-14:30 HG02.702 Herman Geuvers RU/TUE (Co)induction and (Co)algebra in Second Order Logic
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.
Tue 8 oct 13:30-14:30 HG02.702 Robbert Krebbers RU Moessner's Theorem: an exercise in coinductive reasoning in Coq
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.
Tue 1 oct 13:30-14:30 HG02.702 Hans Zantema TUE/RU Cycle rewriting
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.
Tue 24 sep 13:30-14:30 HG02.702 James McKinna U. of Edinburgh On the Sato/Pollack/Schwichtenberg/Takafumi "map/skeleton" representation of lambda terms
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.
Tue 17 sep 13:30-14:30 HG02.702 Andrew Polonsky VU Toward a decidable formulation of extensional type theory
Tue 10 sep 13:30-14:30 HG02.702 Niels van der Weide RU The Polynomial Representation of Real Functions
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.
Tue 3 sep 13:30-14:30 HG02.702 Mark Adams Proof Technologies HOL Zero, Unbreakable Theorem Proving and the $100 Bounty
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!
Tue 27 aug 13:30-14:45 HG02.032 (1) Bram Westerbaan RU A Coalgebraic View of ε-Transitions
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.
(2) Michael Nahas RU A New User's Experience with Formal Proof
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.)
Spring 2013 Time Room Speaker Institute Title
Tue 18 jun 13:30-14:30 HG02.702 Robbert Krebbers RU How to build a certified compiler: a look into CompCert
Tue 11 jun 13:45-15:00 HG00.308 Bram Westerbaan RU 0011 -> 111000
Tue 4 jun 13:30-14:30 HG02.028 Bas Spitters RU Modal Type Theory
Tue 21 may 13:30-14:30 HG00.303 Prakash Panagaden McGill U. Stone Duality for Markov Processes
Tue 14 may 13:30-14:30 HG02.028 Bas Spitters RU Real Numbers in Homotopy Type Theory
Tue 7 may 13:30-14:30 HG02.028 Egbert Rijke RU Higher Inductive Types
Tue 30 apr 13:30-14:30 HG02.028 Queen's day
Tue 23 apr 13:30-14:30 HG02.028 No seminar
Tue 16 apr 13:30-14:30 HG02.028 Robbert Krebbers RU Exploring the formal proof of Feit-Thompson
Tue 9 apr 14:30-15:30 HG01.029 Josef Urban RU AI over Large Formal Knowledge Bases: The First decade
Tue 2 apr 13:30-14:30 HG02.028 Herman Geuvers
Tue 26 mar 13:30-14:30 HG02.028 No seminar (Freek Verbeek's defense in the Aula, see also symposium next day)
Tue 19 mar 13:30-14:30 HG02.028 No seminar
Tue 12 mar 13:30-14:30 HG02.028 Freek Wiedijk RU Should proof assistants be used to verify absence of overflow?
Tue 5 mar 13:30-14:30 HG02.028 No seminar (COIN at CWI)
Tue 26 feb 13:30-14:30 HG02.028 Evgeni Makarov RU Separation Logic for a Functional Language
Tue 19 feb 13:30-14:30 HG02.028 Daniel Gebler VU Compositionality of Approximate and Metric Bisimulation in Probabilistic Transition Systems
Tue 12 feb 13:30-14:30 HG02.028 No seminar
Tue 5 feb 13:30-14:30 HG02.028 No seminar
Tue 29 jan 13:30-14:30 HG02.028 Josef Urban RU BliStr: The Blind Strategymaker
Tue 22 jan 13:30-14:30 HG02.032 Herman Geuvers RU De Bruijn's ideas on the Formalization of Mathematics
Tue 15 jan 13:30-14:30 HG02.028 Henning Basold CWI Co-Banach - How to avoid something
Fall 2012 Time Room Speaker Institute Title
Tue 11 dec 13:30-14:30 HG02.028
Tue 11 dec 13:30-14:30 HG02.028
Tue 4 dec 13:30-14:30 HG02.028 Jasmin Blanchette TU Munchen Foundational, Compositional (Co)datatypes for Higher-Order Logic (Category Theory Applied to Theorem Proving)
Tue 27 nov 13:35-15:00 HG02.028 Egbert Rijke and Bas Spitters RU In homotopy type theory, do hsets form a predicative topos?
Tue 20 nov 13:30-14:30 HG01.058 Robbert Krebbers RU Separation Logic for Non-local Control Flow
Tue 13 nov 13:30-14:30 No seminar
Tue 6 nov 13:30-14:30 HG02.028 Carst Tankink RU Editing programs, editing proofs - A guided tour
Tue 30 oct 13:30-14:30 HG03.054 Helle Hvid Hansen RU Brzozowski revisited: minimal language acceptors via dual adjunctions
Tue 23 oct 13:30-14:30 HG03.054 Egbert Rijke and Bas Spitters RU In homotopy type theory, do hsets form a predicative topos?
Tue 16 oct 13:30-14:30 HG03.054 Andrew Polonski RU Turing-complete typed systems of arithmetic
Tue 9 oct 13:30-14:30 HG03.054 Herman Geuvers RU Extracting a search algorithm from a classical proof
Tue 2 oct 13:30-14:30 HG03.054 Alexandra Silva RU Brzozowski's algorithm (co)algebraically
Tue 25 sep 13:30-14:30 HG03.054 Tessa Matser RU The Curry-Howard isomorphism for classical logic
Tue 18 sep 15:00-16:00 HG01.060 Hans Zantema TUE/RU Cinderella and the wicked Stepmother, or how to avoid overflow
Wed 22 aug 14:30-15:30 HG02.028 Cezary Kaliszyk U. of Innsbruck Initial Experiments with External Provers and Premise Selection on HOL Light Corpora
Spring 2012 Time Room Speaker Institute Title
Tue 19 jun 15:30-17:30 HG00.071 Jade Alglave U. of Oxford Fences in Weak Memory Models
Tue 19 jun 10:45-11:45 HG02.702 Dexter Kozen Cornell U. Program constructs for non-well-founded computation
Tue 12 jun 10:45-11:45 HG02.702 Michael Beeson San Jose State U. Triangle Tiling
Tue 5 jun 10:45-11:45 No seminar (COIN on Monday)
Tue 29 may 10:45-11:45 HG02.702 Freek Wiedijk RU tba
Tue 22 may 10:45-11:45 No seminar
Tue 15 may 10:45-11:45 HG02.702 Andrew Polonski RU Church-Rosser via Standardization
Tue 8 may 10:45-11:45 No seminar
Tue 1 may 10:45-11:45 No seminar
Tue 24 apr 10:45-11:45 HG02.702 Pieter Collins Maastricht U. Validated Function Calculus and Applications to Hybrid Systems
Tue 17 apr 10:45-11:45 HG02.702 Robbert Krebbers RU A call-by-value λ-calculus with lists and control
Tue 10 apr 10:45-11:45 HG02.702 Jelle Herold RU
Tue 3 apr 10:45-11:45 HG02.702 Carst Tankink RU Point-and-write: documenting formal proof by reference
Tue 27 mar 10:45-11:45 HG02.702 Cyril Cohen INRIA A construction of the discrete field of real algebraic numbers in Coq
Tue 20 mar 10:45-11:45 HG01.029 Bas Spitters RU From computational analysis to thoughts about analysis in Homotopy type theory
Tue 13 mar 10:45-11:45 HG02.702 Freek Wiedijk RU The next generation of proof assistants: ten questions
Tue 6 mar 10:45-12:15 HG02.702 Ken Madlener RU Mathematical Operational Semantics in Coq
Tue 28 feb 10:45-12:15 HG02.702 Steffen van Bakel Imperial College London, UK (Classical) Logic and the Pi Calculus
Tue 21 feb 10:45-12:15 HG02.702 No seminar
Tue 14 feb 10:45-12:15 HG02.702 Freek Verbeek OU/RU Using ACL2 for the Formal Verification of on-Chip Communication Fabrics
Tue 7 feb 10:45-12:15 HG02.702 Henk Barendregt RU From Mind to Turing to Mind
Tue 31 jan 10:45-12:15 HG01.029 Bas Joosten OU Effective Layered Verification of Networks-on-Chips
Mon 23 jan 13:30-16:00 HG00.086 seminar merged with COIN on Monday
Tue 17 jan 15:45-17:00 HG02.028 Hans Zantema TUE/RU Type preservation and confluence in simply typed lambda calculus by abstract reduction techniques
Fall 2011 Time Room Speaker Institute Title
Tue 20 dec 15:45-17:00 HG02.028 No seminar
Tue 13 dec 15:45-17:00 HG01.028 Josef Urban RU ATP and Presentation Service for Mizar
Tue 6 dec 15:45-17:00 HG02.028 No seminar (Sinterklaas)
Tue 29 nov 15:45-17:00 HG02.028 Hans Zantema TUE/RU Type preservation in simply typed lambda calculus by abstract reduction techniques
Tue 22 nov 15:45-17:00 HG02.028 Joerg Endrullis / Dimitri Hendriks VU Equational Reasoning and Bisimulation in Coq
Tue 15 nov 15:45-17:00 HG02.028 No seminar (ICT.Open)
Tue 8 nov 15:45-17:00 HG02.028 Wouter Swierstra (organizer) RU Collective exploration of the VSTTE 2012 Software Verification Competition
Tue 1 nov 15:45-17:00 HG02.028 James McKinna Autumn leaves from Shonan Village
Tue 25 oct 15:45-17:00 HG02.028 No seminar
Tue 18 oct 15:45-17:00 HG02.028 Carst Tankink RU Proofs are Documents, and Movies too!
Tue 11 oct 15:45-17:00 HG02.028 Robbert Krebbers RU Formalizing the C99 Standard
Tue 4 oct 15:45-17:00 HG02.028 Wouter Swierstra RU From math to machine: a formal derivation of an executable Krivine machine
Tue 27 sep 15:45-17:00 HG02.028 Jesse Alama New U. of Lisbon Generalizing Theorems of the Mizar Mathematical Library by Type Promotion and Property Omission
Tue 20 sep 15:45-17:00 HG02.028 Bas Joosten RU Ampersand
Tue 13 sep 15:45-17:00 HG02.028 Sebastian Reichelt RU Ideas for a MathWiki Editor
Tue 6 sep 15:45-17:00 No seminar
Tue 30 aug 15:45-17:00 HG02.028 Lionel Mamane RU Dependencies in Coq
Spring 2011 Time Room Speaker Institute Title
Tue 21 jun 15:45-17:00 HG02.028 Andrew Polonsky VU The failure of the range property for the lambda theory H
Tue 17 may 15:45-17:00 HG02.028 Twan van Laarhoven RU Lenses: viewing and updating data structures in Haskell
Tue 10 may 13:30-15:30 HG02.028 Rudolf Mak; Joost Winter TUE; CWI streams seminar Periodic-Drop-Take Calculus for Stream Transformers; Context-free languages and streams
Tue 03 may No seminar (meivakantie)
Tue 26 apr 15:45-17:00 HG00.065 Carst Tankink RU MathWiki and Proviola
Tue 19 apr 15:45-17:00 HG02.028 No seminar
Tue 12 apr No seminar
Tue 05 apr 15:45-17:00 HG02.028 Pierre Letouzey PPS/INRIA Modular Extension of the Arithmetic Libraries in Coq
Tue 29 mar 15:45-17:00 HG02.028 Wouter Swierstra RU Adventures in Extraction Verifying XMonad
Tue 22 mar 15:45-17:00 HG02.028 Robbert Krebbers RU Computer certified efficient exact reals in Coq
Tue 15 mar No seminar
Tue 08 mar No seminar (Carnaval)
Tue 01 mar 15:45-17:00 HG02.028 Bas Joosten U. Twente/RU SMT for Abstract Polyhedra
Tue 22 feb 10:30-12:30 HG00.023 Frits Dannenberg; Franz Staals TU Delft; TUE streams seminar Toeplitz substitutions and transducer equivalence; Stream equality in Coq
Tue 15 feb 15:45-17:00 HG02.028 Wouter Swierstra (TBC) RU Agda Tutorial
Tue 08 feb 15:45-17:00 HG02.028 Daniel Kuhlwein RU The Naproche project
Tue 01 feb 15:30-17:00 HG02.028 Sebastian Reichelt The HLM project
Tue 25 jan 13:30-15:30 HG02.032 Wieb Bosma RU streams seminar: Automatic Sequences
Tue 18 jan 15:30-16:45 HG02.028 Josef Urban RU trip report: AMS Special Session on Formal Mathematics for Mathematicians
Fall 2010 Time Room Speaker Institute Title
Tue 21 dec No seminar (Kleene Coalgebra Day)
Thu 16 dec 15:30-17:00 HG00.308 Jakob Rehof Dortmund Finite Combinatory Logic with Intersection Types
Tue 14 dec 15:30-16:45 HG02.028 Henk Barendregt RU Five Easy Pieces, pt II
Tue 07 dec 15:30-16:45 HG02.028 Jesse Alama New U. of Lisbon Fine-grained mathematical justifications
Tue 30 nov 15:30-16:45 HG02.028 No seminar
Tue 30 nov 13:30-15:30 HG00.065 Wouter Swierstra/Diana Koenraadt streams seminar: Stream Fusion/Equality and unicity by bisimulation
Tue 23 nov No seminar
Tue 16 nov 15:30-16:45 HG00.058 Josef Urban RU A Wiki for Mizar etc.
Tue 09 nov 15:30-16:45 HG00.058 Giulio Manzonetto RU Resource Calculi II: Full Abstraction for Resource Calculus with Tests
Tue 02 nov 15:30-16:45 HG00.058 Robbert Krebbers RU afstudeerpraatje: Classical logic, control calculi and data types
Mon 01 nov 13:30-15:30 HG00.065 Herman Geuvers/Eelis vd Weegen RU streams seminar: Representations of real numbers
Tue 26 oct No seminar
Tue 19 oct 15:30-16:45 HG00.058 Hans Zantema TUE CS in the Mathematical Olympiads
Tue 12 oct 15:30-16:45 HG00.058 Kasper Brink RU Dependently Typed Grammars
Tue 05 oct 15:30-16:45 HG01.058 Henk Barendregt RU Five Easy Pieces, pt I
Mon 04 oct 13:30-15:30 HG00.065 Joerg Endrullis/Hans Zantema TUE streams seminar: Tools proving equality of streams
Tue 28 sep 15:30-16:45 HG01.058 Giulio Manzonetto RU Resource Calculi: some syntax, some semantics
Tue 21 sep No seminar
Wed 15 sep 15:30-16:45 HG00.062 Iris Loeb VU The Layers of Tarski's Foundations of the Geometry of Solids
Tue 14 sep 15:30-16:45 HG01.028 Wouter Swierstra RU The Logic of Interaction
Mon 06 sep 13:30-15:30 HG00.065 Jan Rutten/Milad Niqui RU/CWI streams seminar: Stream differential equations
Spring 2010 Time Room Speaker Institute Title
Tue 13 jul No seminar (papers at ITP/UITP@FLoC, Edinburgh)
Tue 06 jul 15:30-16:45 HG03.082 Olha Shkaravska RU Univariate Polynomial Solutions of Nonlinear Polynomial Recurrence Relations
Tue 29 jun No seminar
Tue 22 jun 15:30-16:45 HG03.082 Cezary Kaliszyk TUM Multiple binders in Nominal Isabelle
Mon 21 jun 14:00-16:00 HG02.028 Bas Spitters RU streams seminar: Quantification over streams
Tue 15 jun 15:30-16:45 HG03.082 Thomas Forster DPMMS, Cambridge Two roots of typing in mathematics
Tue 08 jun 15:30-16:45 HG03.082 James McKinna RU Realisability in Chambery: trip report
Tue 01 jun No seminar
Tue 25 may No seminar
Tue 18 may 15:30-16:45 HG03.082 Peter Hancock MSP group, Strathclyde no-holds barred induction-recursion
Mon 17 may 14:00-16:00 HG02.028 Peter Hancock MSP group, Strathclyde streams seminar: Streams from a type-theoretic perspective
Tue 11 may 15:30-16:45 HG01.058 James McKinna RU Type inference in context: Algorithm W, revisited
Tue 04 may No seminar (meivakantie)
Tue 27 apr No seminar
Tue 20 apr streams seminar: Klop, Hendricks, Endrullis
Tue 13 apr No seminar
Tue 06 apr No seminar (FLoC deadlines)
Tue 30 mar 15:30-16:45 HG01.058 Bas Spitters RU Spitters and vd Weegen, ptIII
Tue 23 mar 15:30-16:45 HG01.058 Bas Spitters RU Spitters and vd Weegen, ptII
Tue 16 mar 15:30-16:45 HG01.058 Bas Spitters RU The algebraic hierarchy using type classes in type theory ptI
Tue 09 mar not assigned yet
Tue 02 mar 15:30-16:45 HG01.058 Josef Urban RU Mizar, Automated Reasoning, and Artificial Intelligence (part 2)
Tue 23 feb 15:30-16:45 HG01.058 Jesse Alama Centro de Inteligência Artificial, Universidade nova de Lisboa Expressibility of some properties of finite combinatorial polyhedra in FOL and extensions
Tue 16 feb No seminar (Carnaval)
Tue 09 feb 15:30-16:45 HG01.058 Josef Urban RU ISLA 2010 and Mizar workshop talk
Tue 02 feb 15:30-16:45 HG01.058 Herman Geuvers RU Deduction modulo
Fall 2009 Time Room Speaker Institute Title
Tue 08 dec 15:30-16:45 HG01.058 Robbert Krebbers RU Typing in simple type theory a la Newman
Tue 17 nov 15:30-16:45 HG01.058 Hans Zantema TUE, RU Computational power of RNA-editing
Tue 10 nov No seminar
Tue 03 nov No seminar (onderzoekvisitatie)
Tue 28 oct No seminar (herfstvakantie)
Tue 21 oct 15:30-16:45 HG01.058 Bas Spitters RU Numerical integration in Coq and ForMath
Tue 14 oct 15:30-16:45 HG01.058 Freek Wiedijk RU report on Dagstuhl seminar Two faces of deduction
Wed 07 oct 15:30-16:45 HG02.032 Cezary Kaliszyk TUM Lifting type properties to properties of equivalence classes in Isabelle/HOL
Tue 06 oct 15:30-16:45 Gymnasion GN2 O'Connor jury various O'Connor Symposium
Mon 05 oct 13:30-14:30 Aula Russell O'Connor McMaster U. thesis defence
Tue 29 sep 15:30-16:45 HG01.058 Freek Wiedijk RU rehearsal: Dagstuhl talk Two automation challenges
Tue 22 sep 15:30-16:45 HG01.058 Allan van Hulst RU A Mizar Formalisation of the Schroeder-Bernstein Theorem in a weak Set Theory
Tue 15 sep 15:30-16:45 HG01.058 Herman Geuvers RU Trip report on CSL 2009
Tue 08 sep 15:30-16:45 HG01.058 Lionel Elie Mamane Gestman, Debian,, L² Transfinite Technologies, ... Trip report on DML2009 workshop
Tue 01 sep 15:30-16:45 HG01.058 Freek Wiedijk RU Trip report on TPHOLs2009 and ITP workshop