Type fixpoints, iteration vs. recursion

DOI10.1145/317636.317789MaRDI QIDQ2817715zbMATH OpenOpenAlexFDO

Authors Zdzisław Spławski, Paweł Urzyczyn

Publication date 1 September 2016

Published in Proceedings of the fourth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/317636.317789

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 1385477
• Partial inductive definitions as type-systems for \(\lambda\)-terms
• Monotone (co)inductive types and positive fixed-point types
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types
• Computer Science Logic

Cited in

(12)

• Non-strictly positive fixed points for classical natural deduction
• Minimality in a linear calculus with iteration
• Parametricity, type equality, and higher-order polymorphism
• Two extensions of System F with (co)iteration and primitive (co)recursion principles
• Termination checking with types
• scientific article; zbMATH DE number 1385477 (Why is no real title available?)
• Efficient lambda encodings for Mendler-style coinductive types in Cedille
• Monotone recursive types and recursive data representations in Cedille
• A Tutorial on Type-Based Termination
• Computer Science Logic
• Iterator Types
• Least and greatest fixed points in intuitionistic natural deduction

This page was built for publication: Type fixpoints, iteration vs. recursion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2817715)