2021/09/10 by Naoki Kobayashi
Computer Science · #cs.PL #cs.LO
paper · pdf · doi:10.4204/eptcs.344.1
published as EPTCS 344, 2021, pp. 1-12 · In Proceedings HCVS 2021, arXiv:2109.03988
arxiv created 2021/09/10 · arxiv updated 2021/09/13
In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HFL, we explain how it can be applied to program verification, and summarize the current status of the project.