Paula Severi - A Light Modality for Recursion

lmcs:4174 - Logical Methods in Computer Science, February 5, 2019, Volume 15, Issue 1 -
A Light Modality for Recursion

Authors: Paula Severi

    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.

    Volume: Volume 15, Issue 1
    Published on: February 5, 2019
    Accepted on: February 5, 2019
    Submitted on: January 3, 2018
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages


    Consultation statistics

    This page has been seen 391 times.
    This article's PDF has been downloaded 218 times.