Copatterns, programming infinite structures by observations
From MaRDI portal
Recommendations
Cited in
(39)- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- A contextual formalization of structural coinduction
- Classical (co)recursion: Mechanics
- A realizability interpretation of Church's simple theory of types
- Regular varieties of automata and coequations
- A mechanized theory of regular trees in dependent type theory
- Indexed codata types
- Some techniques for reasoning automatically on co-inductive data structures
- Coinduction in Flow: The Later Modality in Fibrations
- Wellfounded recursion with copatterns: a unified approach to termination and productivity
- Dualized simple type theory
- A case study in programming coinductive proofs: Howe's method
- scientific article; zbMATH DE number 7376040 (Why is no real title available?)
- Dependent type refinements for futures
- Squeezing streams and composition of self-stabilizing algorithms
- Unnesting of copatterns
- Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
- Defining trace semantics for CSP-Agda
- A model of guarded recursion with clock synchronisation
- Undecidability of equality for codata types
- Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
- How to reason coinductively informally
- Interactive programming in Agda -- objects and graphical user interfaces
- Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- POPLMark reloaded: mechanizing proofs by logical relations
- Inductive and coinductive predicate liftings for effectful programs
- scientific article; zbMATH DE number 7559298 (Why is no real title available?)
- Turing-Completeness Totally Free
- Well-founded recursion with copatterns and sized types
- Intuitionistic fixed point logic
- Relational graph models at work
- Totality for mixed inductive and coinductive types
- Elaborating dependent (co)pattern matching: no pattern left behind
- Efficient lambda encodings for Mendler-style coinductive types in Cedille
- scientific article; zbMATH DE number 7037626 (Why is no real title available?)
- Friends with benefits. Implementing corecursion in foundational proof assistants
- CoCaml: functional programming with regular coinductive types
- Sequent calculus and equational programming
This page was built for publication: Copatterns, programming infinite structures by observations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2931780)
