Email Gateway (Aug 19 2022 at 12:33): Email Gateway (Aug 19 2022 at 12:33):From: Lawrence Paulson <lp15@cam.ac.uk>
New AFP entries are available from http://afp.sf.net
FocusStreamsCaseStudies
Maria Spichkova
An Isabelle/HOL formalisation of stream processing components introduced in Focus, a framework for formal specification and development of interactive systems. This is an extended and updated version of the formalisation, which was elaborated within the methodology "Focus on Isabelle". In addition, we also applied the formalisation on three case studies that cover different application areas: process control (Steam Boiler System), data transmission (FlexRay communication protocol), memory and processing components (Automotive-Gateway System).
GoedelGod
Christoph Benzmüller
Dana Scott's version of Gödel's proof of God's existence is formalized in quantified modal logic KB (QML KB). QML KB is modeled as a fragment of classical higher-order logic (HOL); thus, the formalization is essentially a formalization in HOL.
Larry Paulson
Email Gateway (Aug 22 2022 at 12:05):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce two new developments in the AFP. The first is a package for applicative functors, and the second uses that package to formalise the Stern-Brocot tree, which contains all rational numbers exactly once and in their lowest terms.
http://afp.sourceforge.net/entries/Applicative_Lifting.shtml
http://afp.sourceforge.net/entries/Stern_Brocot.shtml
Many thanks to the authors for their contributions!
Larry Paulson
Last updated: Apr 26 2024 at 12:28 UTC