Elaborating dependent (co)pattern matching: No pattern left behind (Q5110925): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Irdis
@@ Property / describes a project that uses: Irdis / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+AmiCo
@@ Property / describes a project that uses: AmiCo / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lean
@@ Property / describes a project that uses: Lean / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Idris
@@ Property / describes a project that uses: Idris / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Equations
@@ Property / describes a project that uses: Equations / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q126314432
@@ Property / Wikidata QID: Q126314432 / rank @@
+Normal rank
@@ Property / cites work @@
+Wellfounded recursion with copatterns
@@ Property / cites work: Wellfounded recursion with copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+Copatterns
@@ Property / cites work: Copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+Logic Programming with Focusing Proofs in Linear Logic
+Normal rank
@@ Property / cites work @@
+Friends with Benefits
@@ Property / cites work: Friends with Benefits / rank @@
+Normal rank
@@ Property / cites work @@
+Idris, a general-purpose dependently typed programming language: Design and implementation
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Unifiers as equivalences: proof-relevant unification of dependently typed data
+Normal rank
@@ Property / cites work @@
+Telescopic mappings in typed lambda calculus
@@ Property / cites work: Telescopic mappings in typed lambda calculus / rank @@
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+Normal rank
@@ Property / cites work @@
+Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
+Normal rank
@@ Property / cites work @@
+Eliminating Dependent Pattern Matching
@@ Property / cites work: Eliminating Dependent Pattern Matching / rank @@
+Normal rank
@@ Property / cites work @@
+Focusing on pattern matching
@@ Property / cites work: Focusing on pattern matching / rank @@
+Normal rank
@@ Property / cites work @@
+The view from the left
@@ Property / cites work: The view from the left / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247309
@@ Property / cites work: Q4247309 / rank @@
+Normal rank
@@ Property / cites work @@
+Unnesting of Copatterns
@@ Property / cites work: Unnesting of Copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+Equations: A Dependent Pattern-Matching Compiler
@@ Property / cites work: Equations: A Dependent Pattern-Matching Compiler / rank @@
+Normal rank
@@ Property / cites work @@
+Indexed codata types
@@ Property / cites work: Indexed codata types / rank @@
+Normal rank
@@ Property / cites work @@
+Focusing and higher-order abstract syntax
@@ Property / cites work: Focusing and higher-order abstract syntax / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0956796819000182
+Normal rank
@@ Property / OpenAlex ID @@
+W3002727729
@@ Property / OpenAlex ID: W3002727729 / rank @@
+Normal rank