Marcelo Fiore has been explaining his work on Abstract Domain Theory to me, and I think it would be nice to formalize some of it, especially over an arbitrary Grothendieck topos. One good step is to formalize a generalized notion of omega-cpo. The recipe seems to be the following:
Start with a lifting monad L on some category. For example, consider the lifting monad on posets.
Let \omega be the initial L-algebra. In SET with (+1), this is the natural numbers but in general, but it is natural to consider the topos's partial map classifier, and in that case you get something that looks like the natural numbers but also has some spooky stuff in there.
There is an algebraic structure of a "formally \omega-complete object" that one can define on top of your original category, explained in this paper.
If you start with posets and the set theoretic partial map classifier, you get exactly the theory of \omega-cpos. If you replace posets with sets, you get something kind of degenerate. But what is useful to me about this is that you can generate the "correct" theory of \omega-cpos for an arbitrary topos in this way. It would be excellent to work out the details in Coq.
Marcelo Fiore has been explaining his work on Abstract Domain Theory to me, and I think it would be nice to formalize some of it, especially over an arbitrary Grothendieck topos. One good step is to formalize a generalized notion of omega-cpo. The recipe seems to be the following:
Lon some category. For example, consider the lifting monad on posets.\omegabe the initialL-algebra. InSETwith(+1), this is the natural numbers but in general, but it is natural to consider the topos's partial map classifier, and in that case you get something that looks like the natural numbers but also has some spooky stuff in there.If you start with posets and the set theoretic partial map classifier, you get exactly the theory of \omega-cpos. If you replace posets with sets, you get something kind of degenerate. But what is useful to me about this is that you can generate the "correct" theory of \omega-cpos for an arbitrary topos in this way. It would be excellent to work out the details in Coq.