Severi, Paula - 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: Severi, Paula

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.


Source : oai:arXiv.org:1801.00285
Volume: Volume 15, Issue 1
Published on: February 5, 2019
Submitted on: January 3, 2018
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages


Share