Structures for structural recursion

DOI10.1145/2784731.2784762MaRDI QIDQ2981950zbMATH OpenOpenAlexFDO

Authors Paul Downen, Philip Johnson-Freyd, Zena M. Ariola

Publication date 10 May 2017

Published in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

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

zbMATH Keywords

classical logiccoinductiondualityinductionrecursionsequent calculusstrong normalizationstructures

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Structural induction and coinduction in a fibrational setting
• A co-induction principle for recursively defined domains
• Induction by coinduction and control operators in call-by-name
• Well-founded recursion with copatterns and sized types
• Wellfounded recursion with copatterns: a unified approach to termination and productivity

Cited in

(9)

• Structural recursion as a query language on lists and ordered trees
• Abstracting models of strong normalization for classical calculi
• Structural recursion with locally scoped names
• scientific article; zbMATH DE number 4199615 (Why is no real title available?)
• Alpha-structural recursion and induction
• scientific article; zbMATH DE number 1302872 (Why is no real title available?)
• Theorem Proving in Higher Order Logics
• Classical (co)recursion: Mechanics
• A contextual formalization of structural coinduction

This page was built for publication: Structures for structural recursion

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