| Directory name | Source |
|---|---|
| Bird | Richard Bird, Introduction to Functional Programming using Haskell, Prentice Hall, 1998. |
| Lifantsev | Maxim Lifantsev and Leo Bachmair, An LPO-based termination ordering for higher-order terms without lambda-abstraction, Proc. of TPHOLs 1998, LNCS 1479, 1998. |
| AotoYamadaHOR04 | Takahito Aoto and Toshiyuki Yamada, Termination of simply typed applicative term rewriting systems, Proc. HOR 2004, Technical Report AIB-2004-03, RWTH Aachen, Germany. |
| AotoYamadaRTA05 |
The examples of this directory are from a collection of Aoto and
Yamada used to evaluate the results of the paper below.
They have been translated to binary applicative form and we have
removed all type information. Afterwards resulting
duplicate examples were removed.
Takahito Aoto and Toshiyuki Yamada, Dependency Pairs for Simply Typed Term Rewriting, Proc. RTA 2005, LNCS 3467, pages 120-134. 2005. |
| ToyamaRTA04 | Yoshihito Toyama, Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms, Proc. RTA 2004, LNCS 3091, pages 40-54, 2004. |
| BirdWadler | Richard Bird and Philip Wadler, Introduction to Functional Programming, Prentice Hall, 1988. |
| AProVE_HO | These examples were written for this evaluation. One part of them is based on common algorithms from functional programming, the others serve to show certain effects related to untyped vs. typed applicative term rewriting. |
| Kusakari | Keiichirou Kusakari, On proving termination of term rewriting systems with higher-order variables, IPSJ Transactions on Programming, 42 (SIG 7 (PRO 11)), 2001. |
The body of these examples was later accepted into the Termination Problem Data Base (TPDB) as the TRS/higher-order category.
| AProVE 1.2 | AProVE 1.1d | |
|---|---|---|
| Yes () | 43 | 13 |
| Failure () | 8 | 3 |
| No () | 8 | 7 |
| Timeout () | 2 | 38 |
Error ( ) | 0 | 0 |
| Total | 61 | 61 |