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

functional programmingdependent typescoinductionlogical frameworks

Mathematics Subject Classification ID

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

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)

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

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)