Translator from HORSz to HFLz expressed in Coq
To build the tool hz2, run
make build
Run 'hz2 -help' to see the usage.
This software is licensed under the Apache License, Version 2.0 (http://www.apache.org/licenses/LICENSE-2.0.txt).
hz2 was developed by Hiroki Oshikawa and is maintained by Naoki Kobayashi.
Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi: "Reduction from branching-time property verification of higher-order programs to HFL validity checking", Proceedings of PEPM 2019, pp.22-34, 2019.