diff --git a/CITATION b/CITATION index 5fb01eb..82db007 100644 --- a/CITATION +++ b/CITATION @@ -8,22 +8,34 @@ To cite Isabelle/DOF in publications, please use A BibTeX entry for LaTeX users is -@InCollection{ brucker.ea:isabelle-ontologies:2018, - url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018}, - keywords = {Isabelle/Isar, HOL, Ontologies}, - location = {Hagenberg, Austria}, - author = {Achim D. Brucker and Idir Ait-Sadoune and Paolo Crisafulli - and Burkhart Wolff}, - booktitle = {Conference on Intelligent Computer Mathematics (CICM)}, - language = {USenglish}, - publisher = {Springer-Verlag}, - address = {Heidelberg}, - series = {Lecture Notes in Computer Science}, - title = {Using The Isabelle Ontology Framework: Linking the Formal - with the Informal}, - classification= {conference}, - areas = {formal methods, software engineering}, - public = {yes}, - year = {2018}, - pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf} -} +@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}, +} diff --git a/README.md b/README.md index 4ef977d..b0a8192 100644 --- a/README.md +++ b/README.md @@ -142,6 +142,7 @@ SPDX-License-Identifier: BSD-2-Clause ## Publications * 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. + Wolff. [Using The Isabelle Ontology Framework: Linking the Formal + with the Informal]({https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf). + In Conference on Intelligent Computer Mathematics (CICM). Lecture + Notes in Computer Science (11006), Springer-Verlag, 2018.