Higher-order constrained Horn clauses for higher-order program verification
<p>Higher-order constrained Horn clauses (HoCHC) are a fragment of higher-order logic modulo theories recently introduced by Cathcart Burn et al. (2018). This thesis explores the adequacy of HoCHC as a unifying framework for the algorithmic verification of higher-order programs, through links...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2020
|
| Subjects: |
| _version_ | 1826286300592865280 |
|---|---|
| author | Jochems, J |
| author2 | Ong, L |
| author_facet | Ong, L Jochems, J |
| author_sort | Jochems, J |
| collection | OXFORD |
| description | <p>Higher-order constrained Horn clauses (HoCHC) are a fragment of higher-order logic modulo theories recently introduced by Cathcart Burn et al. (2018). This thesis explores the adequacy of HoCHC as a unifying framework for the algorithmic verification of higher-order programs, through links with existing approaches to program verification as well as a sound and refutationally complete solution method for HoCHC. </p>
<p>We establish a continuous interpretation for HoCHC in which the semantic domains are restricted to Scott-continuous functions. We show that the continuous HoCHC decision problem is equivalent to the original problem. This continuous interpretation serves as a foundation for a sound and refutation-complete resolution proof system - based on SLD-resolution - for solving unsatisfiable instances of the HoCHC problem over a semi-decidable background theory.</p>
<p>To address the relation between HoCHC and higher-order model checking, we introduce a coinductive version of HoCHC that is characterised by a greatest fixpoint construction. We define an encoding of higher-order recursion schemes into a HoCHC logic program, which can be used to reduce the open higher-order recursion scheme equivalence problem - and thus the lambdaY-calculus Böhm tree equivalence problem - to semi-decidability of coinductive HoCHC over Maher's complete and decidable background theory of trees (Maher, 1988; Djelloul et al., 2008).</p>
<p>Finally, we develop an axiomatic basis for relations as higher-order program invariants in the form of a Hoare logic. Our approach to Hoare logic for higher-order programs distinguishes itself from the literature through the combination of a higher-order assertion logic and a relatively complete proof system.</p> |
| first_indexed | 2024-03-07T01:41:43Z |
| format | Thesis |
| id | oxford-uuid:9717a949-94dc-44ce-9d7b-0575e061b8d5 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T01:41:43Z |
| publishDate | 2020 |
| record_format | dspace |
| spelling | oxford-uuid:9717a949-94dc-44ce-9d7b-0575e061b8d52022-03-26T23:57:16ZHigher-order constrained Horn clauses for higher-order program verificationThesishttp://purl.org/coar/resource_type/c_db06uuid:9717a949-94dc-44ce-9d7b-0575e061b8d5Computer science (mathematics)EnglishHyrax Deposit2020Jochems, JOng, L<p>Higher-order constrained Horn clauses (HoCHC) are a fragment of higher-order logic modulo theories recently introduced by Cathcart Burn et al. (2018). This thesis explores the adequacy of HoCHC as a unifying framework for the algorithmic verification of higher-order programs, through links with existing approaches to program verification as well as a sound and refutationally complete solution method for HoCHC. </p> <p>We establish a continuous interpretation for HoCHC in which the semantic domains are restricted to Scott-continuous functions. We show that the continuous HoCHC decision problem is equivalent to the original problem. This continuous interpretation serves as a foundation for a sound and refutation-complete resolution proof system - based on SLD-resolution - for solving unsatisfiable instances of the HoCHC problem over a semi-decidable background theory.</p> <p>To address the relation between HoCHC and higher-order model checking, we introduce a coinductive version of HoCHC that is characterised by a greatest fixpoint construction. We define an encoding of higher-order recursion schemes into a HoCHC logic program, which can be used to reduce the open higher-order recursion scheme equivalence problem - and thus the lambdaY-calculus Böhm tree equivalence problem - to semi-decidability of coinductive HoCHC over Maher's complete and decidable background theory of trees (Maher, 1988; Djelloul et al., 2008).</p> <p>Finally, we develop an axiomatic basis for relations as higher-order program invariants in the form of a Hoare logic. Our approach to Hoare logic for higher-order programs distinguishes itself from the literature through the combination of a higher-order assertion logic and a relatively complete proof system.</p> |
| spellingShingle | Computer science (mathematics) Jochems, J Higher-order constrained Horn clauses for higher-order program verification |
| title | Higher-order constrained Horn clauses for higher-order program verification |
| title_full | Higher-order constrained Horn clauses for higher-order program verification |
| title_fullStr | Higher-order constrained Horn clauses for higher-order program verification |
| title_full_unstemmed | Higher-order constrained Horn clauses for higher-order program verification |
| title_short | Higher-order constrained Horn clauses for higher-order program verification |
| title_sort | higher order constrained horn clauses for higher order program verification |
| topic | Computer science (mathematics) |
| work_keys_str_mv | AT jochemsj higherorderconstrainedhornclausesforhigherorderprogramverification |