Copatterns
From MaRDI portal
Publication:2931780
DOI10.1145/2429069.2429075zbMath1301.68080MaRDI 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
pattern matching; functional programming; message passing; coinduction; introduction vs. elimination
Related Items
Unnamed Item, A realizability interpretation of Church's simple theory of types, Unnamed Item, Unnamed Item, Unnamed Item, 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, POPLMark reloaded: Mechanizing proofs by logical relations, Elaborating dependent (co)pattern matching: No pattern left behind, A case study in programming coinductive proofs: Howe’s method, Well-founded recursion with copatterns and sized types, Interactive programming in Agda – Objects and graphical user interfaces, A model of guarded recursion with clock synchronisation, Coinduction in Flow: The Later Modality in Fibrations, Classical (co)recursion: Mechanics, Undecidability of equality for codata types, Intuitionistic fixed point logic, Regular Varieties of Automata and Coequations, Turing-Completeness Totally Free, A Mechanized Theory of Regular Trees in Dependent Type Theory, Dualized Simple Type Theory, Friends with Benefits, Unnamed Item, How to Reason Coinductively Informally
Uses Software
