Webpage for Special Events and GuestsSpecial eventsVisit of Michael Hauhs21st Sept  2nd Oct 2015: Michael Hauhs (Bayreuth) visits to work with Alexander Kurz on coalgebraic aspects of ecological modelling.Visit of Sabine Frittella2031 July 2015: Sabine Frittella (Delft) visits to work with Alexander Kurz and Samuel Balco on the muddy children in Isabelle.Visit of Andrew Moshier417 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 Dostal9th  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 Greco29th September  3rd October 2014: Giuseppe Greco (TU Delft, The Netherlands).Visit of Daniela Petrisan22nd  26th September 2014: Daniela Petrisan (ENS Lyon, France) visits Alexander Kurz, Paula Severi, FerJan de Vries.Visit of Andrew Moshier21st  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 Velebil12th  14th May 2014: Marta Bilkova (Academy of Sciences of the Czech Republic) and Jiri Velebil (Czech Technical University in Prague).Visit of Antonino Salibra26th Jan  31st Jan 2014: Antonino Salibra (Universita Ca'Foscari Venezia) visits FerJan de Vries, Paula Severi, and Alexander Kurz. Antonino will also give a course on Lambda Calculus between Algebra and Topology, see slides.Seminar programme
Visit of Tomoyuki Suzuki24th 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 Greco11th 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 Logic20th June, 2013: Talks from our guest Toby Wilkinson (Southampton) and the local crew: Octavian Babus, Daniela Petrisan, Alexander Kurz.Visit of Viktor Winschel29th 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 Lescanne7th/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 Knapp28th 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 Sokolova13th 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 Dostal10th Dec  14th Dec 2012: Matej Dostal (Prague) comes again, this time for only a week, to discuss his recent work on manyvalued coalgebraic logic.Visit of Guiseppe Greco3rd 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 Silva2930 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 Palmigiano30th 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 SetsOn 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 detailsFinitary nominal subsets and nominal domain theory
Andrew Pitts (Cambridge)
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...
Nikos Tzevelekos (Queen Mary London)
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.
Emilio Tuosto (Leicester)
We consider how languages over infinite alphabets can be represented in terms of nominal sets.
We propose a variant of HistoryDependent Automata for recognising such languages. We introduce the
notion of languageaccepting historydependent automata over infinite alphabets and study their
expressiveness relating them to existing formalisms for languages over infinite alphabets, in particular to
the recently introduced FreshRegister Automata.
Visit of Adriana Balan12th Dec  16th Dec 2011: Adriana Balan will work with us on coalgebraic logic over posets.A visit of Fredrik Nordvall ForsbergSeminar programme
Seminar detailsData types in dependent type theory: inductiveinductive definitions Fredrik Nordvall Forsberg (Department of Computer Science, University of Swansea) MartinLö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, inductiverecursive types, inductiveinductive types, ...) that one can add to dependent type theory, especially focusing on inductiveinductive 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 MyersSeminar programme
Seminar detailsRational Coalgebraic Machines in Varieties Rob Myers (IC London) 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 Setfunctors 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 setbased machines by infinite but finitely presentable algebras.
Visit of Matei DostalOct  Dec 2011: Matej Dostal is a student of Jiri Velebil from Prague and comes to work with us manyvalued coalgebraic logic.A visit of dr Yoshihito TanakaSeminar programme
Seminar detailsConservativity of Boolean algebras with operators over semilattices with operators dr Yoshihito Tanaka (Kyushu Sangyo University) (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 firstorder 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 ELtheory 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 ELtheory 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 PTimecomplete, as well as symmetry and functionality, for which reasoning is ExpTimecomplete. 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 meetsemilattices with monotone operators (SLOs, for short), constraints are given by equational theories of SLOs, and the reasoning problem is validity of quasiequations 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 problemgiven a finitely axiomatised equational theory of SLOs, decide whether it is complete with respect to the relational semanticsis algorithmically undecidable, which establishes a principle limitation regarding possible answers to our research question.
A visit of Sam Van Gool and Dion CoumansJuly 57, 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.
LondonLeicester Coalgebra MeetingSeminar programme
Seminar detailsCoalgebraic logic for stably compact spaces M. Andrew Moshier (Chapman University, Orange, USA) 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 nondiscrete 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 byproduct 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) 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) 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 timedout tableaux for coalgebraic fixed point logics (joint work with Yde Venema) in more detail.
Similarity quotients as final coalgebras Paul Blain Levy (Birmingham) 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) The slides of Rob's presentation are here. A visit of dr Yoshihito TanakaSeminar programme
Seminar detailsOn infinitary connectives in modal logic dr Yoshihito Tanaka (Kyushu Sangyo University)
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 RasiowaSikorski 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'hamLe'ster seminar next day and we devoted a part of it to RasiowaSikorski Lemma.
A visit of dr Katsuhiko SanoOct 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 TechniquesNote 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 detailsAutomata and languages with names and binders dr Vincenzo Ciancia (ILLC, University of Amsterdam)
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 (MontanariPistore).
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 historydependent automata.
It turns out that the recognized languages have an implicit notion of
symmetry, which can be used to compress large, symmetric datasets,
by representing groups of permutations using their generators.
Joint work with Emilio Tuosto.
Towards Nominal Formal Languages dr Emilio Tuosto (University of Leicester)
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 (HDautomata)
by adding stack, and study the recognisability of nominal languages.
This is a joint work with Alexander Kurz and Tomoyuki Suzuki.
A oneandahalfth order firstorder truth dr Murdoch J. Gabbay (HeriotWatt University)
Boolean algebras capture truthvalues of classical logic; Heyting
algebras capture truthvalues of intuitionistic logic; cylindric
algebras capture truthvalues of predicate logic. I will discuss a
(nominal) algebraic presentation of oneandahalfth 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 truthvalue 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 oneandahalfth
order logic paper.
Algebraic Theories over Nominal Sets dr Alexander Kurz (University of Leicester)
(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 manysorted setbased universal algebra. We further
show that restricting these manysorted 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) Graph transformation (GT) is a modelling technique based on the representation of states as graphs (or hypergraphs) 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 DPOGT using intuitionistic linear logic (ILL). ILL allows for a straightforward encoding of DPOGT 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 resourcebound existential quantifier that has some features of freshness quantification  though generally weaker and lacking selfduality. 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)
(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 oneandahalfth order logic, in principle? dr Tadeusz Litak (University of Leicester)
I will discuss to what extent classical algebraic logic (TarskianHungarian style) can be thought of as a oneandahalfthorder 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 mcs.le.ac.uk), T: +44 (0) 116 252 2593. 