The computability path ordering
This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation on terms obtained by lifting a precedence on function symbols. A first version,...
| Published in: | Logical Methods in Computer Science |
|---|---|
| Main Authors: | , , |
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2015-10-01
|
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1604/pdf |