Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Two new AFP entries: "Public Announcement Logi...

view this post on Zulip Email Gateway (Jun 25 2021 at 10:12):

From: "Thiemann, René" <>
Dear all,

I’m happy to announce two new AFP entries.

Public Announcement Logic
by Asta Halkjær

This work is a formalization of public announcement logic with
countably many agents. It includes proofs of soundness and
completeness for a variant of the axiom system PA + DIST! + NEC!. The
completeness proof builds on the Epistemic Logic theory.

MiniSail - A kernel language for the ISA specification language SAIL
by Mark Wassell

MiniSail is a kernel language for Sail, an instruction set
architecture (ISA) specification language. Sail is an imperative
language with a light-weight dependent type system similar to
refinement type systems. From an ISA specification, the Sail compiler
can generate theorem prover code and C (or OCaml) to give an
executable emulator for an architecture. The idea behind MiniSail is
to capture the key and novel features of Sail in terms of their
syntax, typing rules and operational semantics, and to confirm that
they work together by proving progress and preservation lemmas. We use
the Nominal2 library to handle binding.


Last updated: Sep 25 2021 at 09:17 UTC