Monotone recursive types and recursive data representations in Cedille

DOI10.1017/S0960129521000402zbMath1495.68036arXiv2001.02828OpenAlexW3000405346MaRDI QIDQ5076393

Aaron Stump, Christopher Jenkins

Publication date: 17 May 2022

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

recursive typesrecursion schemesCDLEimpredicative encodingsScott encoding

Mathematics Subject Classification ID

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

Uses Software

• Coq
• MiniAgda
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Innovations in computational type theory using Nuprl
• Lectures on the Curry-Howard isomorphism
• Fixed point theorems and semantics: A folk tale
• Recursive programming with proofs
• A discrimination algorithm inside \(\lambda -\beta\)-calculus
• Iteration and coiteration schemes for higher-order and nested datatypes
• Efficient Mendler-style lambda-encodings in Cedille
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types
• A fixpoint theorem for complete categories
• From realizability to induction via dependent intersection
• A lattice-theoretical fixpoint theorem and its applications
• Type fixpoints
• Generic Fibrational Induction
• Syntax and Semantics of Quantitative Type Theory
• Efficiency of lambda-encodings in total type theory
• Safe zero-cost coercions for Haskell
• The calculus of dependent lambda eliminations

This page was built for publication: Monotone recursive types and recursive data representations in Cedille