Hi guys,

There is a style in program analysis where people use lattice theory and order a lot.

For example, they may use least-fixed-point of a monotonic function, which exists on a complete lattice by Tarski-Knaster's theorem, in order to give an inductive definition; following that, they may use it to show that the inductive object subsets another object.

Ordinarily they use the powerset of program properties of interest as the lattice.

There's other nice properties they get through this: for example, monotonic functions that preserve joins now define adjoints and so interpreters using the image set of these monotonic functions as their domain are now sound wrt the original program (abstract interpretation).

http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/asl-short.pdf is the paper where I want to know whether the theorems are easy to embed in Coq. I'd be especially happy if there's a framework that allows you to instantiate all of these objects in an algebraic way, like modules and functors over sets.

So, are there good Coq libraries for lattices and order that allow you to define, e.g., the union over properties?

@Jacob Salzberg see the MathComp library (#math-comp users) and in particular https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/order.v and https://github.com/imdea-software/htt/blob/master/htt/domain.v

abstract interpretation was done for CompCert here: https://people.irisa.fr/Vincent.Laporte/popl15.pdf

Last updated: Jun 13 2024 at 19:02 UTC