Isabelle/DOF

@Article{ brucker.ea:isabelle-dof-afp:2024,
  author   = {Achim D. Brucker and Nicolas M{\'e}ric and Burkhart Wolff},
  title    = {{Isabelle/DOF}},
  journal  = {Archive of Formal Proofs},
  month    = {apr},
  year     = {2024},
  date     = {2024-01-21},
  note     = {\url{https://www.isa-afp.org/entries/Isabelle_DOF.html},
              Formal proof development. 
              Author copy: \url{https://logicalhacking.com/publications/brucker.ea-isabelle-dof-afp-2024/}},
  issn     = {2150-914x},
  areas    = {formal methods, software engineering},
  abstract = {Isabelle/DOF provides an implementation of a document
              ontology framework on top of Isabelle/HOL. The framework
              allows both for defining ontologies and enforcing them during
              document development and document evolution. Isabelle/DOF
              targets use-cases such as mathematical texts referring to a
              theory development or technical reports requiring a particular
              structure. The documentation generation features are
              sufficiently powerful to typeset the most common cases without
              using LaTeX. Isabelle/DOF is integrated into Isabelle's IDE,
              which allows for smooth ontology development as well as
              immediate ontological conformance-checks during the editing of
              a document. Its checking facilities leverage the collaborative
              development of documents required to be consistent with an
              underlying ontological structure. This entry provides a
              user-manual with in-depth presentation of the design concepts
              of Isabelle/DOF's Ontology Definition Language (ODL) and
              describe comprehensively its major commands. Many examples
              show typical best-practice applications of the system.},
  pdf      = {https://logicalhacking.com/publications/brucker.ea-isabelle-dof-afp-2024/brucker.ea-isabelle-dof-afp-2024.pdf},
}