Indexed codata types

DOI10.1145/2951913.2951929MaRDI QIDQ2985784zbMATH OpenOpenAlexFDO

Authors David Thibodeau, Andrew Cave, Brigitte Pientka

Publication date 10 May 2017

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

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

zbMATH Keywords

coinductiondependent typesfunctional programminglogical frameworks

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Data structures (68P05) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Copatterns, programming infinite structures by observations
• Unnesting of copatterns
• Well-founded recursion with copatterns and sized types
• Refining inductive types
• Fibred data types

Cited in

(10)

• On the key dependent message security of the Fujisaki-Okamoto constructions
• Copatterns, programming infinite structures by observations
• Friends with benefits. Implementing corecursion in foundational proof assistants
• \textsc{Lincx}: a linear logical framework with first-class contexts
• scientific article; zbMATH DE number 2090025 (Why is no real title available?)
• Index-stratified types
• Elaborating dependent (co)pattern matching: no pattern left behind
• Unnesting of copatterns
• A case study in programming coinductive proofs: Howe's method
• Codatatypes in ML

This page was built for publication: Indexed codata types

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