Nominal Recursors as Epi-Recursors - POPL 2024

Explore a 21-minute video presentation from POPL 2024 examining nominal recursors in the context of syntax with bindings. Delve into the concept of epi-recursors, which abstractly captures the distinction between recursed constructors and other operators underpinning recursion. Learn about an abstract framework for comparing epi-recursors, its application to existing nominal recursors, and the resulting expressiveness hierarchies. Discover how this methodology extends to nominal corecursors for defining functions targeting infinitary non-well-founded terms. Gain insights into the relative merits of different syntax axiomatizations, validated through Isabelle/HOL theorem proving. Access the accompanying article and supplementary archive for a deeper understanding of this research in nominal logic and formal reasoning.

[POPL'24] Nominal Recursors as Epi-Recursors