From dc7ed74c570c2ae1cf5fad28714b2cd352a1f509 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 4 Nov 2020 10:12:31 +0100 Subject: [PATCH] Second steps to reform cicm paper --- .../IsaDofApplications.thy | 26 +++++++++++++------ .../document/preamble.tex | 6 ++--- .../document/root.bib | 18 +++++++++++++ .../2020-iFM-CSP/document/root.bib | 19 +++++++++++++- .../scholarly_paper/2020-iFM-CSP/paper.thy | 2 ++ 5 files changed, 59 insertions(+), 12 deletions(-) diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy index a99c644..47abf77 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy @@ -21,8 +21,15 @@ declare[[strict_monitor_checking=false]] setup \ DOF_lib.define_shortcut \<^binding>\isadof\ "\\isadof" #> DOF_lib.define_shortcut \<^binding>\LaTeX\ "\\LaTeX{}" + #> DOF_lib.define_shortcut \<^binding>\Protege\ "Prot{\\'e}g{\\'e}" #> DOF_lib.define_shortcut \<^binding>\dots\ "\\ldots" - #> DOF_lib.define_shortcut \<^binding>\isabelle\ "Isabelle/HOL"\ + #> DOF_lib.define_shortcut \<^binding>\isabelle\ "Isabelle/HOL" + +\ + +(* slanted text in contrast to italics *) +setup\ DOF_lib.define_macro \<^binding>\slanted_text\ "\\textsl{" "}" (K(K()))\ + (*>*) @@ -61,6 +68,9 @@ abstract*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''I ontologies inside \<^isadof>, how to use the resulting meta-information for enforcing a certain document structure, and discuss ontology-specific IDE support. + + %% If you consider citing this paper, please refer to + %% @{cite "brucker.ea:isabelle-ontologies:2018"}. \ section*[intro::introduction]\ Introduction \ @@ -121,21 +131,21 @@ scenarios from the point of view of the ontology modeling. In @{text_section (un we discuss the user-interaction generated from the ontological definitions. Finally, we draw conclusions and discuss related work in @{text_section (unchecked) \conclusion\}. \ -section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"] +section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"] \ Background: The Isabelle System \ text*[background::introduction]\ While Isabelle is widely perceived as an interactive theorem prover for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize the view that Isabelle is far more than that: it is the \<^emph>\Eclipse of Formal Methods Tools\. This refers to the -``\textsl{generic system framework of Isabelle/Isar underlying recent +``\<^slanted_text>\generic system framework of Isabelle/Isar underlying recent versions of Isabelle. Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising extensible state components and extensible syntax that can be bound to ML programs. Thus, the Isabelle/Isar architecture may be understood as an extension and refinement of the traditional `LCF approach', with explicit infrastructure for building derivative - \<^emph>\systems\.}''~@{cite "wenzel.ea:building:2007"} + \<^emph>\systems\.\''~@{cite "wenzel.ea:building:2007"} The current system framework offers moreover the following features: @@ -152,10 +162,10 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit asynchronous communication between the Isabelle system and the IDE (right-hand side). \ -text*[blug::introduction]\ The Isabelle system architecture shown in @{docitem \architecture\} +text*[blug::introduction]\ The Isabelle system architecture shown in @{figure \architecture\} comes with many layers, with Standard ML (SML) at the bottom layer as implementation language. The architecture actually foresees a \<^emph>\Nano-Kernel\ (our terminology) which -resides in the SML structure \texttt{Context}. This structure provides a kind of container called +resides in the SML structure \<^ML_structure>\Context\. This structure provides a kind of container called \<^emph>\context\ providing an identity, an ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>. On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific support for higher specification constructs @@ -715,7 +725,7 @@ on documents mixing formal and informal content---a type of documents that is very common in technical certification processes. We see mainly one area of related works: IDEs and text editors that support editing and checking of documents based on an ontology. There is a -large group of ontology editors (\<^eg>, Prot{\'e}g{\'e}~@{cite "protege"}, +large group of ontology editors (\<^eg>, \<^Protege>~@{cite "protege"}, Fluent Editor~@{cite "cognitum"}, NeOn~@{cite "neon"}, or OWLGrEd~@{cite "owlgred"}). With them, we share the support for defining ontologies as well as auto-completion when editing documents based on @@ -725,7 +735,7 @@ OWLGrEd~@{cite "owlgred"}) also support graphical notations. This could be added to \<^isadof> in the future. A unique feature of \<^isadof> is the deep integration of formal and informal text parts. The only other work in this area we are aware of is rOntorium~@{cite "rontorium"}, a plugin -for Prot{\'e}g{\'e} that integrates R~@{cite "adler:r:2010"} into an +for \<^Protege> that integrates R~@{cite "adler:r:2010"} into an ontology environment. Here, the main motivation behind this integration is to allow for statistically analyze ontological documents. Thus, this is complementary to our work. diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex index bb39d89..1cccaa2 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex @@ -55,9 +55,9 @@ \subject{Example of an Academic Paper\footnote{% - This document is an example setup for writing academic paper. While - it is optimized for Springer's LNCS class, it uses a Koma Script - LaTeX class to avoid the need for distributing \texttt{llncs.cls}, + This document is an example setup for writing an academic paper. While + it is optimized for the Springer's LNCS class, it uses a Koma Script + LaTeX class to avoid the re-distribution of \texttt{llncs.cls}, which would violate Springer's copyright. This example has been published at CICM 2018: \protect\begin{quote} diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib index de3c5c6..089f7b4 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib @@ -279,3 +279,21 @@ year = {2018} } +@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/examples/scholarly_paper/2020-iFM-CSP/document/root.bib b/examples/scholarly_paper/2020-iFM-CSP/document/root.bib index d42138b..9093829 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/document/root.bib +++ b/examples/scholarly_paper/2020-iFM-CSP/document/root.bib @@ -11308,5 +11308,22 @@ abstract="In this paper, we present various extensions of Isabelle/HOL by theori isbn="978-3-642-16690-7" } - +@incollection{HOL-CSP-iFM2020, + keywords = {Process-Algebra, Concurrency, Computational Models, Parametric System Verification}, + author = {Safouan Taha and Lina Ye and Burkhart Wolff}, + booktitle = {Integrated Formal Methods (iFM)}, + language = {USenglish}, + publisher = {Springer-Verlag}, + address = {Heidelberg}, + series = {Lecture Notes in Computer Science}, + number = {12546}, + doi = {10.1007/978-3-030-63461-2_23}, + editor = {Carlo A. Furia}, + title = {{P}hilosophers may {D}ine - {D}efinitively!}, + pdf = {https://www.lri.fr/~wolff/papers/conf/2020-iFM_CSP.pdf}, + classification = {conference}, + areas = {formal methods, software}, + year = {2020}, + public = {yes} +} diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index 097d797..34bf1f0 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -45,6 +45,8 @@ abstract*[abs, keywordlist="[\Shallow Embedding\,\Process-Alg We demonstrate a number of resulting verification-techniques for classical, generalized examples: The CopyBuffer and Dijkstra's Dining Philosopher Problem of an arbitrary size. + + If you consider citing this paper, please refer to @{cite "HOL-CSP-iFM2020"}. \ text\\<^vs>\-1.3cm\\ section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\ Introduction \