forked from Isabelle_DOF/Isabelle_DOF
Added citation information.
This commit is contained in:
parent
0c2e2869a7
commit
90add40145
|
|
@ -74,24 +74,50 @@ text\<open>
|
|||
lemma refl: "x = x"
|
||||
by simp
|
||||
\end{isar}
|
||||
\<^item> For small examples of generated document, we use a green background:
|
||||
\<^item> a green background for examples of generated document fragments (\ie, PDF output):
|
||||
\begin{out}
|
||||
The axiom refl
|
||||
\end{out}
|
||||
\<^item> For (S)ML-code, we use a red background:
|
||||
\<^item> a red background for For (S)ML-code:
|
||||
\begin{sml}
|
||||
fun id x = x
|
||||
\end{sml}
|
||||
\<^item> \LaTeX-code, we use a yellow background:
|
||||
\<^item> a yellow background for \LaTeX-code:
|
||||
\begin{ltx}
|
||||
\newcommand{\refl}{$x = x$}
|
||||
\end{ltx}
|
||||
\<^item> For shell scripts and interative shell sessions, we use a grey background:
|
||||
\<^item> a grey background for shell scripts and interactive shell sessions:
|
||||
\begin{bash}
|
||||
achim@logicalhacking:~/Isabelle_DOF$ ls
|
||||
CHANGELOG.md CITATION examples install LICENSE README.md ROOTS src
|
||||
\end{bash}
|
||||
\<close>
|
||||
|
||||
subsubsection\<open>How to Cite \isadof\<close>
|
||||
text\<open>
|
||||
If you use or extend \isadof in your publications, please use
|
||||
\<^item> for the \isadof system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
|
||||
\begin{quote}\small
|
||||
A.~D. Brucker, I.~Ait-Sadoune, P.~Crisafulli, and B.~Wolff. Using the {Isabelle} ontology
|
||||
framework: Linking the formal with the informal. In \emph{Conference on Intelligent Computer
|
||||
Mathematics (CICM)}, number 11006 in Lecture Notes in Computer Science. Springer-Verlag,
|
||||
Heidelberg, 2018. \href{https://doi.org/10.1007/978-3-319-96812-4\_3}
|
||||
{10.1007/978-3-319-96812-4\_3}.
|
||||
\end{quote}
|
||||
A \BibTeX-entry is available at:
|
||||
\url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018}.
|
||||
\<^item> for the implementation of \isadof~@{cite "brucker.ea:isabelledof:2019"}:
|
||||
\begin{quote}\small
|
||||
A.~D. Brucker and B.~Wolff. \isadof: Design and implementation. In P.~{\"O}lveczky and
|
||||
G.~Sala{\"u}n, editors, \emph{Software Engineering and Formal Methods (SEFM)}, Lecture Notes
|
||||
in Computer Science. Springer-Verlag, Heidelberg, 2019.
|
||||
\end{quote}
|
||||
A \BibTeX-entry is available at:
|
||||
\url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019}.
|
||||
|
||||
|
||||
The source code of \isadof is available at
|
||||
\url{https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}.
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
|
|
|
|||
|
|
@ -21,9 +21,7 @@
|
|||
\usepackage{listings}
|
||||
\usepackage{lstisadof-manual}
|
||||
\usepackage{xspace}
|
||||
\usepackage[draft]{fixme}
|
||||
|
||||
|
||||
\usepackage{dtk-logos}
|
||||
\usepackage[caption]{subfig}
|
||||
\usepackage[size=footnotesize]{caption}
|
||||
\usepackage{railsetup}
|
||||
|
|
|
|||
|
|
@ -1,3 +1,101 @@
|
|||
|
||||
|
||||
|
||||
|
||||
@InCollection{ brucker.ea:isabelledof:2019,
|
||||
abstract = {DOF is a novel framework for defining ontologies and
|
||||
enforcing them during document development and evolution. A
|
||||
major goal of DOF is the integrated development of formal
|
||||
certification documents (e. g., for Common Criteria or
|
||||
CENELEC 50128) that require consistency across both formal
|
||||
and informal arguments.
|
||||
|
||||
To support a consistent development of formal and informal
|
||||
parts of a document, we provide Isabelle/DOF, an
|
||||
implementation of DOF on top of the formal methods
|
||||
framework Isabelle/HOL. A particular emphasis is put on a
|
||||
deep integration into Isabelle{\^a}s IDE, which allows for
|
||||
smooth ontology development as well as immediate
|
||||
ontological feedback during the editing of a document.
|
||||
|
||||
In this paper, we give an in-depth presentation of the
|
||||
design concepts of DOF{\^a}s Ontology Definition Language
|
||||
(ODL) and key aspects of the technology of its
|
||||
implementation. Isabelle/DOF is the first ontology language
|
||||
supporting machine-checked links between the formal and
|
||||
informal parts in an LCF-style interactive theorem proving
|
||||
environment. Sufficiently annotated, large documents can
|
||||
easily be developed collabo- ratively, while ensuring their
|
||||
consistency, and the impact of changes (in the formal and
|
||||
the semi-formal content) is tracked automatically.},
|
||||
keywords = {Ontology, Formal Document Development, CERtification, DOF,
|
||||
Isabelle/DOF},
|
||||
location = {Oslo},
|
||||
author = {Achim D. Brucker and Burkhart Wolff},
|
||||
booktitle = {Software Engineering and Formal Methods (SEFM)},
|
||||
language = {USenglish},
|
||||
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019},
|
||||
publisher = {Springer-Verlag},
|
||||
address = {Heidelberg},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
isbn = {3-540-25109-X},
|
||||
editor = {Peter {\"O}lveczky and Gwen Sala{\"u}n},
|
||||
pdf = {https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf},
|
||||
title = {{Isabelle/DOF}: Design and Implementation},
|
||||
classification= {conference},
|
||||
areas = {formal methods, software},
|
||||
categories = {isadof},
|
||||
year = {2019},
|
||||
public = {yes}
|
||||
}
|
||||
|
||||
@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.},
|
||||
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},
|
||||
number = {11006},
|
||||
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018},
|
||||
title = {Using the {Isabelle} Ontology Framework: Linking the
|
||||
Formal with the Informal},
|
||||
classification= {conference},
|
||||
areas = {formal methods, software},
|
||||
categories = {isadof},
|
||||
public = {yes},
|
||||
year = {2018},
|
||||
doi = {10.1007/978-3-319-96812-4_3},
|
||||
pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf}
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
@STRING{pub-springer={Springer} }
|
||||
@STRING{pub-springer:adr=""}
|
||||
@STRING{s-lncs = "LNCS" }
|
||||
|
|
@ -138,18 +236,6 @@
|
|||
timestap = {2008-05-26}
|
||||
}
|
||||
|
||||
@InProceedings{ brucker.ea:isabelle-ontologies:2018,
|
||||
author = {Brucker, Achim D. and Ait-Sadoune, Idir and Crisafulli, Paolo and Wolff, Burkhart},
|
||||
title = {Using the {Isabelle} ontology framework: Linking the formal with the informal.},
|
||||
publisher = pub-springer,
|
||||
address = pub-springer:adr,
|
||||
series = s-lncs,
|
||||
volume = 11006,
|
||||
year = 2018,
|
||||
doi = {10.1007/978-3-319-96812-4_3},
|
||||
booktitle = {Conference on Intelligent Computer Mathematics (CICM)}
|
||||
}
|
||||
|
||||
@InProceedings{ wenzel:asynchronous:2014,
|
||||
author = {Makarius Wenzel},
|
||||
title = {Asynchronous User Interaction and Tool Integration in
|
||||
|
|
|
|||
Loading…
Reference in New Issue