STyLo — Semantics, Types and Logic

The STyLo team is part of the Theory Cluster of the Leiden University. The work of the team revolves around correctness of systems by construction, and the verification and analysis of systems.

To implement systems that fulfil desired properties by construction, one needs languages that statically guarantee these properties. We focus on using type systems, since they enable compositional reasoning. An understanding of the induced behaviour of such languages is gained through their semantics, which we develop with tools from category theory and other areas of mathematics. Interestingly, the same tools that we use to construct and analyse type systems can also be used as the foundation of logical deduction systems. Such deduction systems underlie the verification and analyis of systems, both in the form of computer-assisted proofs and in automatic deduction. We choose to focus on compositional and computer-assisted reasoning because they are key to handling the complexity of constructing and analysing large systems.

Logic and computation are inseparable strands, if viewed through the right lens. In the STyLo team, we use category theory, type theory and language semantics as such lenses to structure our work and gain new insights in how the strands can be developed. The benefit of using and developing abstract theories is that these are readily applicable to systems in various areas of, for example, computer science, physics, biology and chemistry.

Seminar

We have group seminar, which has a separate page with details.

Current Members

Current Students

  • Rakesh Kumar: Isomorphism Theorems for Diffeological Groupoids (Bsc.)
  • Carlos Eduardo Moreira Mendes: Empirical Bounds on Random Graph Colorings using Markov Chains Monte Carlo Simulations (Bsc.)
  • Kimberly Rijvers: Logical Foundations for Attack-Defence Trees (Bsc.)
  • Niels van Schagen: Developing a backend compiler for analog simulation of differential equations (Bsc.)
  • Hessel Sieburgh: Simplicial Coalgebras for Concurrent Regular Languages (Bsc.)
  • Jamie Wiskerke: Probability Theory over Diffeological Spaces (Bsc.)

Former Students