Indexed realizability for bounded-time programming with references and type fixpoints

Aloïs Brunel, Antoine Madet

The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging t…