[isabelle] new AFP entry: Knowledge-Based Programs

We're pleased to announce the availability of a new AFP entry on [http://afp.sf.net] that accompanies the ITP'11 paper of the same title:

Title: Knowledge-based programs
Author: Peter Gammie

 Knowledge-based programs (KBPs) are a formalism for directly
 relating agents' knowledge and behaviour. Here we present a
 general scheme for compiling KBPs to executable automata with a
 proof of correctness in Isabelle/HOL. We develop the algorithm
 top-down, using Isabelle's locale mechanism to structure these
 proofs, and show that two classic examples can be synthesised using
 Isabelle's code generator.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.