Certified Unification for Rational Terms

Certified Unification for Rational Terms

Domoratskiy E.A. (SPbU, St Petersburg, Russia)
Boulytchev D.Yu. (SPbU, St Petersburg, Russia)

Abstract

We present a unification algorithm for first-order rational terms certified with the Rocq proof assistant. The algorithm is based on the results of Martelli and Rossi but reformulated in order to derive a practically useful implementation. We introduce the basic notions of rational terms and equation systems as an intermediate state of the algorithm and the algorithm itself, and prove their main properties. All statements are formally verified in Rocq without any additional axioms. We use an induction-based approach to define a bisimilarity for coinductive types in Rocq that allows one to avoid productivity checker issues. The Rocq specification is automatically extracted into a Haskell implementation. To our knowledge this is the first work that provides a mechanized specification of unification algorithm for rational terms.

Keywords

rational terms; unification; certified programming; coinduction; bisimilarity.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 6, part 1, 2026, pp. 23-40

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(6)-2

For citation

Domo0ratskiy E.A., Boulytchev D.Yu. Certified Unification for Rational Terms. Proceedings of the Institute for System Programming, vol. 38, issue 6, part 1, 2026, pp. 23-40 DOI: 10.15514/ISPRAS-2026-38(6)-2.

Full text of the paper in pdf Back to the contents of the volume