Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in the AFP: Orderings and Lattices, Quanta...


view this post on Zulip Email Gateway (Aug 22 2022 at 18:52):

From: Gerwin.Klein@data61.csiro.au
As set of 3 connected new AFP entries by Georg Struth:

Properties of Orderings and Lattices
https://www.isa-afp.org/entries/Order_Lattice_Props.html

These components add further fundamental order and lattice-theoretic concepts and properties to Isabelle's libraries. They follow by and large the introductory sections of the Compendium of Continuous Lattices, covering directed and filtered sets, down-closed and up-closed sets, ideals and filters, Galois connections, closure and co-closure operators. Some emphasis is on duality and morphisms between structures, as in the Compendium. To this end, three ad-hoc approaches to duality are compared.

Quantales
https://www.isa-afp.org/entries/Quantales.html
These mathematical components formalise basic properties of quantales, together with some important models, constructions, and concepts, including quantic nuclei and conuclei.

Transformer Semantics
https://www.isa-afp.org/entries/Transformer_Semantics.html

These mathematical components formalise predicate transformer semantics for programs, yet currently only for partial correctness and in the absence of faults. A first part for isotone (or monotone), Sup-preserving and Inf-preserving transformers follows Back and von Wright's approach, with additional emphasis on the quantalic structure of algebras of transformers. The second part develops Sup-preserving and Inf-preserving predicate transformers from the powerset monad, via its Kleisli category and Eilenberg-Moore algebras, with emphasis on adjunctions and dualities, as well as isomorphisms between relations, state transformers and predicate transformers.

Enjoy!
Gerwin


Last updated: Nov 21 2024 at 12:39 UTC