A Light Modality for Recursion

DOI10.1007/978-3-662-54458-7_29zbMath1486.68033arXiv1801.00285OpenAlexW2613536533MaRDI QIDQ2988388

Paula G.Severi

Publication date: 19 May 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1801.00285

zbMATH Keywords

productivitydenotational semanticstyped lambda-calculustype inferenceinfinite data

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items

Lewis meets Brouwer: constructive strict implication ⋮ A Light Modality for Recursion

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Type inference with recursive types: Syntax and semantics
• Fundamental properties of infinite trees
• Infinitary lambda calculus
• Guarded Dependent Type Theory with Coinductive Types
• Nominal Coalgebraic Data Types with Applications to Lambda Calculus
• Higher-order functional reactive programming in bounded space
• Programming and Reasoning with Guarded Recursion for Coinductive Types
• A Light Modality for Recursion
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Recursive subtyping revealed
• Infinitary lambda calculi and böhm models
• Pure type systems with corecursion on streams
• Productive coprogramming with guarded recursion
• On Sessions and Infinite Data
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Fair reactive programming
• Impredicative Concurrent Abstract Predicates
• Theoretical Computer Science

This page was built for publication: A Light Modality for Recursion