Email Gateway (Aug 22 2022 at 16:15): Email Gateway (Aug 22 2022 at 16:15):From: Gerwin.Klein@data61.csiro.au
The AFP is now available for Isabelle2017.
With the new release two new entries from the development version have become available from the front page on https://www.isa-afp.org/
Dictionary Construction
by Lars Hupel
Isabelle's code generator natively supports type classes. For targets that do not have language support for classes and instances, it performs the well-known dictionary translation, as described by Haftmann and Nipkow. This translation happens outside the logic, i.e., there is no guarantee that it is correct, besides the pen-and-paper proof. This work implements a certified dictionary translation that produces new class-free constants and derives equality theorems.
https://www.isa-afp.org/entries/Dict_Construction.html
Stone-Kleene Relation Algebras
by Walter Guttmann
We develop Stone-Kleene relation algebras, which expand Stone relation algebras with a Kleene star operation to describe reachability in weighted graphs. Many properties of the Kleene star arise as a special case of a more general theory of iteration based on Conway semirings extended by simulation axioms. This includes several theorems representing complex program transformations. We formally prove the correctness of Conway's automata-based construction of the Kleene star of a matrix. We prove numerous results useful for reasoning about weighted graphs.
https://www.isa-afp.org/entries/Stone_Kleene_Relation_Algebras.html
With Isabelle2017's new session-qualified theory imports it has now become easier to refer to AFP entries in your own developments and for AFP entries to refer to each other. We have updated the instructions on the AFP website accordingly.
The AFP now contains over 1.7 million lines of proof with over 100,000 lemmas in 377 articles from 266 authors. Keep them coming!
Enjoy!
Gerwin
Last updated: Apr 26 2024 at 08:19 UTC