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

None

Former Students