Variations on Inductive-Recursive Definitions. - Neil Ghani; Conor McBride; Fredrik Nordvall Forsberg; Stephan Spahn (MFCS, 2017)

Axiomatizations of Compositional Inductive-Recursive Definitions - Stephan Alexander Spahn (2018)

Strong functional pearl: Harper's regular-expression matcher in Cedille. - Aaron Stump; Christopher Jenkins; Stephan Spahn; Colin McDonald (Proc. ACM Program. Lang., 2020)