Juan Manuel Serrano Hidalgo
Associate professor at University Rey Juan Carlos and co-founder at Habla Computing
Juan M. Serrano divides his time between the University Rey Juan Carlos and Habla Computing, a small consulting studio specializing in functional programming, data engineering, and kdb+/q. An active advocate for functional programming techniques for the last 13 years, he has organized numerous training sessions on functional programming with Scala.
Automating Type-Driven Development with (Co)algebras
Types matter not only for preventing runtime errors but also for guiding implementation. In some cases, they even provide enough information to automatically derive fully verified code from the signature. This derivation proceeds by pure logical reasoning —no need for LLMs here!— in accordance with the well-known Curry-Howard correspondence. This talk will explore this logical process through the lens of recursion schemes. Specifically, the search space for proofs unfolds from the initial proof sequent, while term extraction emerges from folding over the proof tree. For finite search spaces, hylomorphisms offer a brute-force algorithm, while other algorithms require specialized traversals of the search space. Finally, we will outline how to exploit Scala 3 macros and the tagless-final approach to bring these (co)algebraic techniques into practice!
←Back
