The Luxembourg Fonds Nationals de Recherche (National Research Fund) has awarded an AFR to Richard Schmoetten to carry out his PhD research, under the supervision of Jacques Fleuriot, on “Formalising Haag-Kastler Nets in Higher-order Logic”. The work will be carried out in the proof assistant Isabelle.