Team STyLo — Semantics, Types and Logic

The STyLo team is part of the Theory Cluster of the Leiden University. In the team, we investigate logical theories, programming languages and type systems, and various mathematical theories for implementing and reasoning about the behaviour of systems. We are creating tools for building systems that have desired properties by construction, for example via type systems, and for leveraging computers in the verification of properties, typically via computer-assisted proofs.

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, biology and chemistry.

To build systems that fulfil certain 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. Interestingly, the same tools that we use to construct and analyse type systems can also be used as the foundation of proof systems. Such proof systems underlie the verification and analyis of systems, both in the form of computer-assisted proofs and in automatic deduction.

Compositional reasoning and human-computer interaction are key to the construction, control and analysis of large scale systems, and in the STyLo team we are contributing to their foundation.

Current PhD Candidates

Current Students

  • Floyd Remmerswaal: Compilation of ProbNetKAT (Master)
  • Huib Sprangers: Type Systems for Machine Learning Pipelines (Bachelor)

Former Students