Functions-as-constructors higher-order unification: extended pattern unification

DOI10.1007/s10472-021-09774-yOpenAlexW3204285856MaRDI QIDQ2134936

Tomer Libal, Dale A. Miller

Publication date: 4 May 2022

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-021-09774-y

zbMATH Keywords

higher-order unificationdeterministic unification algorithmspattern unificationtype-free unification algorithms

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Uses Software

• TPS
• Beluga
• Isabelle/HOL
• Satallax
• Twelf
• Abella
• Agda
• Leo
• Teyjus

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Deterministic second-order patterns
• The undecidability of the second-order unification problem
• Unification under a mixed prefix
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Proving and applying program transformations expressed with second-order patterns
• Unification with extended patterns
• Isabelle/HOL. A proof assistant for higher-order logic
• Higher-order unification revisited: Complete sets of transformations
• Proof checking and logic programming
• Programming with Higher-Order Logic
• Satallax: An Automatic Higher-Order Prover
• A unification algorithm for Coq featuring universe polymorphism and overloading
• Higher-Order Dynamic Pattern Unification for Dependent Types and Records
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Hints in Unification
• Canonical Big Operators
• Crafting a Proof Assistant
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
• Abella: A System for Reasoning about Relational Specifications
• Implementing type theory in higher order constraint logic programming
• Functions-as-constructors Higher-order Unification
• The undecidability of unification in third order logic
• Logic Based Program Synthesis and Transformation
• Reasoning with higher-order abstract syntax in a logical framework
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

This page was built for publication: Functions-as-constructors higher-order unification: extended pattern unification