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

tested and enforced new author* and abstract* macros.

This commit is contained in:
Burkhart Wolff 2020-11-04 02:52:55 +01:00
parent 0b52e5872d
commit c991e693dc
2 changed files with 37 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

61
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
View File

@ -22,39 +22,38 @@ declare[[strict_monitor_checking=false]]
title*[tit::title]\<open>Using the Isabelle Ontology Framework\<close>
subtitle*[stit::subtitle]\<open>Linking the Formal with the Informal\<close>
text*[adb:: author,
email="''a.brucker@sheffield.ac.uk''",
orcid="''0000-0002-6355-1200''",
affiliation="''The University of Sheffield, Sheffield, UK''"]\<open>Achim D. Brucker\<close>
text*[idir::author,
email = "''idir.aitsadoune@centralesupelec.fr''",
affiliation = "''CentraleSupelec, Paris, France''"]\<open>Idir Ait-Sadoune\<close>
text*[paolo::author,
email = "''paolo.crisafulli@irt-systemx.fr''",
affiliation= "''IRT-SystemX, Paris, France''"]\<open>Paolo Crisafulli\<close>
text*[bu::author,
email = "\<open>wolff@lri.fr\<close>",
affiliation = "\<open>Université Paris-Saclay, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
author*[adb,
email ="''a.brucker@sheffield.ac.uk''",
orcid ="''0000-0002-6355-1200''",
affiliation ="''The University of Sheffield, Sheffield, UK''"]\<open>Achim D. Brucker\<close>
author*[idir,
email = "''idir.aitsadoune@centralesupelec.fr''",
affiliation = "''CentraleSupelec, Paris, France''"]\<open>Idir Ait-Sadoune\<close>
author*[paolo,
email = "''paolo.crisafulli@irt-systemx.fr''",
affiliation = "''IRT-SystemX, Paris, France''"]\<open>Paolo Crisafulli\<close>
author*[bu,
email = "\<open>wolff@lri.fr\<close>",
affiliation = "\<open>Université Paris-Saclay, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
text*[abs::abstract,
keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\<open>
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 \isadof, a novel Document Ontology Framework
on top of Isabelle. \isadof allows for conventional typesetting
\<^emph>\<open>as well\<close> as formal development. We show how to model document
ontologies inside \isadof, how to use the resulting meta-information
for enforcing a certain document structure, and discuss ontology-specific IDE support.
abstract*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\<open>
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 \isadof, a novel Document Ontology Framework
on top of Isabelle. \isadof allows for conventional typesetting
\<^emph>\<open>as well\<close> as formal development. We show how to model document
ontologies inside \isadof, how to use the resulting meta-information
for enforcing a certain document structure, and discuss ontology-specific IDE support.
\<close>
section*[intro::introduction]\<open> Introduction \<close>

23
examples/scholarly_paper/2020-iFM-CSP/paper.thy
View File

@ -18,27 +18,18 @@ title*[tit::title]\<open>Philosophers may Dine - Definitively!\<close>
author*[safouan, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
\<open>Safouan Taha\<close>
(*
author*[safouann::author, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
\<open>Safouan Taha\<close>
text*[safouannn::author, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
\<open>Safouan Taha\<close>
*)
text*[bu::author, email= "''wolff@lri.fr''",affiliation = "\<open>LRI, Université Paris-Saclay\<close>"]
author*[bu, email= "''wolff@lri.fr''",affiliation = "\<open>LRI, Université Paris-Saclay\<close>"]
\<open>Burkhart Wolff\<close>
text*[lina::author,email="''lina.ye@lri.fr''",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]
author*[lina,email="''lina.ye@lri.fr''",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]
\<open>Lina Ye\<close>
abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
\<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
\<open> The theory of Communicating Sequential Processes going back to Hoare and Roscoe is
still today one of the reference theories for concurrent specification and computing.
In 1997, a first formalization in \<^isabelle> of the denotational semantics of the
Failure/Divergence Model of \<^csp> was undertaken; in particular, this model can cope with infinite
alphabets, in contrast to model-checking approaches limited to finite ones.
\<open> The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today
one of the reference theories for concurrent specification and computing. In 1997, a first
formalization in \<^isabelle> of the denotational semantics of the Failure/Divergence Model of
\<^csp> was undertaken; in particular, this model can cope with infinite alphabets, in contrast
to model-checking approaches limited to finite ones.
In this paper, we extend this theory to a significant degree by taking advantage of more powerful
automation of modern Isabelle version, which came even closer to recent developments in the
semantic foundation of \<^csp>.