University of Leicester

informatics

STAFF — Alexander Kurz  Maitrise d'Informatique (Universite de Grenoble), Dipl.-Inform. (TU München), Dr.rer.nat. (LMU München)

Professor
F2 Computer Science Building
Department of Informatics,
University of Leicester,
University Road,
Leicester,
LE1 7RH.

T: +44 (0) 116 252 5356
E: ak155 at le ac uk

Publications. (not always uptodate ... see also dblp and arxiv.)


Research (this section is under construction)

My main area of research is in the mathematical foundations of computer science. This includes creating novel mathematics, but also applications of existing mathematics to computer science. Moreover, I am increasingly interested in how this `computer science mathematics' can be applied to other areas, from theoretical physics to economics and the social sciences.

  • Mathematical Foundations of Computer Science and Applications to Software Engineering

    Most of my work applies logic and/or category theory to mathematical problems that arise from applications in software engineering. Typically, the long-term aim is to develop formal methods that support the specification of software and sometimes its formal verification.

    Since the mathematical foundations of software engineering are not yet as well-developped as those for other engineering disciplines, substantial work in pure mathematics is still required. To this end, I pursue research in modal logic, Stone duality, coalgebras, domain theory, order-enriched category theory, nominal techniques, proof theory ... . Much of this could be described as being pure mathematics, with thinking up definitions and proving theorems being the main activity. But I am also interested in tool development based on proof assistants such as Isabelle and based on automated methods such as tableau procedures.

    Some topics I am currently working on:

    • Coalgebraic logic. Currently, I am interested in the question of how the considerable achievements in coalgebraic logic can be extended to quantitative logics in a systematic way. One direction we explore is to use enriched category theory in order to move from sets via posets to metric spaces, inspired by the general ideas outlined in (Lawvere 1973). As it turned out, there is a lot of interesting work to do and there is still a long way to go. So far we have been working to
      1. move the full duality based framework from sets to preorders/posets (with results on expressiveness, Moss's nabla or the cover modality, duality). This also made it necessary to add to the theory of ordered algebras.
      2. move the coalgebraic side of the story from posets to generalised metric spaces (with results on the many-valued cover modality and extensions of functors from Set to V-cat )
      3. move the algebraic side of the story from posets to metric spaces. Here the difficulty is that while over sets and posets we have a canonically associated propositional logic in the form of Boolean algebras and distributive lattices, this is not the case anymore for metric spaces. We have some results on on the logic of generalised metric spaces, but more remains to be done.
      This is being developed in collaboration with many colleagues and collaborators including Octavian Babus, Marta Bilkova, Adriana Balan, Fredrik Dahlqvist, Daniela Petrisan, and Jiri Velebil.
    • Multi-type display calculi. This started for me with Alessandra Palmigiano's quest for an algebraic semantics of dynamic epistemic logic and Giuseppe Greco joining in to tackle the question of how a good proof theory of dymaic epistemic logic might look like. Our solution to the problem revealed the mult-type structure behind epistemic logic, which was one of the topics of Sabine Frittella's phd thesis. A prototype implementation in Isabelle with a full formalisation of the muddy children puzzle has been done in collaboratio with my PhD student Samuel Balco. For more work on multi-type display calculi see the publication of the applied logic group at Delft.
    • Nominal sets and nominal automata. A standard idea in category theory is to move notions from one category to another. Of particular interest to computer science is the move from sets to nominal set (see here and here for more). This move is interesting both from a semantics and from an algorithm perspective.
      1. From a semantic perpsective, it allows us to build datatypes quotiented by alpha equivalence (= upto renaming of bound variables) but maintaining principles of induction and coinduction. The point of view of Stone duality was taken up, in joint work with Jamie Gabbay, by my (at that time) research associate Tadeusz Litak and PhD student Daniela Petrisan in a paper and Daniela's phd thesis. Jamie then pushed this much further to reveal a new and beautiful mathematical landscape.
      2. From an algorithm point of view, we can look at models of computation in the category of nominal sets. For example, the natural notion of a deterministic finite nominal automaton operates with a finite set of "nominal states", where each nominal state is an equivalence class of infinitely many classical states. This increases the power of computation as we explored in the case of regular languages with binders. For the state of the art of this research direction, I recommend the work of Bartek Klin and his colleagues (search for papers with "nominal" in the title).
    • Domain Theory. Together with Drew Moshier and Achim Jung, we have a purely categorical construction of how to extend a zero-dimensional Stone duality to one for Hausdorff spaces. We build on previous work on duality for relations such as Kegelmann's thesis. We also make use of the fact that in the poset-enriched situation the relation lifting can be equally computed via tabulation and via cotabulation. While the overall process may conceptually be not surprising to the expert, there are many details to sort out and we hope to publish them over the coming year.
    • ...
  • Applications of `computer science mathematics' outside of computer science.

    There always has been a close interaction between mathematics and physics, to the extent that one could call certain areas of mathematics such as calculus and probability theory as `physics maths'. On the other hand, more recently, computer scientists have been developing a body of mathematics of quite a distinct flavour which, for the purpose of comparison, I will call`computer science maths'.

    The basic premise of my interests described in the following is that while `physics maths' found many applications outside physics (most notably, perhaps, in economics but also in many other social sciences), the same cannot yet be said of `computer science maths'. Which indicates plenty of research opportunities for a computer scientist.

    In the opposite direction, questions from outside of computer science are posing new challenges to computer scientists: There is both the question of how technology affects society and the question of whether technological solutions might contribute to solve social problems. For example, to design the software for online courts is not a purely technical problem. In the other direction, research on security and algorithms may have an impact on topics such as voting and democracy. Developments in social media, internet of things, artificial intelligence and virtual reality will lead to a future in which social and technical aspects are inextricably intertwined. Let us be prepaired.

    While I am interested in general how computer science interacts with society, I am also interested in finding concrete research projects motivated by this interaction.

    Two of the areas in which I see research opportunities are the following.
    • Logicians have been developing bespoke logics for a large variety of reasoning tasks (time, knowledge, believes, obligations, probabilities, actions, etc). These logics have found applications largely in computer science, but should be relevant also in other fields. In order to make them available to researchers without special training in maths and computer science, it is important to develop scalable proof systems and automated reasoners that can be combined in a flexible way and be used by domain experts that do not have a training in logic. On the proof theoretic side, this lead Alessandra Palmigiano, Giuseppe Greco, Sabine Frittella and myself to the work on multi-type display logics. This gives us a flexible framework to study how different logics interact and how they can be combined in a systematic way.
    • Already in their famous monograph, von Neumann and Morgenstern raise the problem that economic game theory does not scale up to real world situations. An exciting recent development, initiated by Viktor Winschel, proposes to use methods from functional programming, program semantics and category theory in order to give a compositional account of game theory. This uses ideas of Martin Escardo and Paolo Oliva and has been deeply investigated in Jules Hedges PhD thesis. For a recent paper see Compositional Game Theory by Ghani, Hedges, Winschel and Zahn.

    Leicester provides an excellent environment to develop these and similar research directions as there are a number of interdisciplinary initiatives, for example, IQSCS (Quantum Social and Cognitive Science), CAMEo (Cultural and Media Economies), Econophysics Network, Agent Based Modelling Reading Group, Computational Social Science Network, Seminar on Category Theory and its Applications.



For some years, we have been running informal seminars around categories/logic/semantics. Thanks to Tadeusz Litak, there is a webpage. Since he left to Erlangen it is maintained only irregularly.


Grants.


Some Events (I am planning to go to or support otherwise or simply want to advertise)

AiML 2018: Advances in Modal Logic. Bern, Switzerland, 27-31 August 2018.

TbiLLC 2017: 12th Tbilisi Symposium on Language, Logic and Computation. 18-22 September, 2017, in Kakheti, Georgia.

MFCS 2017: 42nd International Symposium on Mathematical Foundations of Computer Science. August 21-25, 2017, Aalborg (Denmark).

WoLLIC 2017: 24th Workshop on Logic Language Information and Computation. July 18-21, 2017, University College London.

TACL 2017: 8th conference on Topology, Algebra, and Categories in Logic. Prague, June 26–30, 2017.

MFPS+CALCO: 33rd Conference on the Mathematical Foundations of Programming Semantics and 7th Conference on Algebra and Coalgebra in Computer Science. 12-16 June, 2017, Ljubljana, Slovenia.

ALCOP VIII: Algebra and Coalgebra meet Proof Theory. University of Strathclyde, 10-12 April 2017.

MGS 2017: Midlands Graduate School in the Foundations of Computing Science. 9-13 April 2017, University of Leicester.

Dynamics in Logic IV, October 29th, 2016.

Logics, Decisions, and Interactions, Lorentz Center, 24 Oct 2016 through 28 Oct 2016.

AiML 2016: Advances in Modal Logic. 30 Aug - 2 Sep 2016, Budapest, Hungary.

Mini workshop on applications of machine learning and data mining. Leicester, 10th of June, 2016.

MGS 2016. Birmingham, 11 - 15 April, 2016.

Algebra and Coalgebra meet Proof Theory ALCOP VII. Vienna, Austria, April 7–9, 2016.

CMCS 2016. Eindhoven, the Netherlands, 2 - 3 April 2016.

Logics for Social Behaviour 3. 8 - 11 February 2016, ETH Zurich.

Workshop on EFFICIENT AND NATURAL PROOF SYSTEMS. Bath, 14-16 December, 2015.

TRENDS IN LOGIC XV, 2015: Logics for Social Behaviour. Delft, 29 June 2015 to 3 July 2015.

CALCO 2015. 6th Conference on Algebra and Coalgebra in Computer Science, Nijmegen 24-26 June, 2015.

MGS 2015. Sheffield, April 7-11, 2015.

BEYOND 2014. December 03-05, 2014 - University of Florence - Italy.

Lorentz Center Workshop Logics for Social Behaviour. 10 Nov 2014 through 14 Nov 2014. Notes, slides, etc

AiML 2014. Groningen, August 5-8, 2014.

ALCOP 2014. Algebra and Coalgebra meet Proof Theory, 15 - 16 May 2014.

MGS 2014. Nottingham, 22-26 April 2014.



Former events


Author: Alexander Kurz (ak155 at le ac uk), T: +44 (0) 116 252 5356.
© University of Leicester. Last modified: 31st May 2017, 08:04:01.
Informatics Web Maintainer. Any opinions expressed on this page are those of the author.