forked from Isabelle_DOF/Isabelle_DOF
Modifications / evolutions for the second TR example.
Arrived at page 34.
This commit is contained in:
parent
9c21b7a89a
commit
f2bb4f6e31
|
@ -8,15 +8,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
|
||||
|
@ -127,9 +128,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>
|
||||
|
@ -306,8 +309,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
|
||||
|
@ -1048,11 +1051,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>
|
||||
|
||||
|
||||
|
@ -1116,7 +1139,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";
|
||||
|
@ -1143,17 +1167,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 Denmark–Norway\<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>
|
||||
|
||||
|
@ -1172,8 +1346,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>
|
||||
|
||||
|
|
|
@ -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
|
@ -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}
|
||||
}
|
Reference in New Issue