— Alexander Kurz Maitrise d'Informatique (Universite de Grenoble), Dipl.-Inform. (TU München), Dr.rer.nat. (LMU München)
F2 Computer Science Building|
Department of Informatics,
University of Leicester,
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
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.
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.
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 )
- 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.
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
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.
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
- 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
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
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
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
Agent Based Modelling Reading Group, Computational
Social Science Network, Seminar on Category Theory and its Applications.
- 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.
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.
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.