Copatterns

DOI10.1145/2429069.2429075zbMath1301.68080OpenAlexW2074592053MaRDI QIDQ2931780

Brigitte Pientka, Andreas Abel, Anton Setzer, David Thibodeau

Publication date: 27 November 2014

Published in: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

pattern matchingfunctional programmingmessage passingcoinductionintroduction vs. elimination

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Related Items (25)

Regular Varieties of Automata and Coequations ⋮ Turing-Completeness Totally Free ⋮ A Mechanized Theory of Regular Trees in Dependent Type Theory ⋮ A realizability interpretation of Church's simple theory of types ⋮ Classical (co)recursion: Mechanics ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Elaborating dependent (co)pattern matching: No pattern left behind ⋮ Unnamed Item ⋮ Squeezing streams and composition of self-stabilizing algorithms ⋮ Well-founded recursion with copatterns and sized types ⋮ Interactive programming in Agda – Objects and graphical user interfaces ⋮ Dualized Simple Type Theory ⋮ Unnamed Item ⋮ A model of guarded recursion with clock synchronisation ⋮ Intuitionistic fixed point logic ⋮ Friends with Benefits ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ How to Reason Coinductively Informally ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Undecidability of equality for codata types ⋮ Unnamed Item ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs

Uses Software

• Coq
• Haskell
• Agda

This page was built for publication: Copatterns