Free Monads, Intrinsic Scoping, and Higher-Order Preunification

Conference talk · TFP 2024 — Trends in Functional Programming · January 10, 2024 · South Orange, NJ, USA

A higher-order preunification procedure derived generically for any object language presented as a free monad over a bifunctor, with an application to type-checking Martin-Löf Type Theory.

Awarded the 2024 John McCarthy Best Paper Award at TFP 2024.

Slides