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.