Dependent Type Theory with Parameterized First-Order Data Types and Well-Founded Recursion. - David Wahlstedt (2007)

Stop When You Are Almost-Full - Adventures in Constructive Termination. - Dimitrios Vytiniotis; Thierry Coquand; David Wahlstedt (ITP, 2012)

Cumulative Subtraction Games. - Gal Cohensius; Urban Larsson; Reshef Meir; David Wahlstedt (Electron. J. Comb., 2019)