Eliminating Dependent Pattern Matching

DOI10.1007/11780274_27MaRDI QIDQ5757920zbMATH OpenOpenAlexFDO

Authors Healfdene Goguen, Conor McBride, James McKinna

Publication date 7 September 2007

Published in Algebra, Meaning, and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11780274_27

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Eliminating dependent pattern matching without K
• A New Elimination Rule for the Calculus of Inductive Constructions
• Pattern matching without K
• Equations: a dependent pattern-matching compiler
• The view from the left

Cited in

(14)

• Homotopy type theory in Lean
• Pattern matching without K
• The Lean theorem prover (system description)
• A New Elimination Rule for the Calculus of Inductive Constructions
• Algebra of programming in Agda: Dependent types for relational program derivation
• Elaborating dependent (co)pattern matching: no pattern left behind
• An effectful way to eliminate addiction to dependence
• Eliminating dependent pattern matching without K
• Programming with ornaments
• The calculus of dependent lambda eliminations
• Overlapping and order-independent patterns. Definitional equality for all
• Partiality and recursion in interactive theorem provers -- an overview
• Equations: a dependent pattern-matching compiler
• Equations for hereditary substitution in Leivant's predicative system F: a case study

This page was built for publication: Eliminating Dependent Pattern Matching

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