Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Updated bibliographic information.

This commit is contained in:
Achim D. Brucker 2019-01-09 10:31:51 +00:00
parent 1765432e9a
commit 60a0bbb9cb
2 changed files with 35 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
CITATION
View File

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

7
README.md
View File

@ -142,6 +142,7 @@ SPDX-License-Identifier: BSD-2-Clause
## Publications ## Publications
* Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart * Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
Wolff. Using The Isabelle Ontology Framework: Linking the Formal Wolff. [Using The Isabelle Ontology Framework: Linking the Formal
with the Informal. In Conference on Intelligent Computer Mathematics with the Informal]({https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf).
(CICM). Lecture Notes in Computer Science, Springer-Verlag, 2018. In Conference on Intelligent Computer Mathematics (CICM). Lecture
Notes in Computer Science (11006), Springer-Verlag, 2018.