Ádám Kurucz (ELTE Eötvös Loránd University) |
Péter Bereczky (ELTE Eötvös Loránd University) |
Dániel Horpácsi (ELTE Eötvös Loránd University) |
Matching logic is a logical framework for specifying and reasoning about programs using pattern matching semantics. A pattern is made up of a number of structural components and constraints. Structural components are syntactically matched, while constraints need to be satisfied. Having multiple structural patterns poses a practical problem as it requires multiple matching operations. This is easily remedied by unification, for which an algorithm has already been defined and proven correct in a sorted, polyadic variant of matching logic. This paper revisits the subject in the applicative variant of the language while generalising the unification problem and mechanizing a proven-sound solution in Coq. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.410.1 | bibtex | |
Comments and questions to:
![]() |
For website issues:
![]() |