Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
1d44dae01207
Commit
c58a4078
authored
Mar 15, 2012
by
nipkow
Browse files
The
parent
f49b4c83349c
Changes
12
Hide whitespace changes
Inline
Side-by-side
thys/Dijkstra_Shortest_Path/document/root.bib
View file @
1d44dae0
...
...
@@ -64,7 +64,7 @@
@incollection
{
L09_collections
,
author
=
{Peter Lammich}
,
title
=
{Collections Framework}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sf.net/entries/collections.shtml}}
,
month
=
Dec
,
...
...
@@ -76,7 +76,7 @@
@incollection
{
L09_tree_automata
,
author
=
{Peter Lammich}
,
title
=
{Tree Automata}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sf.net/entries/Tree-Automata.shtml}}
,
month
=
Dec
,
...
...
@@ -88,7 +88,7 @@
@incollection
{
NKP10
,
author
=
{Benedikt Nordhoff and Stefan K{\"o}rner and Peter Lammich}
,
title
=
{Finger Trees}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sf.net/entries/Tree-Automata.shtml}}
,
month
=
Oct
,
...
...
thys/Example-Submission/Submission.thy
View file @
1d44dae0
(* Title: An example submission to the Archive of Formal Proof
(* Title: An example submission to the Archive of Formal Proof
s
Author: Gerwin Klein <kleing at cse.unsw.edu.au>, 2004
Maintainer: Gerwin Klein <kleing at cse.unsw.edu.au>
*)
...
...
@@ -10,7 +10,7 @@ theory Submission
begin
text {*
This is an example submission to the Archive of Formal Proof.
This is an example submission to the Archive of Formal Proof
s
.
The scope of the archive encompasses examples, textbook-style
proofs, libraries and larger scientific developments.
...
...
thys/Example-Submission/document/root.tex
View file @
1d44dae0
\documentclass
[11pt,a4paper]
{
article
}
\usepackage
{
isabelle,isabellesym
}
...
...
@@ -38,7 +36,7 @@
\maketitle
\begin{abstract}
This is an example submission to the Archive of Formal Proof. It
This is an example submission to the Archive of Formal Proof
s
. It
shows submission requirements and explains the structure of a simple
typical submission.
\end{abstract}
...
...
thys/GraphMarkingIBP/document/root.bib
View file @
1d44dae0
...
...
@@ -208,7 +208,7 @@ institution="{TUCS}"
@incollection
{
preoteasa:back:afp:2010
,
author
=
{Viorel Preoteasa and Ralph-Johan Back}
,
title
=
{Semantics and Data Refinement of Invariant Based Programs}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sf.net/entries/DataRefinementIBP.shtml}}
,
month
=
May
,
...
...
thys/HRB-Slicing/document/root.tex
View file @
1d44dae0
...
...
@@ -77,7 +77,7 @@ Thomas Reps and Susan Horwitz and Mooly Sagiv and Genevieve Rosay.
\bibitem
{
Wasserrab:08
}
\newblock
Daniel Wasserrab.
\newblock
Towards certified slicing.
\newblock
In G. Klein, T. Nipkow, and L. Paulson, editors,
{
\em
The
Archive of Formal
\newblock
In G. Klein, T. Nipkow, and L. Paulson, editors,
{
\em
Archive of Formal
Proofs
}
.
\newblock
\url
{
http://afp.sf.net/entries/Slicing.shtml
}
, September 2008.
\newblock
Formal proof development.
...
...
thys/InformationFlowSlicing/document/root.bib
View file @
1d44dae0
@INCOLLECTION
{
Wasserrab:08
,
author
=
{Daniel Wasserrab}
,
title
=
{Towards Certified Slicing}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
publisher
=
{\url{http://afp.sf.net/entries/Slicing.shtml}}
,
year
=
{2008}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
...
...
@@ -13,7 +13,7 @@
@INCOLLECTION
{
Wasserrab:09
,
author
=
{Daniel Wasserrab}
,
title
=
{Backing up Slicing: Verifying the Interprocedural Two-Phase {H}orwitz-{R}eps-{B}inkley Slicer}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
publisher
=
{\url{http://afp.sf.net/entries/HRB-Slicing.shtml}}
,
year
=
{2009}
,
OPTeditor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
...
...
@@ -70,7 +70,7 @@
@INCOLLECTION
{
BeringerH:08
,
author
=
{Lennart Beringer and Martin Hofmann}
,
title
=
{Secure information flow and program logics}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
publisher
=
{\url{http://afp.sf.net/entries/SIFPL.shtml}}
,
year
=
{2008}
,
OPTeditor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
...
...
@@ -82,7 +82,7 @@
@INCOLLECTION
{
SneltingW:08
,
author
=
{Gregor Snelting and Daniel Wasserrab}
,
title
=
{A Correctness Proof for the {Volpano/Smith} Security Typing System}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
publisher
=
{\url{http://afp.sf.net/entries/VolpanoSmith.shtml}}
,
year
=
{2008}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
...
...
thys/MonoBoolTranAlgebra/document/root.bib
View file @
1d44dae0
...
...
@@ -257,7 +257,7 @@ results are formalized and mechanically proved in the Isabelle/HOL theorem prove
@incollection
{
preoteasa:back:2010a
,
author
=
{Preoteasa, Viorel and Back, Ralph-Johan}
,
title
=
{Semantics and Data Refinement of Invariant Based Programs }
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{http://afp.sourceforge.net/entries/DataRefinementIBP.shtml}
,
month
=
May
,
...
...
@@ -269,7 +269,7 @@ results are formalized and mechanically proved in the Isabelle/HOL theorem prove
@incollection
{
preoteasa:back:2010b
,
author
=
{Preoteasa, Viorel and Back, Ralph-Johan}
,
title
=
{Verification of the {D}eutsch-{S}chorr-{W}aite Graph Marking Algorithm using Data Refinement}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{http://afp.sourceforge.net/entries/GraphMarkingIBP.shtml}
,
month
=
May
,
...
...
thys/Refine_Monadic/document/root.bib
View file @
1d44dae0
...
...
@@ -76,7 +76,7 @@
@incollection
{
L09_collections
,
author
=
{Peter Lammich}
,
title
=
{Collections Framework}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sf.net/entries/collections.shtml}}
,
month
=
Dec
,
...
...
@@ -88,7 +88,7 @@
@incollection
{
L09_tree_automata
,
author
=
{Peter Lammich}
,
title
=
{Tree Automata}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sf.net/entries/Tree-Automata.shtml}}
,
month
=
Dec
,
...
...
thys/SIFPL/document/root.bib
View file @
1d44dae0
...
...
@@ -69,7 +69,7 @@
@incollection
{
Nipkow-AFP-AHL
,
author
=
{Tobias Nipkow}
,
title
=
{Abstract {H}oare Logics}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sourceforge.net/entries/Abstract-Hoare-Logics.shtml}}
,
month
=
Jun
,
...
...
thys/SenSocialChoice/document/root.bib
View file @
1d44dae0
...
...
@@ -72,7 +72,7 @@
@incollection
{
Nipkow:2008
,
author
=
{Tobias Nipkow}
,
title
=
{{Arrow and Gibbard-Satterthwaite}}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sourceforge.net/devel-entries/ArrowImpossibilityGS.shtml}}
,
month
=
Sep
,
...
...
thys/Transitive-Closure-II/document/root.bib
View file @
1d44dae0
@incollection
{
rtrancl_fin
,
author
=
{C.~Sternagel and R.~Thiemann}
,
title
=
{{Executable} {Transitive} {Closures} of {Finite} {Relations}}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
publisher
=
{\url{http://afp.sf.net/entries/Transitive-Closure.shtml}}
,
month
=
mar
,
year
=
2011
,
...
...
thys/Tree-Automata/document/root.bib
View file @
1d44dae0
...
...
@@ -11,7 +11,7 @@
@incollection
{
L09_collections
,
author
=
{Peter Lammich}
,
title
=
{Isabelle Collection Library}
,
booktitle
=
{
The
Archive of Formal Proofs}
,
booktitle
=
{Archive of Formal Proofs}
,
editor
=
{Gerwin Klein and Tobias Nipkow and Lawrence Paulson}
,
publisher
=
{\url{http://afp.sf.net/entries/collections.shtml}}
,
month
=
Dez
,
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment