Pattern matching without K

DOI10.1145/2628136.2628139zbMATH Open1345.68045OpenAlexW2158830522MaRDI QIDQ2819686FDOQ2819686

Authors: Jesper Cockx, Dominique Devriese, Frank Piessens 

Publication date: 29 September 2016

Published in: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://lirias.kuleuven.be/handle/123456789/452283

Recommendations

• Eliminating dependent pattern matching without K
• Eliminating Dependent Pattern Matching
• A New Elimination Rule for the Calculus of Inductive Constructions
• Overlapping and order-independent patterns. Definitional equality for all
• Elaborating dependent (co)pattern matching: no pattern left behind

zbMATH Keywords

Agdahomotopy type theorydependent pattern matchingK axiom

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40) Functional programming and lambda calculus (68N18)

Cited In (9)

• Eliminating dependent pattern matching without K
• A New Elimination Rule for the Calculus of Inductive Constructions
• Leibniz equality is isomorphic to Martin-Löf identity, parametrically
• The view from the left
• Overlapping and order-independent patterns. Definitional equality for all
• Eliminating Dependent Pattern Matching
• Programming with ornaments
• Subtyping without reduction
• Elaborating dependent (co)pattern matching: no pattern left behind

Uses Software

• Coq
• Agda

This page was built for publication: Pattern matching without K

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819686)