Cass Alexandru (they/them)
I’m a PhD student at the Working Group Programming Languages at the RPTU Kaiserslautern-Landau, supervised by Ralf Hinze. My current research topic is the application of categorical semantics of (dependent) type theory for writing (intrinsically) correct total algorithms (using structured recursion). I am currently investigating recursive coalgebras and bialgebraic semantics.
More broadly, I’m interested in the application
of the full breadth of the theoretical arsenal to
the problem of ergonomic use of dependently typed
programming languages in practice, including but not
limited to:
datatype-generic programming,
recursion schemes, homotopy and simplicial type
theory, substructural type systems, EDSLs, compiler
construction, decision procedures, SMT, ATPs,
proof/program synthesis
Online presence
I go by cxandru
on most online
forums, and also use the same profile icon
everywhere, so I should be relatively easy to spot.
My accounts on selected forums:
- Mastodon: @cxandru@types.pl
- Github: cxandru
Papers
- Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide: “Intrinsically Correct Sorting in Cubical Agda”. CPP 2025.
Talks
“Natural transformations as business logics: An operational intuition”. FP Dag 2025. Updated slides
“Intrinsically correct sorting using bialgebraic semantics”. SPLV 2024 lightning talk.
“When the Types Align: A coincidence of total and partial correctness with a slice of cubical Agda”. Dutch FP Day 2024.
“Structured Traversals for (Mutually) Recursive Algebraic Data Types”. Munihac 2022.
Theses
- “Intrinsically correct sorting using bialgebraic semantics”. Master’s thesis, Radboud University, 2023. BibLaTex entry:
@thesis{alexandru_intrinsically_2023,
author = {Alexandru, Cass},
title = {Intrinsically correct sorting using bialgebraic semantics},
institution = {Radboud University},
type = {mathesis},
year = {2023},
file = {https://www.cs.ru.nl/masters-theses/2023/C_Alexandru___Intrinsically_correct_sorting_using_bialgebraic_semantics.pdf},
url = {https://www.cs.ru.nl/masters-theses#2023},
}
- “Specifying Loops with Contracts”. Bachelor’s thesis, LMU Munich, 2019. BibLaTex entry:
@thesis{alexandru_specifying_2019,
author = {Alexandru, Cass},
title = {Specifying Loops with Contracts},
subtitle = {Reasoning about loops as recursive procedures},
institution = {LMU Munich},
type = {bathesis},
year = {2019},
file = {https://www.sosy-lab.org/research/bsc/2019.Alexandru.Specifying_Loops_With_Contracts.pdf},
url = {https://www.sosy-lab.org/research/bib/Year/2019.html#AlexandruLoopContracts}
}
Unpublished Notes
- “Bialgebraic Semantics, Formalized”. 2023. This research internship report documents the pull request μ-Bialgebras by cxandru · Pull Request #362 · agda/agda-categories