Unifiers as equivalences: proof-relevant unification of dependently typed data
From MaRDI portal
Publication:2985776
DOI10.1145/2951913.2951917zbMath1360.68321OpenAlexW2513071761MaRDI QIDQ2985776
Dominique Devriese, Frank Piessens, Jesper Cockx
Publication date: 10 May 2017
Published in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)
Full work available at URL: https://lirias.kuleuven.be/handle/123456789/544210
Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (3)
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
Uses Software
This page was built for publication: Unifiers as equivalences: proof-relevant unification of dependently typed data
