This thesis introduces recursive types to the Cogent programming language, which forms the basis for recursion and iteration without the use of Cogent's C FFI. Additionally, a pen-and-paper formalisation of a termination checker for the language is defined in order to assist with keeping Cogent functions total and terminating.
A copy of the paper is here, with the source LaTeX here.
The implementation in the model compiler minigent can be found here.