Constraint solving in non-permutative nominal abstract syntax
Nominal abstract syntax is a popular first-order technique for encoding, and reasoning about, abstract syntax involving binders. Many of its applications involve constraint solving. The most commonly used constraint solving algorithm over nominal abstract syntax is the Urban-Pitts-Gabbay nominal uni...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2011-08-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/995/pdf |