Thursday 4 May 2023, 14:00, room 1Z56: Meta-information for Proof Objects, Nicolas Méric (LMF).

Isabelle/DOF is a framework on top of Isabelle/HOL for defining ontologies and enforcing them during proof development and document evolution. With Isabelle/DOF, text- and code- and term-context may contain a special form annotation, a kind of semantic macro that is called antiquotation.

As a novelty, Isabelle/DOF supports ontology-generated antiquotations within meta (proof) terms constructed in Isabelle/HOL via a reification mechanism. Thus term-context antiquotations can be used to add and validate meta-information to Isabelle/HOL proof terms. The mechanism is amenable both to calculations and proofs over meta-data.