Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF

This commit is contained in:
Achim D. Brucker 2019-07-17 14:25:38 +01:00
commit 9608575aff
11 changed files with 2966 additions and 32 deletions

View File

@ -744,8 +744,6 @@ consts ISA_docitem_attr :: "string \<Rightarrow> string \<Rightarrow> 'a" (
\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
(* PORT TO ISABELLE2018 *)
ML \<open>
(* Author: Frédéric Tuong, Université Paris-Saclay *)
(* Title: HOL/ex/Cartouche_Examples.thy

View File

@ -34,7 +34,7 @@ types, terms, proven theorems, code, or established assertions.
Based on a novel adaption of the Isabelle IDE, a document is checked to be
\<^emph>\<open>conform\<close> to a particular ontology---\isadof is designed to give fast user-feedback
\<^emph>\<open>during the capture of content\<close>. This is particularly valuable in case of document
changes, where the \<^emph>\<open>coherence\<close> between the formal and the informal parts of the
evolution, where the \<^emph>\<open>coherence\<close> between the formal and the informal parts of the
content can be mechanically checked.
To avoid any misunderstanding: \isadof is \<^emph>\<open>not a theory in HOL\<close>
@ -46,6 +46,8 @@ itself. \isadof is a plugin into the Isabelle/Isar
framework in the style of~@{cite "wenzel.ea:building:2007"}.
\<close>
(* declaring the forward references used in the subsequent section *)
(*<*)
declare_reference*[bgrnd::text_section]

View File

@ -6,8 +6,9 @@ begin
chapter*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]
\<open> Background: The Isabelle System \<close>
section*[bgrnd1::introduction]\<open>Document Processing in Isabelle\<close>
text*[background::introduction]\<open>
While Isabelle is widely perceived as an interactive theorem prover
While Isabelle @{cite "nipkow.ea:isabelle:2002"} 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>\<open>Eclipse of Formal Methods Tools\<close>. This refers to the
@ -43,10 +44,20 @@ resides in the SML structure \texttt{Context}. This structure provides a kind of
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
were built. \<close>
text\<open> We would like to detail the documentation generation of the architecture,
text\<open> Of particular interest for \dof is documentation generation of the architecture,
which is based on literate specification commands such as \inlineisar+section+ \ldots,
\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc.
\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc. Moreover, we assume that
\<^emph>\<open>inside\<close> text-elements, there are generic and extendible ways to add "semantic", i.e.
machine-checked sub-elements.
In the sequel, we will outline the general assumptions that \dof makes for the underlying
document model, and than explain how Isabelle as a framework fits into this picture.
\<close>
(*
Thus, a user can add a simple text:
\begin{isar}
text\<Open>This is a description.\<Close>
@ -71,8 +82,137 @@ text*[anti]\<open> Thus, antiquotations can refer to formal content, can be type
displayed and can be used for calculations before actually being typeset. When editing,
Isabelle's PIDE offers auto-completion and error-messages while typing the above
\<^emph>\<open>semi-formal\<close> content. \<close>
*)
section*["sec:background"::introduction]\<open>The Document Model\<close>
text\<open>
In this section, we explain the assumed document model underlying
\dof in general; in particular the concepts \<^emph>\<open>integrated document\<close>,
\<^emph>\<open>sub-document\<close> , \<^emph>\<open>text-element\<close> and \<^emph>\<open>semantic macros\<close> occurring
inside text-elements. Furthermore, we assume two different levels of
parsers (for \<^emph>\<open>outer\<close> and \<^emph>\<open>inner syntax\<close>) where the inner-syntax is basically a typed
$\lambda$-calculus and some Higher-order Logic (HOL).\<close>
figure*["fig:dependency"::figure,relative_width="50",src="''figures/document-hierarchy''"]\<open>
A Theory-Graph in the Document Model. \<close>
text\<open>
We assume a hierarchical document model, \ie, an \<^emph>\<open>integrated\<close>
document consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files) that
can depend acyclically on each other. Sub-documents can have different
document types in order to capture documentations consisting of
documentation, models, proofs, code of various forms and other
technical artifacts. We call the main sub-document type, for
historical reasons, \<^emph>\<open>theory\<close>-files. A theory file consists of a
\<^emph>\<open>header\<close>, a \<^emph>\<open>context definition\<close>, and a body consisting of a
sequence of \<^emph>\<open>command\<close>s (@{figure "fig:dependency"}). Even the
header consists of a sequence of commands used for introductory text
elements not depending on any context. The context-definition
contains an \inlineisar{import} and a \inlineisar{keyword} section,
for example:
\begin{isar}
theory Example (* Name of the "theory" *)
imports (* Declaration of "theory" dependencies *)
Main (* Imports a library called "Main" *)
keywords (* Registration of keywords defined locally *)
requirement (* A command for describing requirements *)
\end{isar}
where \inlineisar{Example} is the abstract name of the text-file,
\texttt{Main} refers to an imported theory (recall that the import
relation must be acyclic) and \inlineisar{keywords} are used to
separate commands from each other.\<close>
text\<open>We distinguish fundamentally two different syntactic levels:
\begin{compactenum}
\item the \emph{outer-syntax} (\ie, the syntax for commands) is processed
by a lexer-library and parser combinators built on top, and
\item the \emph{inner-syntax} (\ie, the syntax for $\lambda$-terms in
HOL) with its own parametric polymorphism type checking.
\end{compactenum}
On the semantic level, we assume a validation process for an
integrated document, where the semantics of a command is a
transformation \inlineisar+\<theta> \<rightarrow> \<theta>+ for some
system state \inlineisar+\<theta>+. This document model can be
instantiated with outer-syntax commands for common text elements, \eg,
\inlineisar+section{*...*}+ or \inlineisar+text{*...*}+. Thus, users can add informal text to a
sub-document using a text command:
\begin{isar}
text\<Open>This is a description.\<Close>
\end{isar}
This will type-set the corresponding text in, for example, a PDF document.
However, this translation is not necessarily one-to-one: text
elements can be enriched by formal, \ie, machine-checked content via
\emph{semantic macros}, called antiquotations:
\begin{isar}
text\<Open>According to the reflexivity axiom @{thm refl}, we obtain in \<Gamma>
for @{term "fac 5"} the result @{value "fac 5"}.\<Close>
\end{isar}
which is represented in the final document (\eg, a PDF) by:
\begin{out}
According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$.
\end{out}
Semantic macros are partial functions of type %
\inlineisar+\<theta> \<rightarrow> text+; since they can use the
system state, they can perform all sorts of specific checks or
evaluations (type-checks, executions of code-elements, references to
text-elements or proven theorems such as \inlineisar+refl+, which is
the reference to the axiom of reflexivity).
Semantic macros establish \<^emph>\<open>formal content\<close> inside informal content; they can be
type-checked before being displayed and can be used for calculations before being
typeset. They represent the device for linking the formal with the informal. \<close>
subsection*[bgrnd21::introduction]\<open>Implementability of the Assumed Document Model.\<close>
text\<open>
Batch-mode checkers for \dof can be implemented in all systems of the
LCF-style prover family, \ie, systems with a type-checked
\inlinesml{term}, and abstract \inlinesml{thm}-type for
theorems (protected by a kernel). This includes, \eg, ProofPower,
HOL4, HOL-light, Isabelle, as well as Coq and its derivatives. \dof
is, however, designed for fast interaction in an IDE. If a user wants
to benefit from this experience, only Isabelle and Coq have the
necessary infrastructure of asynchronous proof-processing and support
by a PIDE
@{cite "DBLP:conf/itp/Wenzel14" and "DBLP:journals/corr/Wenzel14" and "DBLP:conf/mkm/BarrasGHRTWW13"
and "Faithfull:2018:COQ:3204179.3204223"} which in many features
over-accomplishes the required features of \dof. For example, current Isabelle versions
offer cascade-syntaxes (different syntaxes and even parser-technologies
which can be nested along the \inlineisar+ \<Open> ... \<Close> + barriers, while
\dof actually only requires a 2-level syntax model.\<close>
figure*["fig:dof-ide"::figure,relative_width="80",src="''figures/cicm2018-combined''"]\<open>
The \isadof IDE (left) and the corresponding PDF (right).% , showing the first page
% of~\cite{brucker.ea:isabelle-ontologies:2018}. \<close>
text\<open> We call the present implementation of \dof on the
Isabelle platform \isadof. In
@{docitem "fig:dof-ide"}, a screen-shot of an introductory paper on \isadof
@{cite "brucker.ea:isabelle-ontologies:2018"} is shown;
this paper focusses on a number of application scenarios and user-interface aspects.
In @{docitem "fig:dof-ide"}, the \isadof PIDE can be seen on the left, while
the generated presentation in PDF is shown on the right.
Isabelle provides, beyond the features required for \dof, a lot of
additional benefits. For example, it also allows the asynchronous
evaluation and checking of the document content
@{cite "DBLP:conf/itp/Wenzel14" and "DBLP:journals/corr/Wenzel14" and
"DBLP:conf/mkm/BarrasGHRTWW13"}
and is dynamically extensible. Its PIDE provides a \<^emph>\<open>continuous build, continuous check\<close>
functionality, syntax highlighting, and IntelliSense-like auto-completion.
It also provides infrastructure for
displaying meta-information (\eg, binding and type annotation) as
pop-ups, while hovering over sub-expressions. A fine-grained
dependency analysis allows the processing of individual parts of
theory files asynchronously, allowing Isabelle to interactively
process large (hundreds of theory files) documents. Isabelle can
group sub-documents into sessions, \ie, sub-graphs of the
document-structure that can be ``pre-compiled'' and loaded
instantaneously, \ie, without re-processing. \<close>
(*<*)
end
(*>*)

View File

@ -6,13 +6,14 @@ begin
text*[bib::bibliography]\<open>References\<close>
(*<*)
close_monitor*[this]
text\<open>Resulting trace in doc\_item ''this'': \<close>
ML\<open>@{trace_attribute this}\<close>
(*<*)
end
(*>*)

View File

@ -1,4 +1,4 @@
session "IsaDof_Manual" = "Isabelle_DOF" +
session "IsaDofManual" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", quick_and_dirty = true]
theories
IsaDofManual
@ -21,3 +21,18 @@ session "IsaDof_Manual" = "Isabelle_DOF" +
"figures/srac-as-es-application.png"
"figures/Dogfood-figures.png"
"figures/IsaArchGlobal.png"
"figures/document-hierarchy.svg"
"figures/IsaArchInteract.png"
"figures/document-model.key"
"figures/PIDE-interaction.pdf"
"figures/document-model.pdf"
"figures/cicm2018-combined.png"
"figures/isabelle-architecture.svg"
"figures/Dogfood-figures.png"
"figures/cicm2018-dof.png"
"figures/isadof.png"
"figures/cicm2018-pdf.png"
"figures/IsaArch.odp"
"figures/document-hierarchy.pdf"
"figures/srac-definition.png"

View File

@ -57,3 +57,6 @@
\title{<TITLE>}
\author{<AUTHOR>}
\newcommand{\dof}{DOF\xspace}

View File

@ -138,7 +138,17 @@
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},
@ -279,3 +289,66 @@
year = {2018}
}
@InProceedings{ DBLP:conf/itp/Wenzel14,
author = {Makarius Wenzel},
title = {Asynchronous User Interaction and Tool Integration in
Isabelle/PIDE},
booktitle = {Interactive Theorem Proving (ITP)},
pages = {515--530},
year = 2014,
doi = {10.1007/978-3-319-08970-6_33},
timestamp = {Sun, 21 May 2017 00:18:59 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/Wenzel14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@InProceedings{ DBLP:journals/corr/Wenzel14,
author = {Makarius Wenzel},
title = {System description: Isabelle/jEdit in 2014},
booktitle = {Proceedings Eleventh Workshop on User Interfaces for
Theorem Provers, {UITP} 2014, Vienna, Austria, 17th July
2014.},
pages = {84--94},
year = 2014,
doi = {10.4204/EPTCS.167.10},
timestamp = {Wed, 03 May 2017 14:47:58 +0200},
biburl = {https://dblp.org/rec/bib/journals/corr/Wenzel14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@InProceedings{ DBLP:conf/mkm/BarrasGHRTWW13,
author = {Bruno Barras and Lourdes Del Carmen
Gonz{\'{a}}lez{-}Huesca and Hugo Herbelin and Yann
R{\'{e}}gis{-}Gianas and Enrico Tassi and Makarius Wenzel
and Burkhart Wolff},
title = {Pervasive Parallelism in Highly-Trustable Interactive
Theorem Proving Systems},
booktitle = {Intelligent Computer Mathematics - MKM, Calculemus, DML,
and Systems and Projects},
pages = {359--363},
year = 2013,
doi = {10.1007/978-3-642-39320-4_29},
timestamp = {Sun, 04 Jun 2017 10:10:26 +0200},
biburl = {https://dblp.org/rec/bib/conf/mkm/BarrasGHRTWW13},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{Faithfull:2018:COQ:3204179.3204223,
author = {Faithfull, Alexander and Bengtson, Jesper and Tassi, Enrico and Tankink, Carst},
title = {Coqoon},
journal = {Int. J. Softw. Tools Technol. Transf.},
issue_date = {April 2018},
volume = {20},
number = {2},
month = apr,
year = {2018},
issn = {1433-2779},
pages = {125--137},
numpages = {13},
url = {https://doi.org/10.1007/s10009-017-0457-2},
doi = {10.1007/s10009-017-0457-2},
acmid = {3204223},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
}

View File

@ -7,15 +7,16 @@ begin
open_monitor*[this::report]
(*>*)
title*[tit::title]\<open>An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\<close>
subtitle*[stit::subtitle]\<open>Version : Isabelle 2017\<close>
title*[tit::title]\<open>My Personal, Ecclectic Isabelle Programming Manual\<close>
subtitle*[stit::subtitle]\<open>Version : Isabelle 2019\<close>
text*[bu::author,
email = "''wolff@lri.fr''",
affiliation = "''Universit\\'e Paris-Saclay, Paris, France''"]\<open>Burkhart Wolff\<close>
affiliation = "\<open>Université Paris-Saclay, LRI, France\<close>"]\<open>Burkhart Wolff\<close>
text*[abs::abstract,
keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Tactic Programming'']"]\<open>
keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Programming Guide'',
''Tactic Programming'']"]\<open>
While Isabelle is mostly known as part of Isabelle/HOL (an interactive
theorem prover), it actually provides a system framework for developing a wide
spectrum of applications. A particular strength of the Isabelle framework is the
@ -126,9 +127,11 @@ figure*[fig2::figure, relative_width="100",src="''figures/text-element''"]
text\<open> text-commands, ML- commands (and in principle any other command) can be seen as
\<^emph>\<open>quotations\<close> over the underlying SML environment (similar to OCaml or Haskell).
Linking these different sorts of quotations with each other and the underlying SML-envirnment
is supported via \<^emph>\<open>antiquotations\<close>'s. Generally speaking, antiquotations are a programming technique
to specify expressions or patterns in a quotation, parsed in the context of the enclosing expression
or pattern where the quotation is.
is supported via \<^emph>\<open>antiquotations\<close>'s. Generally speaking, antiquotations are a programming
technique to specify expressions or patterns in a quotation, parsed in the context of the
enclosing expression or pattern where the quotation is. Another way to understand this concept:
anti-quotations are "semantic macros" that produce a value for the surrounding context
(ML, text, HOL, whatever) depending on local arguments and the underlying logical context.
The way an antiquotation is specified depends on the quotation expander: typically a specific
character and an identifier, or specific parentheses and a complete expression or pattern.\<close>
@ -305,8 +308,8 @@ ML\<open>
\<close>
subsection*[t213::example]\<open>Mechanism 2 : global arbitrary data structure that is attached to the global and
local Isabelle context $\theta$ \<close>
subsection*[t213::example]\<open>Mechanism 2 : global arbitrary data structure that is attached to
the global and local Isabelle context $\theta$ \<close>
ML \<open>
datatype X = mt
@ -1047,11 +1050,31 @@ function. Thus, the Isar-toplevel supports the generic document model
and allows for user-programmed extensions.
\<close>
text\<open>Isabelle \<^verbatim>\<open>.thy\<close>-files were processed by two types of parsers:
text\<open>In the traditional literature, Isabelle \<^verbatim>\<open>.thy\<close>-files were
were said to be processed by processed by two types of parsers:
\<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed
by a lexer-library and parser combinators built on top, and
\<^enum> the "inner-syntax" (i.e. the syntax for @{term \<open>\<Lambda>\<close>} - terms)
with an evolved, eight-layer parsing and pretty-printing process.
with an evolved, eight-layer parsing and pretty-printing process
based on an Early-algorithm.
\<close>
text\<open>This picture is less and less true for a number of reasons:
\<^enum> With the advent of \inlineisar+\<Open> ... \<Close>+, a mechanism for
\<^emph>\<open>cascade-syntax\<close> came to the Isabelle platform that introduce a flexible means
to change parsing contexts \<^emph>\<open>and\<close> parsing technologies.
\<^enum> Inside the term-parser levels, the concept of \<^emph>\<open>cartouche\<close> can be used
to escape the parser and its underlying parsing technology.
\<^enum> Outside, in the traditional toplevel-parsers, the
\inlineisar+\<Open> ... \<Close>+ is becoming more and more enforced
(some years ago, syntax like \<open>term{* ... *}\<close> was replaced by
syntax \<open>term(\<open>)... (\<close>)\<close>. This makes technical support of cascade syntax
more and more easy.
\<^enum> The Lexer infra-structure is already rather generic; nothing prevents to
add beside the lexer - configurations for ML-Parsers, Toplevel Command Syntax
parsers, mathematical notation parsers for $\lambda$-terms new pillars
of parsing technologies, say, for parsing C or Rust or JavaScript inside
Isabelle.
\<close>
@ -1115,7 +1138,8 @@ and properties; @{ML_structure Markup} provides a number of of such \<^emph>\<op
such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample
from \<^theory_text>\<open>Isabelle_DOF\<close>. A markup must be tagged with an id; this is done by the @{ML serial}-function
discussed earlier.\<close>
ML\<open>
subsection\<open>A simple Example\<close>
ML\<open>
local
val docclassN = "doc_class";
@ -1142,17 +1166,167 @@ in the Front-End, converts this into markup together with a unique number identi
markup, and sends this as a report to the Front-End. \<close>
section\<open>Environment Structured Reporting\<close>
subsection\<open>A Slightly more Complex Example\<close>
ML \<open>
fun markup_tvar def_name ps (name, id) =
let
fun markup_elem name = (name, (name, []): Markup.T);
val (tvarN, tvar) = markup_elem ((case def_name of SOME name => name | _ => "") ^ "'s nickname is");
val entity = Markup.entity tvarN name
val def = def_name = NONE
in
tvar ::
(if def then I else cons (Markup.keyword_properties Markup.ML_keyword3))
(map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps)
end
fun report [] _ _ = I
| report ps markup x =
let val ms = markup x
in fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps end
\<close>
ML \<open>
local
val data = \<comment> \<open>Derived from Yakoub's example ;-)\<close>
[ (\<open>Frédéric 1er\<close>, \<open>King of Naples\<close>)
, (\<open>Frédéric II\<close>, \<open>King of Sicily\<close>)
, (\<open>Frédéric III\<close>, \<open>the Handsome\<close>)
, (\<open>Frédéric IV\<close>, \<open>of the Empty Pockets\<close>)
, (\<open>Frédéric V\<close>, \<open>King of DenmarkNorway\<close>)
, (\<open>Frédéric VI\<close>, \<open>the Knight\<close>)
, (\<open>Frédéric VII\<close>, \<open>Count of Toggenburg\<close>)
, (\<open>Frédéric VIII\<close>, \<open>Count of Zollern\<close>)
, (\<open>Frédéric IX\<close>, \<open>the Old\<close>)
, (\<open>Frédéric X\<close>, \<open>the Younger\<close>) ]
val (tab0, markup) =
fold_map (fn (name, msg) => fn reports =>
let val id = serial ()
val pos = [Input.pos_of name]
in
( (fst(Input.source_content msg), (name, pos, id))
, report pos (markup_tvar NONE pos) (fst(Input.source_content name), id) reports)
end)
data
[]
val () = Position.reports_text markup
in
val tab = Symtab.make tab0
end
\<close>
ML \<open>
val _ =
fold (fn input =>
let
val pos1' = Input.pos_of input
fun ctnt name0 = fst(Input.source_content name0)
val pos1 = [pos1']
val msg1 = fst(Input.source_content input)
val msg2 = "No persons were found to have such nickname"
in
case Symtab.lookup tab (fst(Input.source_content input)) of
NONE => tap (fn _ => Output.information (msg2 ^ Position.here_list pos1))
(cons ((pos1', Markup.bad ()), ""))
| SOME (name0, pos0, id) => report pos1 (markup_tvar (SOME (ctnt name0)) pos0) (msg1, id)
end)
[ \<open>the Knight\<close> \<comment> \<open>Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\<close>
, \<open>the Handsome\<close> \<comment> \<open>Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\<close>
, \<open>the Spy\<close> \<comment> \<open>Example of a failure to retrieve the person in \<^ML>\<open>tab\<close>\<close>
]
[]
|> Position.reports_text
\<close>
text\<open>The pudding comes with the eating: \<close>
subsection\<open>Environment Structured Reporting\<close>
text\<open> The structure @{ML_structure \<open>Name_Space\<close>} offers an own infra-structure for names and
manages the markup accordingly. MORE TO COME\<close>
text\<open> @{ML_type "'a Name_Space.table"} \<close>
section\<open> Parsing issues \<close>
text\<open> Parsing combinators represent the ground building blocks of both generic input engines
as well as the specific Isar framework. They are implemented in the structure \verb+Token+
providing core type \verb+Token.T+.
section\<open> The System Lexer and Token Issues\<close>
text\<open>Four syntactic contexts are predefined in Isabelle (others can be added):
the ML context, the text context, the Isar-command context and the teerm-context, referring
to different needs of the Isabelle Framework as an extensible framework supporting incremental,
partially programmable extensions and as a Framework geared towards Formal Proofs and therefore
mathematical notations. The basic data-structure for the lexical treatment of these
\<close>
ML\<open> open Token\<close>
subsection\<open>Tokens\<close>
text\<open>The basic entity that lexers treat are \<^emph>\<open>tokens\<close>. defined in @{ML_structure "Token"}}
It provides a classification infrastructure, the references to positions and Markup
as well as way's to annotate tokens with (some) values they denote:
\<close>
ML\<open>
local
open Token
type dummy = Token.T
type src = Token.T list
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}
val _ = Token.is_command : Token.T -> bool;
val _ = Token.content_of : Token.T -> string; (* textueller kern eines Tokens. *)
val _ = pos_of: T -> Position.T
(*
datatype kind =
(*immediate source*)
Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
Float | Space |
(*delimited content*)
String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
(*special content*)
Error of string | EOF
datatype value =
Source of src |
Literal of bool * Markup.T |
Name of name_value * morphism |
Typ of typ |
Term of term |
Fact of string option * thm list |
Attribute of morphism -> attribute |
Declaration of declaration |
Files of file Exn.result list
*)
in val _ = ()
end
\<close>
subsection\<open>A Lexer Configuration Example\<close>
ML\<open>
\<close>
section\<open> Combinator Parsing \<close>
text\<open>Parsing Combinators go back to monadic programming as advocated by Wadler et. al, and has been
worked out @{cite "DBLP:journals/jfp/Hutton92"}\<close>
ML\<open> \<close>
ML\<open>
@ -1171,8 +1345,6 @@ val _ = parser2contextparser : 'a parser -> 'a context_parser;
(* bah, is the same as Scan.lift *)
val _ = Scan.lift Args.cartouche_input : Input.source context_parser;
Token.is_command;
Token.content_of; (* textueller kern eines Tokens. *)
\<close>

View File

@ -1,8 +1,9 @@
session "TR_mycommentedisabelle" = "Isabelle_DOF" +
session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
options [document = pdf, document_output = "output",quick_and_dirty = true]
theories
"MyCommentedIsabelle"
"TR_MyCommentedIsabelle"
document_files
"root.bib"
"isadof.cfg"
"preamble.tex"
"prooftree.sty"

File diff suppressed because it is too large Load Diff

View File

@ -0,0 +1,528 @@
@misc{bockenek:hal-02069705,
TITLE = {{Using Isabelle/UTP for the Verification of Sorting Algorithms A Case Study}},
AUTHOR = {Bockenek, Joshua A and Lammich, Peter and Nemouchi, Yakoub and Wolff, Burkhart},
URL = {https://easychair.org/publications/preprint/CxRV},
NOTE = {Isabelle Workshop 2018, Colocated with Interactive Theorem Proving. As part of FLOC 2018, Oxford, GB.},
YEAR = {2018},
MONTH = Jul
}
@book{DBLP:books/sp/NipkowPW02,
author = {Tobias Nipkow and
Lawrence C. Paulson and
Markus Wenzel},
title = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
series = {Lecture Notes in Computer Science},
volume = {2283},
publisher = {Springer},
year = {2002},
url = {https://doi.org/10.1007/3-540-45949-9},
deactivated_doi = {10.1007/3-540-45949-9},
isbn = {3-540-43376-7},
timestamp = {Tue, 14 May 2019 10:00:35 +0200},
biburl = {https://dblp.org/rec/bib/books/sp/NipkowPW02},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sosp/KleinEHACDEEKNSTW09,
author = {Gerwin Klein and
Kevin Elphinstone and
Gernot Heiser and
June Andronick and
David Cock and
Philip Derrin and
Dhammika Elkaduwe and
Kai Engelhardt and
Rafal Kolanski and
Michael Norrish and
Thomas Sewell and
Harvey Tuch and
Simon Winwood},
title = {seL4: formal verification of an {OS} kernel},
deactivated_booktitle = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles
2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009},
pages = {207--220},
year = {2009},
crossref = {DBLP:conf/sosp/2009},
url = {https://doi.org/10.1145/1629575.1629596},
deactivated_doi = {10.1145/1629575.1629596},
timestamp = {Tue, 06 Nov 2018 16:59:32 +0100},
biburl = {https://dblp.org/rec/bib/conf/sosp/KleinEHACDEEKNSTW09},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/sosp/2009,
editor = {Jeanna Neefe Matthews and
Thomas E. Anderson},
title = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles
2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009},
publisher = {{ACM}},
year = {2009},
url = {https://doi.org/10.1145/1629575},
deactivated_doi = {10.1145/1629575},
isbn = {978-1-60558-752-3},
timestamp = {Tue, 06 Nov 2018 16:59:32 +0100},
biburl = {https://dblp.org/rec/bib/conf/sosp/2009},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/CohenDHLMSST09,
author = {Ernie Cohen and
Markus Dahlweid and
Mark A. Hillebrand and
Dirk Leinenbach and
Michal Moskal and
Thomas Santen and
Wolfram Schulte and
Stephan Tobies},
title = {{VCC:} {A} Practical System for Verifying Concurrent {C}},
deactivated_booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
pages = {23--42},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03359-9_2},
deactivated_doi = {10.1007/978-3-642-03359-9_2},
timestamp = {Tue, 23 May 2017 01:12:08 +0200},
biburl = {https://dblp.org/rec/bib/conf/tphol/CohenDHLMSST09},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cacm/Leroy09,
author = {Xavier Leroy},
title = {Formal verification of a realistic compiler},
journal = {Commun. {ACM}},
volume = {52},
number = {7},
pages = {107--115},
year = {2009},
url = {http://doi.acm.org/10.1145/1538788.1538814},
deactivated_doi = {10.1145/1538788.1538814},
timestamp = {Thu, 02 Jul 2009 13:36:32 +0200},
biburl = {https://dblp.org/rec/bib/journals/cacm/Leroy09},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Wenzel14,
author = {Makarius Wenzel},
title = {Asynchronous User Interaction and Tool Integration in Isabelle/PIDE},
deactivated_booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 14-17, 2014. Proceedings},
pages = {515--530},
year = {2014},
crossref = {DBLP:conf/itp/2014},
url = {https://doi.org/10.1007/978-3-319-08970-6\_33},
deactivated_doi = {10.1007/978-3-319-08970-6\_33},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/Wenzel14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/itp/2014,
editor = {Gerwin Klein and
Ruben Gamboa},
title = {Interactive Theorem Proving - 5th International Conference, {ITP}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8558},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08970-6},
deactivated_doi = {10.1007/978-3-319-08970-6},
isbn = {978-3-319-08969-0},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/2014},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Wenzel14,
author = {Makarius Wenzel},
title = {System description: Isabelle/jEdit in 2014},
deactivated_booktitle = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers,
{UITP} 2014, Vienna, Austria, 17th July 2014.},
pages = {84--94},
year = {2014},
crossref = {DBLP:journals/corr/BenzmullerP14},
url = {https://doi.org/10.4204/EPTCS.167.10},
deactivated_doi = {10.4204/EPTCS.167.10},
timestamp = {Wed, 12 Sep 2018 01:05:15 +0200},
biburl = {https://dblp.org/rec/bib/journals/corr/Wenzel14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/BenzmullerP14,
editor = {Christoph Benzm{\"{u}}ller and
Bruno {Woltzenlogel Paleo}},
title = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers,
{UITP} 2014, Vienna, Austria, 17th July 2014},
series = {{EPTCS}},
volume = {167},
year = {2014},
url = {https://doi.org/10.4204/EPTCS.167},
deactivated_doi = {10.4204/EPTCS.167},
timestamp = {Wed, 12 Sep 2018 01:05:15 +0200},
biburl = {https://dblp.org/rec/bib/journals/corr/BenzmullerP14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/BarrasGHRTWW13,
author = {Bruno Barras and
Lourdes Del Carmen Gonz{\'{a}}lez{-}Huesca and
Hugo Herbelin and
Yann R{\'{e}}gis{-}Gianas and
Enrico Tassi and
Makarius Wenzel and
Burkhart Wolff},
title = {Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving
Systems},
deactivated_booktitle = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems
and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12,
2013. Proceedings},
pages = {359--363},
year = {2013},
crossref = {DBLP:conf/mkm/2013},
url = {https://doi.org/10.1007/978-3-642-39320-4\_29},
deactivated_doi = {10.1007/978-3-642-39320-4\_29},
timestamp = {Sun, 02 Jun 2019 21:17:34 +0200},
biburl = {https://dblp.org/rec/bib/conf/mkm/BarrasGHRTWW13},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/mkm/2013,
editor = {Jacques Carette and
David Aspinall and
Christoph Lange and
Petr Sojka and
Wolfgang Windsteiger},
title = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems
and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12,
2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7961},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39320-4},
deactivated_doi = {10.1007/978-3-642-39320-4},
isbn = {978-3-642-39319-8},
timestamp = {Sun, 02 Jun 2019 21:17:34 +0200},
biburl = {https://dblp.org/rec/bib/conf/mkm/2013},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/LammichW19,
author = {Peter Lammich and
Simon Wimmer},
title = {{IMP2} - Simple Program Verification in Isabelle/HOL},
journal = {Archive of Formal Proofs},
volume = {2019},
year = {2019},
url = {https://www.isa-afp.org/entries/IMP2.html},
timestamp = {Mon, 20 May 2019 11:45:07 +0200},
biburl = {https://dblp.org/rec/bib/journals/afp/LammichW19},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@misc{frama-c-home-page,
title = {The Frama-C Home Page},
author = {CEA LIST},
year = 2019,
month = jan,
day = 10,
url = {https://frama-c.com},
note = {Accessed \DTMdate{2019-03-24}}
}
@inproceedings{DBLP:conf/fm/LeinenbachS09,
author = {Dirk Leinenbach and Thomas Santen},
title = {Verifying the Microsoft Hyper-V Hypervisor with {VCC}},
deactivated_booktitle = {{FM} 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands,
November 2-6, 2009. Proceedings},
pages = {806--809},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-05089-3_51},
deactivated_doi = {10.1007/978-3-642-05089-3_51},
timestamp = {Mon, 22 May 2017 17:11:19 +0200},
biburl = {https://dblp.org/rec/bib/conf/fm/LeinenbachS09},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tap/Keller18,
author = {Chantal Keller},
title = {Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL},
deactivated_booktitle = {Tests and Proofs - 12th International Conference, {TAP} 2018, Held
as Part of {STAF} 2018, Toulouse, France, June 27-29, 2018, Proceedings},
pages = {103--119},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-92994-1\_6},
deactivated_doi = {10.1007/978-3-319-92994-1\_6},
timestamp = {Mon, 18 Jun 2018 13:57:50 +0200},
biburl = {https://dblp.org/rec/bib/conf/tap/Keller18},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/AissatVW16,
author = {Romain A{\"{\i}}ssat and
Fr{\'{e}}d{\'{e}}ric Voisin and
Burkhart Wolff},
title = {Infeasible Paths Elimination by Symbolic Execution Techniques - Proof
of Correctness and Preservation of Paths},
deactivated_booktitle = {Interactive Theorem Proving - 7th International Conference, {ITP}
2016, Nancy, France, August 22-25, 2016, Proceedings},
pages = {36--51},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-43144-4\_3},
deactivated_doi = {10.1007/978-3-319-43144-4\_3},
timestamp = {Thu, 17 Aug 2017 16:22:01 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/AissatVW16},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocs/KleinAEMSKH14,
author = {Gerwin Klein and
June Andronick and
Kevin Elphinstone and
Toby C. Murray and
Thomas Sewell and
Rafal Kolanski and
Gernot Heiser},
title = {Comprehensive formal verification of an {OS} microkernel},
journal = {{ACM} Trans. Comput. Syst.},
volume = {32},
number = {1},
pages = {2:1--2:70},
year = {2014},
url = {http://doi.acm.org/10.1145/2560537},
deactivated_doi = {10.1145/2560537},
timestamp = {Tue, 03 Jan 2017 11:51:57 +0100},
biburl = {https://dblp.org/rec/bib/journals/tocs/KleinAEMSKH14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/GreenawayLAK14,
author = {David Greenaway and
Japheth Lim and
June Andronick and
Gerwin Klein},
title = {Don't sweat the small stuff: formal verification of {C} code without
the pain},
deactivated_booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
{PLDI} '14, Edinburgh, United Kingdom - June 09 - 11, 2014},
pages = {429--439},
year = {2014},
url = {http://doi.acm.org/10.1145/2594291.2594296},
deactivated_doi = {10.1145/2594291.2594296},
timestamp = {Tue, 20 Dec 2016 10:12:01 +0100},
biburl = {https://dblp.org/rec/bib/conf/pldi/GreenawayLAK14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/BruckerACW18,
author = {Achim D. Brucker and
Idir A{\"{\i}}t{-}Sadoune and
Paolo Crisafulli and
Burkhart Wolff},
title = {Using the Isabelle Ontology Framework - Linking the Formal with the
Informal},
deactivated_booktitle = {Intelligent Computer Mathematics - 11th International Conference,
{CICM} 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings},
pages = {23--38},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-96812-4\_3},
deactivated_doi = {10.1007/978-3-319-96812-4\_3},
timestamp = {Sat, 11 Aug 2018 00:57:41 +0200},
biburl = {https://dblp.org/rec/bib/conf/mkm/BruckerACW18},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/TuongW15,
author = {Fr{\'{e}}d{\'{e}}ric Tuong and
Burkhart Wolff},
title = {A Meta-Model for the Isabelle {API}},
journal = {Archive of Formal Proofs},
volume = {2015},
year = {2015},
url = {https://www.isa-afp.org/entries/Isabelle\_Meta\_Model.shtml},
timestamp = {Mon, 07 Jan 2019 11:16:33 +0100},
biburl = {https://dblp.org/rec/bib/journals/afp/TuongW15},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/WinwoodKSACN09,
author = {Simon Winwood and
Gerwin Klein and
Thomas Sewell and
June Andronick and
David Cock and
Michael Norrish},
title = {Mind the Gap},
deactivated_booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
pages = {500--515},
year = {2009},
crossref = {DBLP:conf/tphol/2009},
url = {https://doi.org/10.1007/978-3-642-03359-9\_34},
deactivated_doi = {10.1007/978-3-642-03359-9\_34},
timestamp = {Fri, 02 Nov 2018 09:49:05 +0100},
biburl = {https://dblp.org/rec/bib/conf/tphol/WinwoodKSACN09},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tphol/2009,
editor = {Stefan Berghofer and
Tobias Nipkow and
Christian Urban and
Makarius Wenzel},
title = {Theorem Proving in Higher Order Logics, 22nd International Conference,
TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5674},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03359-9},
deactivated_doi = {10.1007/978-3-642-03359-9},
isbn = {978-3-642-03358-2},
timestamp = {Tue, 23 May 2017 01:12:08 +0200},
biburl = {https://dblp.org/rec/bib/conf/tphol/2009},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/BruckerTW14,
author = {Achim D. Brucker and
Fr{\'{e}}d{\'{e}}ric Tuong and
Burkhart Wolff},
title = {Featherweight {OCL:} {A} Proposal for a Machine-Checked Formal Semantics
for {OCL} 2.5},
journal = {Archive of Formal Proofs},
volume = {2014},
year = {2014},
url = {https://www.isa-afp.org/entries/Featherweight\_OCL.shtml},
timestamp = {Mon, 07 Jan 2019 11:16:33 +0100},
biburl = {https://dblp.org/rec/bib/journals/afp/BruckerTW14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/SananZHZTL17,
author = {David San{\'{a}}n and
Yongwang Zhao and
Zhe Hou and
Fuyuan Zhang and
Alwen Tiu and
Yang Liu},
title = {CSimpl: {A} Rely-Guarantee-Based Framework for Verifying Concurrent
Programs},
deactivated_booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 23rd International Conference, {TACAS} 2017, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}},
pages = {481--498},
year = {2017},
crossref = {DBLP:conf/tacas/2017-1},
url = {https://doi.org/10.1007/978-3-662-54577-5\_28},
deactivated_doi = {10.1007/978-3-662-54577-5\_28},
timestamp = {Mon, 18 Sep 2017 08:38:37 +0200},
biburl = {https://dblp.org/rec/bib/conf/tacas/SananZHZTL17},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tacas/2017-1,
editor = {Axel Legay and
Tiziana Margaria},
title = {Tools and Algorithms for the Construction and Analysis of Systems
- 23rd International Conference, {TACAS} 2017, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {10205},
year = {2017},
url = {https://doi.org/10.1007/978-3-662-54577-5},
deactivated_doi = {10.1007/978-3-662-54577-5},
isbn = {978-3-662-54576-8},
timestamp = {Wed, 24 May 2017 08:28:32 +0200},
biburl = {https://dblp.org/rec/bib/conf/tacas/2017-1},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/HouSTL17,
author = {Zhe Hou and
David San{\'{a}}n and
Alwen Tiu and
Yang Liu},
title = {Proof Tactics for Assertions in Separation Logic},
deactivated_booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}
2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
pages = {285--303},
year = {2017},
crossref = {DBLP:conf/itp/2017},
url = {https://doi.org/10.1007/978-3-319-66107-0\_19},
deactivated_doi = {10.1007/978-3-319-66107-0\_19},
timestamp = {Mon, 18 Sep 2017 08:38:37 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/HouSTL17},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/itp/2017,
editor = {Mauricio Ayala{-}Rinc{\'{o}}n and
C{\'{e}}sar A. Mu{\~{n}}oz},
title = {Interactive Theorem Proving - 8th International Conference, {ITP}
2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10499},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-66107-0},
deactivated_doi = {10.1007/978-3-319-66107-0},
isbn = {978-3-319-66106-3},
timestamp = {Wed, 06 Sep 2017 14:53:52 +0200},
biburl = {https://dblp.org/rec/bib/conf/itp/2017},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sigbed/CarrascosaCMBC14,
author = {E. Carrascosa and
Javier Coronel and
Miguel Masmano and
Patricia Balbastre and
Alfons Crespo},
title = {XtratuM hypervisor redesign for {LEON4} multicore processor},
journal = {{SIGBED} Review},
volume = {11},
number = {2},
pages = {27--31},
year = {2014},
url = {https://doi.org/10.1145/2668138.2668142},
deactivated_doi = {10.1145/2668138.2668142},
timestamp = {Tue, 06 Nov 2018 12:51:31 +0100},
biburl = {https://dblp.org/rec/bib/journals/sigbed/CarrascosaCMBC14},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cacm/Earley70,
author = {Jay Earley},
title = {An Efficient Context-Free Parsing Algorithm},
journal = {Commun. {ACM}},
volume = {13},
number = {2},
pages = {94--102},
year = {1970},
url = {https://doi.org/10.1145/362007.362035},
deactivated_doi = {10.1145/362007.362035},
timestamp = {Wed, 14 Nov 2018 10:22:30 +0100},
biburl = {https://dblp.org/rec/bib/journals/cacm/Earley70},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/Hutton92,
author = {Graham Hutton},
title = {Higher-Order Functions for Parsing},
journal = {J. Funct. Program.},
volume = {2},
number = {3},
pages = {323--343},
year = {1992},
url = {https://doi.org/10.1017/S0956796800000411},
deactivated_doi = {10.1017/S0956796800000411},
timestamp = {Sat, 27 May 2017 14:24:34 +0200},
biburl = {https://dblp.org/rec/bib/journals/jfp/Hutton92},
bibsource = {dblp computer science bibliography, https://dblp.org}
}