Email Gateway (Jun 25 2021 at 10:12): Email Gateway (Jun 25 2021 at 10:12):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
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.
https://www.isa-afp.org/entries/Public_Announcement_Logic.html
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.
https://www.isa-afp.org/entries/MiniSail.html
Enjoy,
René
Last updated: Jan 04 2025 at 20:18 UTC