University of Leicester


Webpage for Special Events and Guests

Special events

Visit of Michael Hauhs

21st Sept - 2nd Oct 2015: Michael Hauhs (Bayreuth) visits to work with Alexander Kurz on coalgebraic aspects of ecological modelling.

Visit of Sabine Frittella

20-31 July 2015: Sabine Frittella (Delft) visits to work with Alexander Kurz and Samuel Balco on the muddy children in Isabelle.

Visit of Andrew Moshier

4-17 July 2015: Andrew Moshier (Chapman University, Orange, California) visits Alexander Kurz and is joined by Achim Jung from Birmingham to work on Domain Theory and Stone Duality.

Visit of Matej Dostal

9th - 20th December 2014: Matej Dostal (Prague, Czech Republic). Matej will give a mini course on exactness for algebras enriched over categories (following Bourke and Garner) and about HSP theorems in this setting.

Visit of Guiseppe Greco

29th September - 3rd October 2014: Giuseppe Greco (TU Delft, The Netherlands).

Visit of Daniela Petrisan

22nd - 26th September 2014: Daniela Petrisan (ENS Lyon, France) visits Alexander Kurz, Paula Severi, Fer-Jan de Vries.

Visit of Andrew Moshier

21st - 28th August 2014: Andrew Moshier (Chapman University, Orange, California) visits Alexander Kurz and is joined by Achim Jung from Birmingham to work on Domain Theory and Stone Duality.

Visit of Marta Bilkova and Jiri Velebil

12th - 14th May 2014: Marta Bilkova (Academy of Sciences of the Czech Republic) and Jiri Velebil (Czech Technical University in Prague).

Visit of Antonino Salibra

26th Jan - 31st Jan 2014: Antonino Salibra (Universita Ca'Foscari Venezia) visits Fer-Jan de Vries, Paula Severi, and Alexander Kurz. Antonino will also give a course on Lambda Calculus between Algebra and Topology, see slides.

Seminar programme

  • Mon, 27th Jan 2014, 13:15 in G4 (Host: Alexander Kurz)
    Antonino Salibra (Universita Ca'Foscari Venezia)
    Topology: Scott, Selinger, Visser, Priestley

  • Tue, 28th Jan 2014, 12:00 in G4 (Host: Alexander Kurz)
    Antonino Salibra (Universita Ca'Foscari Venezia)
    Algebras: Stone, Boole and Church

  • Wed, 29th Jan 2014, 12:30 in G4 (Host: Alexander Kurz)
    Antonino Salibra (Universita Ca'Foscari Venezia)
    The lambda-calculus is algebraic

  • Thu, 30th Jan 2014, 13:00 in G4 (Host: Alexander Kurz)
    Antonino Salibra (Universita Ca'Foscari Venezia)
    Separability: Selinger, Coleman, Kearnes, Sequeira

Visit of Tomoyuki Suzuki

24th Nov - 7 Dec 2013: Tomoyuki Suzuki (Academy of Sciences, Prague) comes to work with Emilio Tuosto and Alexander Kurz on Nominal Automata.

Visit of Sabine Frittella and Giuseppe Greco

11th Nov - 22nd Nov 2013: Sabine Fritella (Marseille) and Giuseppe Greco (Delft) come to work with Alexander Kurz on proof theory of dynamic logics.

Seminar on Enriched Coalgebraic Logic

20th June, 2013: Talks from our guest Toby Wilkinson (Southampton) and the local crew: Octavian Babus, Daniela Petrisan, Alexander Kurz.

Visit of Viktor Winschel

29th April - 10th May 2013: Viktor is an economist from the University of Mannheim (Germany) with a keen interest in the semantics of programming languages and coalgebra. During his visit we will explore connections between coalgebra and game theory, following work by Lescanne and Abramsky and Winschel.

Visit of Pierre Lescanne

7th/8th Feb 2013: Pierre is known for his work in lambda calculus and rewriting, but is also pioneering the use of coinduction and theorem proving in game theory, see eg his articles in arXiv. Pierre will give a departmental seminar and join more informal discussions on his work.

Visit of Alexander Knapp

28th Jan - 1st Feb 2013: Alexander Knapp is a software engineer from Augsburg, Germany. He will give a departmental seminar and work with us on verification and epistemic logic.

Visit of Ana Sokolova

13th Dec - 14th Dec 2012: Ana Sokolova (Salzburg) comes to explain to us her very interesting result that the algebras for the subdistribution monad are finitely presentable if they are finitely generated. This technical result has some potentially interesting consequences for probabilistic transition systems. The intention is to look at some details of the proof. We will meet on the 13th at 2pm in G4.

Visit of Matej Dostal

10th Dec - 14th Dec 2012: Matej Dostal (Prague) comes again, this time for only a week, to discuss his recent work on many-valued coalgebraic logic.

Visit of Guiseppe Greco

3rd Dec - 14th Dec 2012: Guiseppe, a proof theorist from Amsterdam, comes for two weeks to work with us on display calculi for dynamic epistemic logic.

Visit of Alexandra Silva

29-30 Nov 2012: Alexandra Silva from Nijmegen comes to explain us her recent work on coalgebraic automata, to discuss nominal automata, and to give a departmental seminar.

Visit of Alessandra Palmigiano

30th Oct- 2nd Nov 2012: Alessandra Palmigiano (Amsterdam) will come to work with us on the algebraic semantics of dynamic epistemic logic and to give a departmental seminar.

Workshop on Nominal Sets

On the occasion of Daniela Petrisan's PhD defence, we will have a workshop on nominal sets, jointly organised by Roy Crole, Alexander Kurz, and Andrei Murawski.

Seminar programme

Seminar details

Finitary nominal subsets and nominal domain theory

Andrew Pitts (Cambridge)
Nov 23, 2011, 14:00 in G4

A key concept underlying the research programme of Mikolaj Bojanczyk et al on "Nominal Computation" (LICS 2011, POPL 2012) turns out to coincide with one introduced (for quite different purposes) by David Turner in his PhD thesis "Nominal domain theory for concurrency" (Univ. Cambridge 2009). Let me explain...

Games with names

Nikos Tzevelekos (Queen Mary London)
Nov 24, 2011, 9:00 in G4

This talk is about formal techniques for reasoning about names which have emerged in the last years. We will focus on game semantics, and in particular nominal game semantics. The latter constitutes a fresh strand of the theory, founded on nominal sets of Gabbay and Pitts, which provides models for programming languages with new resources such as fragments of ML. Moreover, nominal game models can be given algorithmic representations by means of newly introduced abstract machines, called Fresh- Register Automata, which operate on infinite alphabets of names.

Accepting Language with Names

Emilio Tuosto (Leicester)
Nov 24, 2011, 10:45 in G4

We consider how languages over infinite alphabets can be represented in terms of nominal sets. We propose a variant of History-Dependent Automata for recognising such languages. We introduce the notion of language-accepting history-dependent automata over infinite alphabets and study their expressiveness relating them to existing formalisms for languages over infinite alphabets, in particular to the recently introduced Fresh-Register Automata.

Visit of Adriana Balan

12th Dec - 16th Dec 2011: Adriana Balan will work with us on coalgebraic logic over posets.

A visit of Fredrik Nordvall Forsberg

Seminar programme

Seminar details

Data types in dependent type theory: inductive-inductive definitions

Fredrik Nordvall Forsberg (Department of Computer Science, University of Swansea)
Nov 3, 2011, 11:00 in G4

Martin-Löf's dependent type theory is both a foundational framework for constructive mathematics and a functional programming language with a very rich type system. Of course, we want this language to have a rich notion of data structure as well. I will review some classes of data types (indexed inductive types, inductive-recursive types, inductive-inductive types, ...) that one can add to dependent type theory, especially focusing on inductive-inductive definitions and their axiomatisation and categorical semantics.

Note that Fredrik's talk will be a continuation of an earlier one he will give at our PhD seminar

A visit of Rob Myers

Seminar programme

Seminar details

Rational Coalgebraic Machines in Varieties

Rob Myers (IC London)
Oct 24, 2011, 15:00 in G4

Note this is an unathorized abstract by Alexander

Rob Myers thesis not only generalises and conceptually explains the important work of Bonsangue, Rutten and Silva on generalized Kleene theorems. It also breaks new ground in several important ways.

First, this is the first time different notions of presentations of functors have been systematically investigated and related to the existence and properties of algorithms (such as satisfiability and bisimilarity checking).

Second, the thesis shows how—moving from Set-functors to functors on varieties of algebras—it is possible to increase the computational power of the machines which are described by coalgebras. The important conceptual insight that makes this possible is to replace the finite set of states of the traditional set-based machines by infinite but finitely presentable algebras.

Visit of Matei Dostal

Oct - Dec 2011: Matej Dostal is a student of Jiri Velebil from Prague and comes to work with us many-valued coalgebraic logic.

A visit of dr Yoshihito Tanaka

Seminar programme

Seminar details

Conservativity of Boolean algebras with operators over semilattices with operators

dr Yoshihito Tanaka (Kyushu Sangyo University)
August 11, 2011, 14:00 in G4

(joint work with A. Kurucz, F. Wolter and M. Zakharyaschev)

An extended abstract of Yoshihito's talk is here and slides are here.

The problems considered in this paper originate in recent applications of large scale ontologies in medicine and other life sciences. The profile OWLEL of the OWL Web Ontology Language, used for this purpose, is based on the description logic EL. The syntactic terms of EL, called concepts, are interpreted as sets in first-order relational models. Concepts are constructed from atomic concepts and constants for the whole domain and empty set using intersection and existential restrictions. From a modal logic point of view, concepts are modal formulas constructed from propositional variables and the constants top, bottom using conjunction and diamonds.

An EL-theory is a set of inclusions (or implications) between such concepts, and the main reasoning problem in applications of EL in life sciences is to decide whether an EL-theory entails a concept inclusion when interpreted over a class of relational structures satisfying certain constraints on its binary relations. Standard constraints in OWLEL are transitivity and reflexivity, for which reasoning in EL is PTime-complete, as well as symmetry and functionality, for which reasoning is ExpTime-complete.

As in modal logic, apart from reasoning over relational models, one can try to develop a purely syntactical reasoning machinery using a calculus. In other words, we can define a more general algebraic semantics for EL: the underlying algebras are bounded meet-semilattices with monotone operators (SLOs, for short), constraints are given by equational theories of SLOs, and the reasoning problem is validity of quasi-equations in such equational theories. The resulting more general entailment problem is not necessarily complete with respect to the `intended' relational semantics. This paper presents our initial results in an attempt to clarify which equational theories of SLOs are complete in this sense and which are not. We also prove that the completeness problem---given a finitely axiomatised equational theory of SLOs, decide whether it is complete with respect to the relational semantics---is algorithmically undecidable, which establishes a principle limitation regarding possible answers to our research question.

A visit of Sam Van Gool and Dion Coumans

July 5-7, 2011: Sam Van Gool and Dion Coumans from the Radboud Universiteit Nijmegen, will give both a PhD seminar and we're going to have our regular Domain Theory, Coalgebras and Dualities seminar with them.

London-Leicester Coalgebra Meeting

Seminar programme

  • June 24, 2011, 11:00 in ATT LT3
    Thorsten Altenkirch (Nottingham)
    Higher order Eating or How to eliminate function types

  • June 24, 2011, 11:40 in ATT LT3
    M. Andrew Moshier (Chapman University, Orange, USA)
    Coalgebraic logic for stably compact spaces

  • June 24, 2011, 12:20 in ATT LT3
    Tadeusz Litak (Leicester)
    Coalgebraic Predicate Logic: First Steps

  • June 24, 2011, 14:00 in ATT LT3
    Lutz Schröder (Bremen, Germany)
    Coalgebraic logic for knowledge representation and reactive systems

  • June 24, 2011, 15:15 in ATT LT3
    Sam Staton (Cambridge)
    Intuitionistic modal frames

  • June 24, 2011, 15:30 in ATT LT3
    Paul Blain Levy (Birmingham)
    Similarity quotients as final coalgebras

  • June 24, 2011, 16:30 in ATT LT3
    Rob Myers (Imperial College London)
    Rational Coalgebraic Machines on Varieties

  • June 24, 2011, 17:00 in ATT LT3
    Björn Lellmann (Imperial College London)
    A Doodling Calculus - Can We Draw Conclusions?

  • June 24, 2011, 17:30 in ATT LT3
    Clemens Kupke (Imperial College London)
    Minimal automata via duality

  • June 24, 2011, 18:00 in ATT LT3
    Nick Bezhanishvili (Imperial College London)
    Duality for Vietoris coalgebras on compact Hausdorff spaces

  • June 24, 2011, 18:30 in ATT LT3
    Daniela Petrişan (Leicester)
    Stone Duality in Nominal Sets

Seminar details

Coalgebraic logic for stably compact spaces

M. Andrew Moshier (Chapman University, Orange, USA)
June 24, 2011, 11:40 in ATT LT3

With the notable exception of Moss's treatment of coalgebraic logic for measurable spaces, most of the literature on coalgebraic logic takes the intended semantics to be coalgebras in the category Set. That is, the state spaces are discrete, and the logics are classical. And yet, we know that the duals of Boolean algebras are Stone spaces, and hence are not discrete. We also know that a satisfactory treatment of probabilistic transitions will need to deal with non-discrete spaces in order to capture distributions other than the finitely supported ones.

This talk builds coalgebraic logic for Stone spaces, spectral spaces, compact Hausdorff spaces and stably compact spaces in one go, in that precisely the same machinery is used in all four cases to obtain coalgebraic logics for suitable functors. In particular, in each case we define a dcpo of logics tailored to the desired category of state spaces, and show that the coalgebraic logic asssociated to a functor is the least fixpoint of a related Scott continuous function. One pleasant by-product of this approach is that in order to get the right dcpos, the logics must be equipped with a proof theoretic notion of entailment. Thus one can ask about soundness and completeness. We show that the resulting logics are indeed sound and complete for "strong entailment", as well as being expressive (bisimilarity is captured by agreement on formulas). For many functors this also yields decidability of entailment.

Coalgebraic Predicate Logic: First Steps

Tadeusz Litak (Leicester)
June 24, 2011, 12:20 in ATT LT3

I will discuss our recent work with Dirk Pattinson and Katsuhiko Sano on the right correspondence language for coalgebras, i.e., the coalgebraic counterpart of predicate logic. As it turns out, the invention can be traced back to a relatively unknown paper by C.C Chang. I begin with some examples of properties expressible in the new language. Later on, I discuss its relationship with the modal language and more powerful coalgebraic languages and briefly sketch how to prove its completeness for some general classes of functors and predicate liftings. I conclude outlining open questions and directions for future research.

Coalgebraic logic for knowledge representation and reactive systems

Lutz Schröder (Bremen, Germany)
June 24, 2011, 14:00 in ATT LT3

Lutz's talk was also our External Seminar for this week. Please see our External Seminar webpage.

The slides of Lutz's talk are here.

Modal logic is currently one of the most successful logical formalisms in computer science, in particular through its role as the basis for temporal logics on the one hand, and for description logics on the other hand. While modal logics are standardly equipped with a relational semantics, many modes of expression found both in knowledge representation and in the more detailed modelling of reactive systems, in particular where these involve uncertainty or multiple agents, require substantial extensions or modifications of relational semantics. Coalgebraic logic serves as a unified semantic and algorithmic framework for such modalities. We give an introduction to coalgebraic logic and then present a specific result on timed-out tableaux for coalgebraic fixed point logics (joint work with Yde Venema) in more detail.

Similarity quotients as final coalgebras

Paul Blain Levy (Birmingham)
June 24, 2011, 15:30 in ATT LT3

The slides of Paul's talk are here.

We give a general framework connecing a branching time relation on nodes of a transition system to a final coalgebra for a suitable endofunctor. Examples of relations treated by our theory include bisimilarity, similarity, upper and lower similarity for transition systems with divergence, similarity for discrete probabilistic systems, and nested similarity. Our results describe firstly how to characterize the relation in terms of a given final coalgebra, and secondly how to construct a final coalgebra using the relation.

Our theory uses a notion of ``relator'' based on earlier work of Thijs. But whereas a relator must preserve binary composition in Thijs' framework, it only laxly preserves composition in ours. It is this weaker requirement that allows nested similarity to be an example.

Rational Coalgebraic Machines on Varieties

Rob Myers (Imperial College London)
June 24, 2011, 16:30 in ATT LT3

The slides of Rob's presentation are here.

A visit of dr Yoshihito Tanaka

Seminar programme

Seminar details

On infinitary connectives in modal logic

dr Yoshihito Tanaka (Kyushu Sangyo University)
January 26, 2011, 14:00 in G4

The talk was an overview of dr Tanaka's work in infinitary and predicate modal/superintuitionistic logic. In particular, we focused on the use of Rasiowa-Sikorski Lemma in completeness proofs: a subject recurrent in several papers of dr Tanaka. The last part was devoted to his more recent work on generalization of Yankov formulas in infinitary setting. Slides are here. Yoshihito also took part in the B'ham-Le'ster seminar next day and we devoted a part of it to Rasiowa-Sikorski Lemma.

A visit of dr Katsuhiko Sano

Oct 2010 - Jan 2011: We are proud that the philosopher and modal logician Katsuhiko Sano will visit and work with us on coalgebraic logic.

Workshop on Nominal Algebra and Nominal Techniques

Note that the schedule is approximate and subject to change depending on speakers' preferences. Presentations will take place from Tuesday to Thursday between 14:00 and 17:00 in ATT SB2.07: Attenborough Seminar Block Second Floor LR SB2.07. Also, please note that Jamie Gabbay will give a departmental seminar on Friday.

Seminar programme

Seminar details

Automata and languages with names and binders

dr Vincenzo Ciancia (ILLC, University of Amsterdam)
1 June 2010, 14:00 in ATT SB2.07

We present the results of a preliminary investigation on a theory of automata with names. The recognised languages are (nominal) sets of strings over an alphabet with names. More expressive power is obtained by adding the ability to bind names along transitions. These nominal automata can be represented in two ways: either as coalgebras over the nominal sets by Gabbay and Pitts, or as history dependent automata (Montanari-Pistore). Using the latter, more compact representation, we can allocate names over a loop. This results in a "finite memory effect" which is made formal by proving that the finite memory automata of Kaminski and Francez can be encoded as history-dependent automata. It turns out that the recognized languages have an implicit notion of symmetry, which can be used to compress large, symmetric data-sets, by representing groups of permutations using their generators. Joint work with Emilio Tuosto.

Towards Nominal Formal Languages

dr Emilio Tuosto (University of Leicester)
1 June 2010, starting sometime between 15:30 and 16:00 depending on the agreed length of the coffee break in ATT SB2.07

We introduce formal languages with binders based on nominal algebras so to characterise classes of nominal formal languages with respect to different types of binders in a uniform way. More precisely, we show initial nominal monoids, which are monoids on nominal algebras, of typical classes of nominal languages, and axiomatise them in a hierarchy of all nominal monoids. Moreover, we extend history dependent automata (HD-automata) by adding stack, and study the recognisability of nominal languages. This is a joint work with Alexander Kurz and Tomoyuki Suzuki.

A one-and-a-halfth order first-order truth

dr Murdoch J. Gabbay (Heriot-Watt University)
2 June 2010, 14:00 in ATT SB2.07

Boolean algebras capture truth-values of classical logic; Heyting algebras capture truth-values of intuitionistic logic; cylindric algebras capture truth-values of predicate logic. I will discuss a (nominal) algebraic presentation of one-and-a-halfth order logic which, it has been proved, also captures truth values in predicate logic, using nominal algebra. I will briefly sketch nominal algebra and speculate that this nominal algebraic presentation is a useful and natural algebraic notion of truth-value to use in the study of predicate logic. I hope to stimulate discussion on how to turn this speculation into proper research papers. See also the one-and-a-halfth order logic paper.

Algebraic Theories over Nominal Sets

dr Alexander Kurz (University of Leicester)
2 June 2010, starting sometime between 15:30 and 16:00 depending on the agreed length of the coffee break in ATT SB2.07

(joint work with D. Petrişan and J. Velebil) Nominal sets were introduced by Gabbay/Pitts. Two different notions of equational logic over nominal sets were studied by Gabbay/Mathijssen and Clouston/Pitts. In this talk, we introduce the general notion of a based monad and show that finitary based monads give rise to equational theories in the standard sense of many-sorted set-based universal algebra. We further show that restricting these many-sorted equational theories to `uniform' ones brings us back to the equational logics of Gabbay/Mathijssen and Clouston/Pitts. A benefit of our approach is that it allows to apply known results from universal algebra to algebras over nominal sets.

Encoding graph transformation in intuitionistic linear logic

dr Paolo Torrini (University of Leicester)
3 June 2010, 14:00 in ATT SB2.07

Graph transformation (GT) is a modelling technique based on the representation of states as graphs (or hyper-graphs) and transitions as application of transformation rules. In the DPO algebraic approach, a rule is represented as a span of total graph morphisms, and its application as a double pushout diagram. We have tried to give a formalisation of DPO-GT using intuitionistic linear logic (ILL). ILL allows for a straightforward encoding of DPO-GT at a basic propositional level. In order to deal with rule pattern matching and in particular with renaming associated to injective morphisms, we have introduced a resource-bound existential quantifier that has some features of freshness quantification --- though generally weaker and lacking self-duality.

The paper is based on a joint paper with Reiko Heckel.

Click here to read the full abstract with more background

Uniform theories categorically

Daniela Petrişan (University of Leicester)
3 June 2010, quite likely 15:00 in ATT SB2.07

(ongoing work with A. Kurz and J. Velebil) In this talk we'll have a closer look at the uniform theories introduced in this paper on universal algebra over nominal sets. I will discuss several attempts to define and characterize uniform theories at a more conceptual level.

A one-and-a-halfth order logic, in principle?

dr Tadeusz Litak (University of Leicester)
3 June 2010, quite likely 16:00 in ATT SB2.07

I will discuss to what extent classical algebraic logic (Tarskian-Hungarian style) can be thought of as a one-and-a-halfth-order logic in Jamie Gabbay's sense. Those who attended our AQSN seminar series so far should be familiar with most of the contents of this mostly improvised talk.

Author: Tadeusz Litak (tml12 if_you're_a_spambot_this_underlined_part_is_to_confuse_you at, T: +44 (0) 116 252 2593.
© University of Leicester 12 Feb 2010. Last modified: 23rd September 2015, 15:14:29
Informatics Web Maintainer. This document has been approved by the Head of Department.