Eliminating dependent pattern matching without K

DOI10.1017/S0956796816000174zbMath1419.68037OpenAlexW2516238737MaRDI QIDQ5371975

Dominique Devriese, Frank Piessens, Jesper Cockx

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796816000174

Mathematics Subject Classification ID

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

Related Items (1)

Foundations of dependent interoperability

Uses Software

• Coq
• Epigram
• Irdis
• Lean
• Idris
• cubicaltt
• Equations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013, vii + 583 pp.
• Pattern matching without K
• Higher Homotopies in a Hierarchy of Univalent Universes
• Unifiers as equivalences: proof-relevant unification of dependently typed data
• The Lean Theorem Prover (System Description)
• A New Elimination Rule for the Calculus of Inductive Constructions
• The view from the left
• On the bright side of type classes
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Generalizations of Hedberg’s Theorem
• Advanced Functional Programming
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Equations: A Dependent Pattern-Matching Compiler
• Eliminating Dependent Pattern Matching
• Types for Proofs and Programs

This page was built for publication: Eliminating dependent pattern matching without K