Nominal unification with letrec and environment-variables

DOI10.1007/978-3-030-68446-4_5OpenAlexW3131123633MaRDI QIDQ2119105

Manfred Schmidt-Schauss, Yunus D. K. Kutz

Publication date: 23 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-68446-4_5

zbMATH Keywords

program transformationsautomated deductionnominal unificationabstract environmentsletrec-expressions

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Haskell
• GHC
• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nominal techniques in Isabelle/HOL
• A polynomial nominal unification algorithm
• Nominal unification with atom-variables
• Nominal unification of higher order expressions with recursive let
• Nominal Sets
• Unification and matching on compressed terms
• Algorithms for Extended Alpha-Equivalence and Complexity
• Safety of Nöcker's strictness analysis
• An Efficient Unification Algorithm
• αCheck: A mechanized metatheory model checker
• Rewriting with generalized nominal unification
• Computer Science Logic
• An Efficient Nominal Unification Algorithm
• General Bindings and Alpha-Equivalence in Nominal Isabelle

This page was built for publication: Nominal unification with letrec and environment-variables