Level: L3 Info-Math, M1
Contact: Burkhart Wolff
Summary.HOL-Bee is a semantic Frontend for Abrial's Event-B Method in Isabelle/HOL. It permits to edit specifications in the Event-B language inside the eco-sytem of Isabelle (IDE, kernel, code-generator, proof-system, libraries) and to generate its semantic representation in form of state-relations.
In this internship, the objective is to extend this functionality by generating the proof-obligations
and elementary proof-support. (Read the detailed internship proposal.).