[FOM] Fwd: [isabelle] two new AFP entries

[Serguei Mokhov]

JFYI:

---------- Forwarded message ----------
From: Lawrence Paulson <lp15 at cam.ac.uk>
Date: Mon, Nov 18, 2013 at 11:39 AM
Subject: [isabelle] two new AFP entries
To: isabelle-users <isabelle-users at cl.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





-- 
Serguei Mokhov
http://www.cs.concordia.ca/~mokhov
http://marf.sf.net | http://sf.net/projects/marf