Higher-order Constrained Horn Clauses: A New Approach to Verifying Higher-order Programs
Lead Research Organisation:
University of Bristol
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
People |
ORCID iD |
| Steven Ramsay (Principal Investigator) |
Publications
Jochems J
(2023)
Higher-Order MSL Horn Constraints
in Proceedings of the ACM on Programming Languages
Jones E
(2022)
CycleQ: an efficient basis for cyclic equational reasoning
Jones E
(2021)
Intensional datatype refinement: with application to scalable verification of pattern-match safety
in Proceedings of the ACM on Programming Languages
Ramsay S
(2024)
Ill-Typed Programs Don't Evaluate
in Proceedings of the ACM on Programming Languages
| Description | This work has established a new theoretical foundation for higher-order program verification based on higher-order logic. Algorithms and other techniques for automatically verifying the absence of certain classes of bugs in higher-order programs (such as functional programs written in Haskell, OCaml, Scala, F#, Elixir, Clojure and Erlang) have been disparate and disconnected, but fell mainly into three categories: (i) bespoke type systems, (ii) higher-order grammars and automata, (iii) higher-order fixpoint logic. Whilst the relationship between (iii) and higher-order logic is straightforward, our work has shown how to understand (i) and (ii) also in the setting of higher-order logic. This gives a conceptual way to understand e.g. different kinds of types as a means for expressing program invariants quite directly. |
| Exploitation Route | Those who are involved in automated program verification, in industry and academia, may put our results to use. There are a large number of program verifiers used today in industry that are based on first-order Horn clauses, and consequently do not have the ability to verify higher-order programming. Our results show how these verifiers could in principle be extended to verify higher-order features, whilst still fundamentally being rooted in logic and the establishment of invariants expressed as logical formulae. In academia, we anticipate our results being the start of a taxonomy of higher-order program invariants, in which specific type systems are given a logical semantics according to the techniques developed in our work. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | Higher-order Program Invariants and Higher-order Constrained Horn Clauses |
| Amount | £81,532 (GBP) |
| Organisation | The Research Institute on Verified Trustworthy Software Systems |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 10/2019 |
| End | 03/2023 |
| Title | Intensional Datatypes GHC Plugin with Accompanying Benchmark Datasets |
| Description | A virtual machine image containing the version of the Intensional Datatypes GHC plugin and all associated benchmark data, whose versions are exactly those used to produce the empirical results contained in the paper Intensional Datatype Refinement which is conditionally accepted for publication in the journal Proceedings of the ACM on Programming Languages (POPL'21). To get started, log into the virtual machine using the account "aeval" with password "popl21". The software and all relevant benchmark data and tooling is located in the artifact subdirectory of the home directory. Follow the instructions in artifact/README.md to recreate the benchmarking. The virtual machine image is a standard Ubuntu 20.04.1 LTS minimal install, to which we have added ghc-8.8.3 and cabal-install-3.0 (for compiling and running the artifact) and python3-tabulate (for pretty printing the benchmark results) and visual studio code (for convenience). The virtual machine image was created using Virtual Box 6.0.24 on a Windows 10 host. |
| Type Of Technology | Software |
| Year Produced | 2020 |
| Open Source License? | Yes |
| Impact | N/A |
| URL | https://zenodo.org/record/4072906 |