CITATION

To cite Isabelle/DOF in publications, please use
  
  Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
  Wolff. Using The Isabelle Ontology Framework: Linking the Formal
  with the Informal. In Conference on Intelligent Computer Mathematics
  (CICM). Lecture Notes in Computer Science, Springer-Verlag, 2018.
  
A BibTeX entry for LaTeX users is

@InCollection{ brucker.ea:isabelle-ontologies:2018,
	abstract  = {While Isabelle is mostly known as part of Isabelle/HOL (an 
                     interactive theorem prover), it actually provides a framework
                     for developing a wide spectrum of applications. A particular 
                     strength of the Isabelle framework is the combination of text 
                     editing, formal verification, and code generation.\\\\
                     Up to now, Isabelle's document preparation system lacks a mechanism 
                     for ensuring the structure of different document types (as, e.g.,
                     required in certification processes) in general and, in particular,
                     mechanism for linking informal and formal parts of a document.\\\\
                     In this paper, we present Isabelle/DOF, a novel Document Ontology 
                     Framework on top of Isabelle. Isabelle/DOF allows for conventional 
                     typesetting \emph{as well} as formal development. We show how to model 
                     document ontologies inside Isabelle/DOF, how to use the resulting 
                     meta-information for enforcing a certain document structure, and discuss 
                     ontology-specific IDE support.},
	address	  = {Heidelberg},
	author	  = {Achim D. Brucker and Idir Ait-Sadoune and Paolo Crisafulli and Burkhart Wolff},
	booktitle = {Conference on Intelligent Computer Mathematics (CICM)},
	doi	  = {10.1007/978-3-319-96812-4_3},
	keywords  = {Isabelle/Isar, HOL, Ontologies},
	language  = {USenglish},
	location  = {Hagenberg, Austria},
	number	  = {11006},
	pdf	  = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf},
	publisher = {Springer-Verlag},
	series	  = {Lecture Notes in Computer Science},
	title	  = {Using the {Isabelle} Ontology Framework: Linking the Formal with the Informal},
	url	  = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018},
	year	  = {2018},
}