Email Gateway (Aug 19 2022 at 16:16): Email Gateway (Aug 19 2022 at 16:16):From: Tobias Nipkow <nipkow@in.tum.de>
XML
Christian Sternagel and René Thiemann
This entry provides an XML library for Isabelle/HOL. This includes parsing and
pretty printing of XML trees as well as combinators for transforming XML trees
into arbitrary user-defined data. The main contribution of this entry is an
interface (fit for code generation) that allows for communication between
verified programs formalized in Isabelle/HOL and the outside world via XML. This
library was developed as part of the IsaFoR/CeTA project to which we refer for
examples of its usage.
http://afp.sourceforge.net/entries/XML.shtml
Certification Monads
Christian Sternagel and René Thiemann
This entry provides several monads intended for the development of stand-alone
certifiers via code generation from Isabelle/HOL. More specifically, there are
three flavors of error monads (the sum type, for the case where all monadic
functions are total; an instance of the former, the so called check monad,
yielding either success without any further information or an error message; as
well as a variant of the sum type that accommodates partial functions by
providing an explicit bottom element) and a parser monad built on top. All of
this monads are heavily used in the IsaFoR/CeTA project which thus provides many
examples of their usage.
http://afp.sourceforge.net/entries/Certification_Monads.shtml
Many thanks, Christian and René!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC