A Light Modality for Recursion

We investigate the interplay between a modality for controlling the behaviourof recursive functional programs on infinite structures which are completelysilent in the syntax. The latter means that programs do not contain "marks"showing the application of the introduction and elimination rules for themodality. This shifts the burden of controlling recursion from the programmerto the compiler. To do this, we introduce a typed lambda calculus a la Currywith a silent modality and guarded recursive types. The typing disciplineguarantees normalisation and can be transformed into an algorithm which infersthe type of a program.Comment: 32 pages 1 figure in pdf forma