https://arxiv.org/abs/1705.06216
Currently, he's pitching horn-clauses, saying there's already plenty of horn-clause solvers.
Most people prefer higher order logic for writing stuff, but what if we could lift Horn-clauses into a basis for higher-order program verification.
No least-model property.
- Converted it into the monotone problem
- So we can use an efficient solver for the monotone problem.
Collection of mutually-recursive functions.
- Then, they want the "summaries" to be invariant, or something..
- "Overapproximation" of the graph relating the mutual recusions.. oh, duh.
- I think he's just saying that every time they can't tell whether something's connected, they just assume it is.
- Then, they add invariants to the collection until the result has a solution. (refining it).. as usual.
Higher-order "twists", e.g. higher-order "unknown" relations.
- (He gives example of function with multiple args, not too uncommon.. xD)
"Everything's simply typed"
Two distinct minimal models, thus no least model, gives rise to theorem:
-
There is a system of higher-order constrained Horn clauses with two minimal models.
-
Because no monotonicity in general.
- Obvious solution: just exclude everything that's not monotone.
-
Hybrid solution "best of both":
- Specify verification problems in standard semantics but compute solutions using monotone problems.
Theorem:
-
Let H be a system of higher-order constrained Horn clauses. Then H is satisfiable in the standard semantics iff H is satisfiable in the monotone semantics.
-
Galois-theory something, something?
-
Use an adjoint map to preserve quality of being a solution.
- (Category theory summary/diagram)
How they solve HOCHCs:
- Theorem: "If there is a type env. Gamma which types a system H of higher-order constrained Horn clauses, then Gamma rep. a model of H."
"Using standard techniques, typability reduces to first-order CHC solving."
- CHC = Constrained Horn Clause
github.com/penteract/HigherOrderHornRefinement
Next:
- apply defunctionalization techniques to Horn clauses
- are HOCHS's expressive (Cook)
- are models with higher-order constraints more accurate/modular than first-order constraints
Only have a prototype solver, so can't talk about scalability.
- i.e. "research" lol
The same as other work, but this is the logic version and the noted paper was the type-theory version, but they're doing similar stuff.