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 089f7b4..483cd7b 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 @@ -108,7 +108,7 @@ volume = 2283, doi = {10.1007/3-540-45949-9}, abstract = {This book is a self-contained introduction to interactive - proof in higher-order logic (\acs{hol}), using the proof + proof in higher-order logic HOL, using the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for researchers. The book has three parts. @@ -121,7 +121,7 @@ such advanced topics as nested and mutual recursion. 2. Logic and Sets presents a collection of lower-level tactics that you can use to apply rules selectively. It also - describes Isabelle/\acs{hol}'s treatment of sets, functions + describes Isabelle/HOL's treatment of sets, functions and relations and explains how to define sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib index 771ccaa..f9e86ab 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib @@ -4334,6 +4334,23 @@ isbn="978-3-540-48509-4" acknowledgement={none} } +@incollection{Tuong-IsabelleC:2019, + address = {Heidelberg}, + author = {Fr\'ederic Tuong and Burkhart Wolff}, + booktitle = {International Workshop on Formal Integrated Development Environments (F-IDE)}, + doi = {10.4204/EPTCS.310.3}, + keywords = {Isabelle, HOL, C11, Program Verification, Program Testing}, + language = {USenglish}, + location = {Porto, Protogal}, + number = {314}, + pdf = {https://www.lri.fr/~wolff/papers/conf/2019-fide-isabelle_c.pdf}, + publisher = {Open Publishing Association}, + series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)}, + title = {{D}eeply {I}ntegrating {C11} {C}ode {S}upport into {I}sabelle/{PIDE}}, + year = {2019} +} + + @InProceedings{ bishop.ea:rigorous:2005, author = {Steve Bishop and Matthew Fairbairn and Michael Norrish and Peter Sewell and Michael Smith and Keith Wansbrough}, diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 756e602..05b44dc 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -53,29 +53,50 @@ propagation. This challenge incites numerous research efforts summarized under the labels ``semantic web'', ``data mining'', or any form of advanced ``semantic'' text processing. Turning informal into (more) formal content is the key for advanced techniques of research, -combination, and the maintenance of consistency in the midst of data evolution. +combination, and the maintenance of consistency in evolving data. Admittedly, Isabelle is not the first system that comes into one's mind when writing a document, be it a scientific paper, a book, or a larger technical documentation. However, it has a typesetting system inside which is in the tradition of document generation systems such as mkd, Document! X, Doxygen, -Javadoc, etc., which embed elements of formal content such as code-snippets +Javadoc, etc., and which embed elements of formal content such as code-snippets or generated system output into informal text. In Isabelle, these "embedders" or meta-text elements are a form of machine-checked macro called \<^emph>\antiquotations\. For example, the text element as appearing in the Isabelle frontend: -@{theory_text [display] - \ According to the reflexivity axiom @{thm refl}, we obtain in \ - for @{term "fac 5"} the result @{value "fac 5"}.\} -is represented in the generated LaTeX or HTML output by: -@{theory_text [display] +@{theory_text [display,indent=10, margin=70] +\ + text\ According to the reflexivity axiom @{thm refl}, we obtain in \ + for @{term "fac 5"} the result @{value "fac 5"}.\ + +\} +is represented in the generated \<^latex>\\ or HTML output by: +@{theory_text [display,indent=10, margin=70] \According to the reflexivity axiom \x = x\, we obtain in \ for \fac 5\ the result \120\.\ } where the meta-texts \@{thm refl}\ ("give the presentation of theorem 'refl'), \@{term "fac 5"}\ ("parse and type-check 'fac 5' in the previous logical context) and \@{value "fac 5"}\ ("compile and execute 'fac 5' according to its -definitions in the previous logical context) are built-in antiquotations -in \<^hol>. +definitions") are built-in antiquotations in \<^hol>. + +%too long ! +Hence, developers are rewarded for an evolution strategy consisting in +source integration in Isabelle and replacing \<^emph>\text\ by appropriate \<^emph>\meta-text\: +the resulting semantic checks increase the robustness of the document +consistency under (usually collaborative) changes. +%For example, if someone changes the theorem name, an error would result when processing +%the text. On the other hand, \@{value "fac 5"}\ would not guard against a change of definition +%of \fac\. If this is desirable, an antiquotation like \@{assert "fac 5 = 120"}\ would be more appropriate. +%too long ! +Antiquotations do not only occur in text-elements in Isabelle; they are also heavily used +in the code-elements of Isabelle's SML implementation, or were specifically supported in +C-program contexts in Isabelle/C @{cite "Tuong-IsabelleC:2019"}. + +However, programming antiquotations on the intern Isabelle API's is nothing for the +faint-hearted. Recently \<^dof> @{cite "10.1007/978-3-030-30446-1_15" and "10.1007/978-3-319-96812-4_3"} +has been designed as an Isabelle component that \<^emph>\generates\ antiquotation languages +from a more abstract level, namely an \<^emph>\ontology description\ that provides typed meta-data +and typed reference mechanisms inside text- and ML-contexts.