Current Courses

• Computational Models and Semantics (Master, Autumn 2024)
• Introduction to Logic (Bachelor, Spring 2024)

The Proof Rondo first-order logic proof checker that is used in the logic course.

Course archive

Student Projects

Here are some example projects that cover my research and education areas. Please feel free to propose other projects in any of these areas.

Projects in Type Theory and Logic

• Efficient sampling for coinductive programming language
• Compiler for partial differential equations on hybrid computers
• Type system for partial differential equations on hybrid computers
• Refinement type system for machine learning pipelines and guided AutoML
• Duality for equality on inductive and coinductive types
• Control systems language based on inductive-coinductive types
• Train control verification in theorem prover like Coq
• Combined inductive-coinductive logic programming (Semantics, resolution, implementation)

Projects in Coalgebra

• Coalgebras on local time scales
• Generic proof systems for coinductive predicates
• Computability via behavioural differential equations

Projects in Category Theory

• Implement tool for bio-modelling based on memory evolutive systems