Title: A Light Modality for Recursion,
Abstract: We investigate the interplay between a modality for controlling the behaviour
of recursive functional programs on infinite structures which are completely
silent in the syntax. The latter means that programs do not contain "marks"
showing the application of the introduction and elimination rules for the
modality. This shifts the burden of controlling recursion from the programmer
to the compiler. To do this, we introduce a typed lambda calculus a la Curry
with a silent modality and guarded recursive types. The typing discipline
guarantees normalisation and can be transformed into an algorithm which infers
the type of a program.