Recursive programming with proofs
We present some methods for programming with recursive data types using a fixed-point combinator, which allows one to construct programs having their intended behaviour.
scientific article; zbMATH DE number 55538