Please contact the organizers , Niels van der Weide or Freek Wiedijk in case you are interested in giving a talk.
Winter 2018  Time  Room  Speaker  Institute  Title 

Fr 26 Jan  10:3011: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 downwardclosed under the subsumption (linearisation) order.

Tu 16 Jan  13:3014: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:3015: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 ``Kuratowskifinite type'' and ``Kuratowskifinite subobject'', which we contrast with established notions, e.g. Bishopfinite types and enumerated types. We argue that Kuratowskifiniteness 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 wellknown finite set implementations such as tree and listlike 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:3014:30  HG00.310  Guillaume Allais  RU  A ScopeandType 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 wellscopedness and sometimes even welltypedness.
However the user still has to write a lot of boilerplate code to get
common scopeandtype safe programs (e.g. renaming, substitution,
normalisation by evaluation, or various compilation passes) and the
proofs that they are wellbehaved.
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 genericsyntax. 
Th 16 Nov  15:0016:00  HG00.065  SvenBodo Scholz  HeriotWatt University  A LambdaCalculus 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 / listbased setting.

Tu 14 Nov  13:3014:30  HG01.057  Niels van der Weide  RU  The ThreeHITs 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:3014:30  HG00.633  Henning Basold  CNRS, ENS de Lyon  A Recursive Logic for the Equivalence of InductiveCoinductive
Programs
In this talk, I will present a logic the behavioural equivalence of
inductivecoinductive 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 selfreferences
would temper with the soundness of the proof system. In the presented
system, this will be achieved by using the socalled 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 backreferences. 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:3014:30    Cancelled     
Tu 18 April  11:3012:30    Easter     
Tu 4 April  11:3012:30  HG00.310  Guillaume Allais  RU  A Library of Total Parser Combinators
Parser combinator libraries represent parsers as functions and, using higherorder functions, define a DSL of combinators allowing users to quickly put together programs capable of handling complex grammars. When moving to total functional languages such as Agda, these programs cannot be directly ported: there is nothing in the original definitions guaranteeing termination. In this talk, we will introduce a 'guarded' modal operator acting on types and show how it allows us to give more precise types to existing combinators thus guaranteeing totality. The resulting library is available online together with various usage examples at https://github.com/gallais/agdarsec . 
Tu 21 Feb  13:3014: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:3014: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 SpoilerDuplicator 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
nonconformance between an implementation and specification.
Moreover, I will show how we can generalise and parameterise our
SpoilerDuplicator 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:3014: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:3014: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 CantorRussellTuringGö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:3014: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 (n1)^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 (n1)^2, refuting Trahtman's conjecture. For n > 4 we prove that none of the known examples admit nontrivial extensions keeping the same smallest synchronizing word length (n1)^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:3014:30  HG00.023  Robbert Krebbers  Delft University of Technology  Interactive Proofs in HigherOrder 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 nonspatial) named proof contexts for the object logic. Thanks to these contexts we have been able to implement highlevel 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 higherorder 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 finegrained concurrent algorithms. This is joint work with Amin Timany and Lars Birkedal. 
Spring 2016  Time  Room  Speaker  Institute  Title 
Tu 19 Jul  13:3014:30  HG00.086  Rik de Kort  RU  A TypeTheoretic 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 callbyvalue lambda calculus.

Tu 14 Jun  13:3014:30  HG00.086  Niels van der Weide  RU  Higher Inductive Types
In type theories like MartinLö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 nontrivial 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:3014: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 "ifthenelse".
We show that, if we also have "false" and "true",
"ifthenelse" is functionally complete for constructive
proposition logic.
Our procedure also yields new rules for wellknown
connectives that — as we will argue — are better
than the wellknown 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:3014: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 nondeterministic 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:3014:30  HG01.028  Henk Don  RU  The Cerny conjecture and 1contracting 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 1contracting 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 1contracting automata. The talk will not require any specific knowledge about automata, I will just start from the basics. 
Tu 29 Mar  13:3014:30  HG01.058  João Pizani  Universiteit Utrecht  ΠWare: A Hardware Description Language embedded in Agda
In this talk we will introduce ΠWare, a DomainSpecific
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
*typesafe* 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 semanticspreserving circuit transformations.
Considering the tradition enjoyed by the study of coalgebras
in Nijmegen, we also present our simple coalgebraic
semantics for stateful circuits, with some corresponding
examples and correctness proofs.
Further information and accompanying code can be found at http://piware.alvb.in. 
Tu 22 Mar  13:3014: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:3014:30  HG01.028  Michiel de Bondt  RU  Solving Mahjong Solitaire boards with peeking
We first prove that solving Mahjong Solitaire boards with
peeking is NPcomplete, even if one only allows isolated
stacks of the forms 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 ShisenSho with peeking. 
Tu 26 Jan  13:3014: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:3014: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:0016:00  HG00.071  Xavier Leroy, Wouter Swierstra, Lars Birkedal, Yves Bertot, Robbert Krebbers  Several  Workshop on Realistic Program Verification
This is a workshop colocated with Robbert Krebbers'
defense.
It takes place one day after.
Details, abstracts etc. can be found at
http://robbertkrebbers.nl/verification_workshop/.

Tue 03 Nov  13:3014: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
kautomatic 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 kautomatic 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:3014:30  HG00.058  Bas Spitters  Århus U.  The cubical set model of homotopy type theory
Homotopy Type Theory refers to a new interpretation of
MartinLö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
homotopyinvariant 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:3014: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 preorder the smallest streams are the ultimately
periodic streams.
The structure of streams with respect to this preorder
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:3014:30  HG00.068  Vincenzo Ciancia  ISTICNR, 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., objectorientation, cryptograpy, serviceoriented 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:3014: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:3014:30  HG00.308  Henning Basold  RU  Trip report TYPES'15 
Tue 26 may  13:3014: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 BallesterBolinches, CosmeLlopez, 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:3014: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. AIATP 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 knowledgesharing 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:3014:30  No Seminar  
Tue 5 may  13:3014:30  Bevrijdingsdag  
Tue 28 apr  13:3014:30  HG02.028  Luís CruzFilipe  Syddansk U.  Advances in sorting networks
Sorting networks are a very simple model of dataindependent 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 computerscience has led to a number
of computerassisted proofs of new results about sorting networks during
the last two years.

Tue 21 apr  13:3014: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:

Tue 14 apr  13:3014: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 upto 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 upto 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:3014: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:3014: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 learningbased 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 ATPtuning 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 CASCJ7, 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 CADE25 and is pending review. 
Tue 24 mar  13:3014:30  HG01.028  Matteo Sammartino  RU  A coalgebraic semantics for causality in Petri nets
Petri Nets are a wellknown 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 settheoretic 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 infinitelymany
states and transitions, but an equivalent, finitelybranching model can
be derived, which admits a minimal, often finitestate, representative.
Then we recast these models in a categorytheoretical 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 TuriPlotkin 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 wellbehaved category of coalgebras. Our coalgebraic model is
still infinitestate, 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 settheoretical compact
model. Remarkably, state reduction is automatically performed along the
equivalence.

Tue 17 mar  13:3014: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:0012: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
wellorganized. 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 wikimodel 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:3014:30  HG00.086  Hans Zantema  TUE/RU  Proving nontermination automatically
Over the years many techniques and strong tools have been developed
for automatically proving termination of rewrite systems.
For proving nontermination 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 nontermination follows from the existence of a nonempty 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 nontermination. By this technique nontermination 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:3014: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 nontrivial support library. The CH2O project has two abstract Clike 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:0012:00  HG01.060  Cezary Kaliszyk  U. of Innsbruck  HOL(y)Hammer: Beyond HOL Light
Learningassisted automated reasoning systems provide a toolchain
for automatically proving theorems in ITPs. This toolchain consists of
proof translation, premise selection and proof reconstruction. The
HOL(y)Hammer system has implemented such a toolchain 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:3014: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:3014: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 lambdacalculus. This is joint work with Paul Levy, presented at CSLLICS 2014. http://www.cs.ru.nl/~sstaton/papers/lics2014games.pdf 
Tue 27 jan  13:3014: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 nontermination and infinite data) and on the other hand
2categorical (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 manysorted
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:3014: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:0015:00  HG00.065  Prakash Panagaden  McGill U.  Approximate minimization of weighted automata 
Tue 25 nov  13:3014: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 noncompositional formalism of safety games on finite graphs. We
present sound and complete Hoarestyle 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:3014: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 setbased 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:1515: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.

Tue 4 nov  13:3014:30  HG00.065  Herman Geuvers  RU/TUE  A typed lambdacalculus with callbyname and callbyvalue iteration
We define a simply typed lambda calculus with positive recursive types in
which we study the less wellknown 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 "callbyname iterator" and
a "callbyvalue iterator" with appropriate reduction rules. We show that
the calculus is strongly normalizing.

Tue 28 oct  No seminar  
Tue 21 oct  13:3014: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 packetswitching model. I will also discuss
the coalgebraic theory of NetKAT and present the
bisimulationbased decision procedure for the equational
theory from Foster et al. (POPL 2015).

Tue 14 oct  13:3014: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 softwaredefined networking.

Tue 7 oct  13:3014: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 PDLlike logics for Tcoalgebras
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:3014: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 onboard computers. As
these systems must be able to control safetycritical 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
onboard 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
noninterference 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:3014: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:3014: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 embeddingprojection 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:3014: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 operatingsystem 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:3014: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 typechecking 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 onetime 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 wellbehaved 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: thirdorder logical frameworks behave very differently from secondorder logical frameworks. This difficulty may show that we do not understand the most wellstudied features of type theories as well as we think we do. 

Tue 17 jun  13:3014:30  HG00.065  Tonny Hurkens  Deloitte  Continuation Calculus (Continued): Call by Need and Type by Rule
One can check at
http://www.cs.ru.nl/~herman/ccalc, that the CC program
goto.E → E twice.G.E → G.(G.E) evaluates the term twice.(twice.goto).end in 7 steps to end. It contains two terms of the form twice.goto.E which evaluate in 3 steps to Z. A Call by Need evaluation avoids this as follows:
CC terms do not use lambdaabstraction (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 muabstraction to define recursive types. Just like in simply typed lambda calculus, each type is either


Tue 10 jun  13:3014: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 = selfsimilar behaviour: it contains an upscaled
copy of itself. In the talk we give criteria on turtle curves for being
finite or selfsimilar, providing a guide to generate amazing pictures
that we show for very simple morphic stream definitions. Moreover,
we show how the ThueMorse stream may yield the Koch curve. 

Tue 3 jun  13:3014:30  HG00.065  Herman Geuvers  RU/TUE  The ChurchScott 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
runtime). The much less wellknown 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, coinductive data types,
and we show how programs can be extracted from proofs in second order
predicate logic.


Tue 27 may  13:3014: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 informationtheoretic
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:3014: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 Prologstyle resolution procedure in the
dependently typed programming language Agda. Connecting this
resolution procedure to Agda's reflection mechanism provides a
firstclass proof search tactic for firstorder 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:3014: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 handoptimized 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 handoptimized cryptographic software
written in AMD64 assembly.


Thu 15 may  13:3016:00  HG00.307  Smetsers, Winter, CosmeLlopez, Rutten  Various  COIN seminar
The schedule is as follows:


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:3014: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 kautomatic and
kregular sequences, together with coinductive specification formats in
the form of behavioural differential equations using the zipoperations.


Fri 25 apr  11:0012: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
nonstandard notions of bisimulations, and may yield infinitelybranching
and infinitestate transition systems. These issues have been tackled by
introducing adhoc operational models. In this seminar I will present two
of them, namely coalgebras over presheaves and HistoryDependent Automata.
The former equip coalgebras with name generation capabilities, the latter
are finitestate automata suitable for verification. These models are
tightly related: HDautomata 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:3014:30  HG00.065  Robbert Krebbers  RU  Separation algebras for C verification in Coq
Separation algebras are a wellknown 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:0016: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:0015:30  LIN 7  Cramer, Schulz, Blanchette, Kuehlwein, Urban  Various  Workshop on Machine Learning for Automated Reasoning
Preliminary schedule:


Tue 8 apr  13:3014: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 typeintype 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:
The system has two kinds of substitutions


Tue 1 apr  13:3014: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 contextfree language L of words over {0,1} such that the language of streams L^{ω} := { w_{1} w_{2} w_{3} ... : w_{1}, w_{2}, ... in L } is not Borel! 

Tue 25 mar  No seminar  
Tue 18 mar  13:3014:30  HG01.028  Josef Urban  RU  Learningassisted 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 reused 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 reused in later proofs. We show that in combination with
learningbased 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:3014: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 wellknown 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 6685. 

Tue 4 mar  No seminar  Carnaval  
Tue 25 feb  13:3014: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 Wtypes 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 0constructors (for terms) and
1constructors (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 infinitytopos can be
presented in a way admitting HITs.


Tue 18 feb  13:3014: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 CurryHoward correspondence between logic and programming, we find a relation between, on the one hand, propositions of the μcalculus and their proofs and, on the other hand, fixed point types and terms. For the last link we establish a topology on the sets T (A) of terms of type A. This topology shall specialise to existing topologies (e.g. induced by prefixes in the case of streams). Furthermore we expect that terms t : A → B give rise to continuous maps T (A) → T (B). This establishes the connection to [4, 5] where it is demonstrated how continuous maps on final coalgebras can be programmed. The work presented is still in progress, so some topics are subject to change. References [1] A. Abel and B. Pientka. Wellfounded recursion with copatterns: a unified approach to termination and productivity. In ICFP, 2013. [2] A. Abel, B. Pientka, D. Thibodeau, and A. Setzer. Copatterns: Programming infinite structures by observations. In POPL, 2013. [3] J. Fortier and L. Santocanale. Cuts for circular proofs: semantics and cutelimination. 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:3014: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:3014: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:3014:30  HG01.058  No seminar  
Tue 21 jan  13:3014:30  HG01.058  No seminar  
Tue 14 jan  14:1515: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:3014: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:3014:30  Aula  Carst Tankink  RU  Thesis defense 
Mon 16 dec  15:4517: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 statebased 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 twofold: on the one hand, we obtain a more abstract proof for the wellknown 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 nondeterministic automata. In particular, this approach deals with decorated trace equivalences for labelled transition systems and probabilistic systems and, (the socalled "must" and "may") testing semantics for divergent nondeterministic systems. 
Mon 16 dec  10:4511:45  HG00.308  Makarius Wenzel  U. ParisSud/LRI  Documentoriented Prover Interaction with Isabelle/PIDE
LCFstyle proof assistants like Coq, HOL, and Isabelle have been
traditionally tied to a sequential READEVALPRINT 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 1015 years
ago, prover frontends like Proof General (with its many clones such
as CoqIDE) have perfected this commandline interaction, but left
fundamental questions open. Is interactive theorem proving a
necessarily synchronous and sequential process? Is stepbystep
commandline 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 DocumentModel 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 frontend and prover backend 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 sideconditions. 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 stronglytyped higherorder 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 Isabelle20111 (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 Isabelle20132 (December 2013). Recent improvements revisit the old READEVALPRINT model within the new documentoriented environment, in order to integrate longrunning 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 disprovers 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 frontend that presents itself like wellknown 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:3014:30  HG01.058  No seminar  
Tue 3 dec  13:3014: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:

Tue 26 nov  13:3014:30  HG01.058  Robbert Krebbers  RU  An Operational and Axiomatic Semantics for Nondeterminism 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 sideeffects 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 nondeterminism 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:3014: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 alreadyproved 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:3014:30  No seminar  (COIN at CWI)  
Tue 5 nov  13:3014:30  No seminar  
Tue 29 oct  13:3014: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:3014: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:3014: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 CurryHoward 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 wellknown 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:3014: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 nontrivial 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:3014: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:3014: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 coauthors have
developed a canonical representation of namecarrying lambda terms
based on a novel datastructure for representing binding, the socalled
"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 McKinnaPollack 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:3014:30  HG02.702  Andrew Polonsky  VU  Toward a decidable formulation of extensional type theory 
Tue 10 sep  13:3014: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:3014: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:3014: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 nondeterministic 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 highperformance 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:3014:30  HG02.702  Robbert Krebbers  RU  How to build a certified compiler: a look into CompCert 
Tue 11 jun  13:4515:00  HG00.308  Bram Westerbaan  RU  0011 > 111000 
Tue 4 jun  13:3014:30  HG02.028  Bas Spitters  RU  Modal Type Theory 
Tue 21 may  13:3014:30  HG00.303  Prakash Panagaden  McGill U.  Stone Duality for Markov Processes 
Tue 14 may  13:3014:30  HG02.028  Bas Spitters  RU  Real Numbers in Homotopy Type Theory 
Tue 7 may  13:3014:30  HG02.028  Egbert Rijke  RU  Higher Inductive Types 
Tue 30 apr  13:3014:30  HG02.028  Queen's day  
Tue 23 apr  13:3014:30  HG02.028  No seminar  
Tue 16 apr  13:3014:30  HG02.028  Robbert Krebbers  RU  Exploring the formal proof of FeitThompson 
Tue 9 apr  14:3015:30  HG01.029  Josef Urban  RU  AI over Large Formal Knowledge Bases: The First decade 
Tue 2 apr  13:3014:30  HG02.028  Herman Geuvers  
Tue 26 mar  13:3014:30  HG02.028  No seminar  (Freek Verbeek's defense in the Aula, see also symposium next day)  
Tue 19 mar  13:3014:30  HG02.028  No seminar  
Tue 12 mar  13:3014:30  HG02.028  Freek Wiedijk  RU  Should proof assistants be used to verify absence of overflow? 
Tue 5 mar  13:3014:30  HG02.028  No seminar  (COIN at CWI)  
Tue 26 feb  13:3014:30  HG02.028  Evgeni Makarov  RU  Separation Logic for a Functional Language 
Tue 19 feb  13:3014:30  HG02.028  Daniel Gebler  VU  Compositionality of Approximate and Metric Bisimulation in Probabilistic Transition Systems 
Tue 12 feb  13:3014:30  HG02.028  No seminar  
Tue 5 feb  13:3014:30  HG02.028  No seminar  
Tue 29 jan  13:3014:30  HG02.028  Josef Urban  RU  BliStr: The Blind Strategymaker 
Tue 22 jan  13:3014:30  HG02.032  Herman Geuvers  RU  De Bruijn's ideas on the Formalization of Mathematics 
Tue 15 jan  13:3014:30  HG02.028  Henning Basold  CWI  CoBanach  How to avoid something 
Fall 2012  Time  Room  Speaker  Institute  Title 

Tue 11 dec  13:3014:30  HG02.028  
Tue 11 dec  13:3014:30  HG02.028  
Tue 4 dec  13:3014:30  HG02.028  Jasmin Blanchette  TU Munchen  Foundational, Compositional (Co)datatypes for HigherOrder Logic (Category Theory Applied to Theorem Proving) 
Tue 27 nov  13:3515:00  HG02.028  Egbert Rijke and Bas Spitters  RU  In homotopy type theory, do hsets form a predicative topos? 
Tue 20 nov  13:3014:30  HG01.058  Robbert Krebbers  RU  Separation Logic for Nonlocal Control Flow 
Tue 13 nov  13:3014:30  No seminar  
Tue 6 nov  13:3014:30  HG02.028  Carst Tankink  RU  Editing programs, editing proofs  A guided tour 
Tue 30 oct  13:3014:30  HG03.054  Helle Hvid Hansen  RU  Brzozowski revisited: minimal language acceptors via dual adjunctions 
Tue 23 oct  13:3014:30  HG03.054  Egbert Rijke and Bas Spitters  RU  In homotopy type theory, do hsets form a predicative topos? 
Tue 16 oct  13:3014:30  HG03.054  Andrew Polonski  RU  Turingcomplete typed systems of arithmetic 
Tue 9 oct  13:3014:30  HG03.054  Herman Geuvers  RU  Extracting a search algorithm from a classical proof 
Tue 2 oct  13:3014:30  HG03.054  Alexandra Silva  RU  Brzozowski's algorithm (co)algebraically 
Tue 25 sep  13:3014:30  HG03.054  Tessa Matser  RU  The CurryHoward isomorphism for classical logic 
Tue 18 sep  15:0016:00  HG01.060  Hans Zantema  TUE/RU  Cinderella and the wicked Stepmother, or how to avoid overflow 
Wed 22 aug  14:3015: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:3017:30  HG00.071  Jade Alglave  U. of Oxford  Fences in Weak Memory Models 
Tue 19 jun  10:4511:45  HG02.702  Dexter Kozen  Cornell U.  Program constructs for nonwellfounded computation 
Tue 12 jun  10:4511:45  HG02.702  Michael Beeson  San Jose State U.  Triangle Tiling 
Tue 5 jun  10:4511:45  No seminar  (COIN on Monday)  
Tue 29 may  10:4511:45  HG02.702  Freek Wiedijk  RU  tba 
Tue 22 may  10:4511:45  No seminar  
Tue 15 may  10:4511:45  HG02.702  Andrew Polonski  RU  ChurchRosser via Standardization 
Tue 8 may  10:4511:45  No seminar  
Tue 1 may  10:4511:45  No seminar  
Tue 24 apr  10:4511:45  HG02.702  Pieter Collins  Maastricht U.  Validated Function Calculus and Applications to Hybrid Systems 
Tue 17 apr  10:4511:45  HG02.702  Robbert Krebbers  RU  A callbyvalue λcalculus with lists and control 
Tue 10 apr  10:4511:45  HG02.702  Jelle Herold  RU  
Tue 3 apr  10:4511:45  HG02.702  Carst Tankink  RU  Pointandwrite: documenting formal proof by reference 
Tue 27 mar  10:4511:45  HG02.702  Cyril Cohen  INRIA  A construction of the discrete field of real algebraic numbers in Coq 
Tue 20 mar  10:4511:45  HG01.029  Bas Spitters  RU  From computational analysis to thoughts about analysis in Homotopy type theory 
Tue 13 mar  10:4511:45  HG02.702  Freek Wiedijk  RU  The next generation of proof assistants: ten questions 
Tue 6 mar  10:4512:15  HG02.702  Ken Madlener  RU  Mathematical Operational Semantics in Coq 
Tue 28 feb  10:4512:15  HG02.702  Steffen van Bakel  Imperial College London, UK  (Classical) Logic and the Pi Calculus 
Tue 21 feb  10:4512:15  HG02.702  No seminar  
Tue 14 feb  10:4512:15  HG02.702  Freek Verbeek  OU/RU  Using ACL2 for the Formal Verification of onChip Communication Fabrics 
Tue 7 feb  10:4512:15  HG02.702  Henk Barendregt  RU  From Mind to Turing to Mind 
Tue 31 jan  10:4512:15  HG01.029  Bas Joosten  OU  Effective Layered Verification of NetworksonChips 
Mon 23 jan  13:3016:00  HG00.086  seminar merged with COIN on Monday  
Tue 17 jan  15:4517: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:4517:00  HG02.028  No seminar  
Tue 13 dec  15:4517:00  HG01.028  Josef Urban  RU  ATP and Presentation Service for Mizar 
Tue 6 dec  15:4517:00  HG02.028  No seminar  (Sinterklaas)  
Tue 29 nov  15:4517:00  HG02.028  Hans Zantema  TUE/RU  Type preservation in simply typed lambda calculus by abstract reduction techniques 
Tue 22 nov  15:4517:00  HG02.028  Joerg Endrullis / Dimitri Hendriks  VU  Equational Reasoning and Bisimulation in Coq 
Tue 15 nov  15:4517:00  HG02.028  No seminar  (ICT.Open)  
Tue 8 nov  15:4517:00  HG02.028  Wouter Swierstra (organizer)  RU  Collective exploration of the VSTTE 2012 Software Verification Competition 
Tue 1 nov  15:4517:00  HG02.028  James McKinna  Autumn leaves from Shonan Village  
Tue 25 oct  15:4517:00  HG02.028  No seminar  
Tue 18 oct  15:4517:00  HG02.028  Carst Tankink  RU  Proofs are Documents, and Movies too! 
Tue 11 oct  15:4517:00  HG02.028  Robbert Krebbers  RU  Formalizing the C99 Standard 
Tue 4 oct  15:4517:00  HG02.028  Wouter Swierstra  RU  From math to machine: a formal derivation of an executable Krivine machine 
Tue 27 sep  15:4517: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:4517:00  HG02.028  Bas Joosten  RU  Ampersand 
Tue 13 sep  15:4517:00  HG02.028  Sebastian Reichelt  RU  Ideas for a MathWiki Editor 
Tue 6 sep  15:4517:00  No seminar  
Tue 30 aug  15:4517:00  HG02.028  Lionel Mamane  RU  Dependencies in Coq 
Spring 2011  Time  Room  Speaker  Institute  Title 

Tue 21 jun  15:4517:00  HG02.028  Andrew Polonsky  VU  The failure of the range property for the lambda theory H 
Tue 17 may  15:4517:00  HG02.028  Twan van Laarhoven  RU  Lenses: viewing and updating data structures in Haskell 
Tue 10 may  13:3015:30  HG02.028  Rudolf Mak; Joost Winter  TUE; CWI  streams seminar PeriodicDropTake Calculus for Stream Transformers; Contextfree languages and streams 
Tue 03 may  No seminar  (meivakantie)  
Tue 26 apr  15:4517:00  HG00.065  Carst Tankink  RU  MathWiki and Proviola 
Tue 19 apr  15:4517:00  HG02.028  No seminar  
Tue 12 apr  No seminar  
Tue 05 apr  15:4517:00  HG02.028  Pierre Letouzey  PPS/INRIA  Modular Extension of the Arithmetic Libraries in Coq 
Tue 29 mar  15:4517:00  HG02.028  Wouter Swierstra  RU  Adventures in Extraction Verifying XMonad 
Tue 22 mar  15:4517: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:4517:00  HG02.028  Bas Joosten  U. Twente/RU  SMT for Abstract Polyhedra 
Tue 22 feb  10:3012: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:4517:00  HG02.028  Wouter Swierstra (TBC)  RU  Agda Tutorial 
Tue 08 feb  15:4517:00  HG02.028  Daniel Kuhlwein  RU  The Naproche project 
Tue 01 feb  15:3017:00  HG02.028  Sebastian Reichelt  The HLM project  
Tue 25 jan  13:3015:30  HG02.032  Wieb Bosma  RU  streams seminar: Automatic Sequences 
Tue 18 jan  15:3016: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:3017:00  HG00.308  Jakob Rehof  Dortmund  Finite Combinatory Logic with Intersection Types 
Tue 14 dec  15:3016:45  HG02.028  Henk Barendregt  RU  Five Easy Pieces, pt II 
Tue 07 dec  15:3016:45  HG02.028  Jesse Alama  New U. of Lisbon  Finegrained mathematical justifications 
Tue 30 nov  15:3016:45  HG02.028  No seminar  
Tue 30 nov  13:3015: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:3016:45  HG00.058  Josef Urban  RU  A Wiki for Mizar etc. 
Tue 09 nov  15:3016:45  HG00.058  Giulio Manzonetto  RU  Resource Calculi II: Full Abstraction for Resource Calculus with Tests 
Tue 02 nov  15:3016:45  HG00.058  Robbert Krebbers  RU  afstudeerpraatje: Classical logic, control calculi and data types 
Mon 01 nov  13:3015:30  HG00.065  Herman Geuvers/Eelis vd Weegen  RU  streams seminar: Representations of real numbers 
Tue 26 oct  No seminar  
Tue 19 oct  15:3016:45  HG00.058  Hans Zantema  TUE  CS in the Mathematical Olympiads 
Tue 12 oct  15:3016:45  HG00.058  Kasper Brink  RU  Dependently Typed Grammars 
Tue 05 oct  15:3016:45  HG01.058  Henk Barendregt  RU  Five Easy Pieces, pt I 
Mon 04 oct  13:3015:30  HG00.065  Joerg Endrullis/Hans Zantema  TUE  streams seminar: Tools proving equality of streams 
Tue 28 sep  15:3016:45  HG01.058  Giulio Manzonetto  RU  Resource Calculi: some syntax, some semantics 
Tue 21 sep  No seminar  
Wed 15 sep  15:3016:45  HG00.062  Iris Loeb  VU  The Layers of Tarski's Foundations of the Geometry of Solids 
Tue 14 sep  15:3016:45  HG01.028  Wouter Swierstra  RU  The Logic of Interaction 
Mon 06 sep  13:3015: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:3016:45  HG03.082  Olha Shkaravska  RU  Univariate Polynomial Solutions of Nonlinear Polynomial Recurrence Relations 
Tue 29 jun  No seminar  
Tue 22 jun  15:3016:45  HG03.082  Cezary Kaliszyk  TUM  Multiple binders in Nominal Isabelle 
Mon 21 jun  14:0016:00  HG02.028  Bas Spitters  RU  streams seminar: Quantification over streams 
Tue 15 jun  15:3016:45  HG03.082  Thomas Forster  DPMMS, Cambridge  Two roots of typing in mathematics 
Tue 08 jun  15:3016: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:3016:45  HG03.082  Peter Hancock  MSP group, Strathclyde  noholds barred inductionrecursion 
Mon 17 may  14:0016:00  HG02.028  Peter Hancock  MSP group, Strathclyde  streams seminar: Streams from a typetheoretic perspective 
Tue 11 may  15:3016: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:3016:45  HG01.058  Bas Spitters  RU  Spitters and vd Weegen, ptIII 
Tue 23 mar  15:3016:45  HG01.058  Bas Spitters  RU  Spitters and vd Weegen, ptII 
Tue 16 mar  15:3016: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:3016:45  HG01.058  Josef Urban  RU  Mizar, Automated Reasoning, and Artificial Intelligence (part 2) 
Tue 23 feb  15:3016: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:3016:45  HG01.058  Josef Urban  RU  ISLA 2010 and Mizar workshop talk 
Tue 02 feb  15:3016:45  HG01.058  Herman Geuvers  RU  Deduction modulo 
Fall 2009  Time  Room  Speaker  Institute  Title 

Tue 08 dec  15:3016:45  HG01.058  Robbert Krebbers  RU  Typing in simple type theory a la Newman 
Tue 17 nov  15:3016:45  HG01.058  Hans Zantema  TUE, RU  Computational power of RNAediting 
Tue 10 nov  No seminar  
Tue 03 nov  No seminar  (onderzoekvisitatie)  
Tue 28 oct  No seminar  (herfstvakantie)  
Tue 21 oct  15:3016:45  HG01.058  Bas Spitters  RU  Numerical integration in Coq and ForMath 
Tue 14 oct  15:3016:45  HG01.058  Freek Wiedijk  RU  report on Dagstuhl seminar Two faces of deduction 
Wed 07 oct  15:3016:45  HG02.032  Cezary Kaliszyk  TUM  Lifting type properties to properties of equivalence classes in Isabelle/HOL 
Tue 06 oct  15:3016:45  Gymnasion GN2  O'Connor jury  various  O'Connor Symposium 
Mon 05 oct  13:3014:30  Aula  Russell O'Connor  McMaster U.  thesis defence 
Tue 29 sep  15:3016:45  HG01.058  Freek Wiedijk  RU  rehearsal: Dagstuhl talk Two automation challenges 
Tue 22 sep  15:3016:45  HG01.058  Allan van Hulst  RU  A Mizar Formalisation of the SchroederBernstein Theorem in a weak Set Theory 
Tue 15 sep  15:3016:45  HG01.058  Herman Geuvers  RU  Trip report on CSL 2009 
Tue 08 sep  15:3016:45  HG01.058  Lionel Elie Mamane  Gestman, Debian, cypherpunks.lu, L² Transfinite Technologies, ...  Trip report on DML2009 workshop 
Tue 01 sep  15:3016:45  HG01.058  Freek Wiedijk  RU  Trip report on TPHOLs2009 and ITP workshop 