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

Agdadependent pattern matchinghomotopy type theoryK 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

(10)

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

Describes a project that uses

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)