A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking

DOI10.1007/978-3-030-64437-6_5zbMath1476.68149OpenAlexW3107553734MaRDI QIDQ2038070

Naoki Iwayama, Hiroyuki Katsura, Naoki Kobayashi, Takeshi Tsukada

Publication date: 8 July 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-64437-6_5

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (2)

On higher-order reachability games vs may reachability ⋮ An overview of the HFL model checking project

This page was built for publication: A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking