Elaborating dependent (co)pattern matching: No pattern left behind

DOI10.1017/S0956796819000182zbMath1442.68025OpenAlexW3002727729WikidataQ126314432 ScholiaQ126314432MaRDI QIDQ5110925

Andreas Abel, Jesper Cockx

Publication date: 26 May 2020

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796819000182

Mathematics Subject Classification ID

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

Related Items

Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Uses Software

• Coq
• Agda
• Irdis
• Lean
• Idris
• AmiCo
• GitHub
• Equations

Cites Work

• Unnamed Item
• Telescopic mappings in typed lambda calculus
• Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
• Copatterns
• Unifiers as equivalences: proof-relevant unification of dependently typed data
• Indexed codata types
• Friends with Benefits
• Focusing and higher-order abstract syntax
• The Lean Theorem Prover (System Description)
• Logic Programming with Focusing Proofs in Linear Logic
• The view from the left
• Unnesting of Copatterns
• Wellfounded recursion with copatterns
• Focusing on pattern matching
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Types for Proofs and Programs
• Equations: A Dependent Pattern-Matching Compiler
• Eliminating Dependent Pattern Matching