Higher-Order Dynamic Pattern Unification for Dependent Types and Records

DOI10.1007/978-3-642-21691-6_5zbMath1331.68040OpenAlexW2120226337MaRDI QIDQ3007654

Brigitte Pientka, Andreas Abel

Publication date: 17 June 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21691-6_5

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (3)

Functions-as-constructors higher-order unification: extended pattern unification ⋮ Unnamed Item ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading

Uses Software

• Beluga
• Twelf
• Delphin

Cites Work

• Unnamed Item
• The undecidability of the second-order unification problem
• Unification with extended patterns
• A Linear Spine Calculus
• Contextual modal type theory
• Foundations of Software Science and Computational Structures
• Types for Proofs and Programs
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

This page was built for publication: Higher-Order Dynamic Pattern Unification for Dependent Types and Records