Pattern matching without K

DOI10.1145/2628136.2628139MaRDI QIDQ2819686zbMATH OpenOpenAlexFDO

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

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)

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

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

Describes a project that uses

Uses Software

• Agda
• Coq

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)