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
- Alejandro Villoria (PhD Candidate)
- Berend van Starkenburg (PhD Candidate)
- Chase Ford (Postdoc)
- Tanjona Ralaivaosaona (PhD Candidate)
Current Students
None
Former Students
- Walt Duivenvoorde: Simulating Differential Equations using Hybrid Digital-Analog Computers (Bsc., finished August 2024)
- Lulof Pirrée: Coalgebraic Modal Logic for Cellular Automata (Msc., finished July 2024)
- Huib Sprangers: A Type System for Machine Learning Pipelines (Bsc., finished May 2024)
- Floyd Remmerswaal: Validation & Simulation of Software-Defined Network Specifications in Probabilistic NetKAT (Msc, Finished December 2023)
- Berend van Starkenburg: Working Towards Category Theoretic Semantics for Separation Logic (Msc., Finished September 2023)
- Dirck van den Ende: Towards a Compiler for Partial Differential Equations for Analog Computers (Bsc., finished July 2023)
- Dominique R. Lawson: Formalizing the Van Kampen Theorem for Directed Topology (Bsc., finished July 2023)
- Mattias Tuk: Usability of VR in the construction of category theoretical diagrams (Bsc., finished March 2023)
- Thomas Baronner: Finite accessibility of Higher-Dimensional Automata and unbounded parallelism of their languages (Bsc., finished Dec. 2022)
- Lennard Schaap: Formalised semantics of Lustre (Bsc., finished July 2022)
- Julia Bolt: An approach to describing the semantics of Hedy, a gradual programming language for education (Msc., finished June 2022)
- Loes Dekker: Formal Semantics of ALCH (Msc., finished July 2021)
- Rintse van de Vlasakker: Operational Semantics of GHOPFL – A guarded, higher order, probabilisitc, coinductive, functional language (Msc., finished July 2021)
- Daniëlle Gramsbergen: Subcoinductive Types (Bsc., finished July 2020)
- Alex Keizer: Coalgebras of Session Types (Bsc., finished July 2020)
- Daniël Otten: M-Types and Bisimulation (Bsc., finished July 2020)