Commit 67799050 authored by kleing's avatar kleing
Browse files

afp.sf.net links -> isa-afp.org

parent 18ab0d760c57
......@@ -18,7 +18,7 @@
@article{Bourke14,
author = {Bourke, T.},
journal = {Archive of Formal Proofs},
note = {\url{http://afp.sf.net/entries/AWN.shtml}},
note = {\url{http://isa-afp.org/entries/AWN.shtml}},
title = {Mechanization of the {Algebra for Wireless Networks} {(AWN)}},
year = 2014
}
......
......@@ -59,7 +59,7 @@
journal = {Archive of Formal Proofs},
month = apr,
year = 2013,
note = {\url{http://afp.sf.net/entries/Containers.shtml},
note = {\url{http://isa-afp.org/entries/Containers.shtml},
Formal proof development},
ISSN = {2150-914x},
}
......@@ -70,7 +70,7 @@
journal = {Archive of Formal Proofs},
month = sep,
year = 2014,
note = {\url{http://afp.sf.net/entries/Gauss_Jordan.shtml},
note = {\url{http://isa-afp.org/entries/Gauss_Jordan.shtml},
Formal proof development},
ISSN = {2150-914x},
}
......@@ -81,7 +81,7 @@
journal = {Archive of Formal Proofs},
month = jun,
year = 2010,
note = {\url{http://afp.sf.net/entries/Matrix.shtml},
note = {\url{http://isa-afp.org/entries/Matrix.shtml},
Formal proof development},
ISSN = {2150-914x},
}
......@@ -120,7 +120,7 @@
journal = {Archive of Formal Proofs},
volume = {2015},
year = {2015},
url = {http://afp.sourceforge.net/entries/Jordan_Normal_Form.shtml},
url = {http://isa-afp.org/entries/Jordan_Normal_Form.shtml},
timestamp = {Fri, 02 Oct 2015 13:06:45 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/afp/ThiemannY15},
bibsource = {dblp computer science bibliography, http://dblp.org}
......@@ -132,7 +132,7 @@
journal = {Archive of Formal Proofs},
volume = {2014},
year = {2014},
url = {http://afp.sourceforge.net/entries/Real_Impl.shtml},
url = {http://isa-afp.org/entries/Real_Impl.shtml},
timestamp = {Mon, 24 Mar 2014 12:06:18 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/afp/Thiemann14},
bibsource = {dblp computer science bibliography, http://dblp.org}
......
......@@ -155,7 +155,7 @@ author = "Samson Abramsky and Chih-Hao Luke Ong"
journal = {Archive of Formal Proofs},
month = jan,
year = 2013,
note = {\url{http://afp.sf.net/entries/Launchbury.shtml},
note = {\url{http://isa-afp.org/entries/Launchbury.shtml},
Formal proof development},
ISSN = {2150-914x},
}
......
......@@ -19,7 +19,7 @@
journal = {Archive of Formal Proofs},
month = apr,
year = 2014,
note = {\url{http://afp.sf.net/entries/Discrete_Summation.shtml},
note = {\url{http://isa-afp.org/entries/Discrete_Summation.shtml},
Formal proof development},
ISSN = {2150-914x},
}
......@@ -43,7 +43,7 @@
These theories are part of a joint work with Alwen Tiu and Leonor
P. Nieto \cite{bars_leon_tiu}. In this work the correctness of
Schneider schema was also verified using Isabelle (available at
\url{http://afp.sourceforge.net/entries/GenClock.shtml}).
\url{http://isa-afp.org/entries/GenClock.shtml}).
\end{abstract}
......
......@@ -21,7 +21,7 @@ begin
Isabelle/HOLs code generator to generate ML-code.
The implementation uses the Isabelle Collection Framework (ICF)
(Available at @{url "http://afp.sourceforge.net/entries/Collections.shtml"}),
(Available at @{url "http://isa-afp.org/entries/Collections.shtml"}),
to provide efficient set implementations. We choose a hashset
(backed by a Red Black Tree) for the visited set, and lists for
all other sets. Moreover, we fix the node type to natural numbers.
......
......@@ -404,7 +404,7 @@ text_raw {*\label{sec:userguide.design}*}
For a more detailed discussion of the data refinement issue, we refer to
the monadic refinement framework, that is available in the AFP
(@{url "http://afp.sourceforge.net/entries/Refine_Monadic.shtml"})
(@{url "http://isa-afp.org/entries/Refine_Monadic.shtml"})
*}
subsection {* Operation Records *}
......
......@@ -304,7 +304,7 @@ year = {201x}
journal = {Archive of Formal Proofs},
month = nov,
year = 2011,
note = {\url{http://afp.sf.net/entries/TLA},
note = {\url{http://isa-afp.org/entries/TLA},
Formal proof development},
ISSN = {2150-914x},
}
......@@ -561,7 +561,7 @@ year = {201x}
journal = {Archive of Formal Proofs},
month = apr,
year = 2015,
note = {\url{http://afp.sf.net/entries/ConcurrentIMP.shtml},
note = {\url{http://isa-afp.org/entries/ConcurrentIMP.shtml},
Formal proof development},
ISSN = {2150-914x},
}
\ No newline at end of file
......@@ -304,7 +304,7 @@ year = {201x}
journal = {Archive of Formal Proofs},
month = nov,
year = 2011,
note = {\url{http://afp.sf.net/entries/TLA},
note = {\url{http://isa-afp.org/entries/TLA},
Formal proof development},
ISSN = {2150-914x},
}
......
......@@ -22,7 +22,7 @@
@article{DBLP:journals/afp/DebratM12,
Author = {Henri Debrat and Stephan Merz},
Bibsource = {DBLP, http://dblp.uni-trier.de},
Url = {http://afp.sourceforge.net/entries/Heard_Of.shtml},
Url = {http://isa-afp.org/entries/Heard_Of.shtml},
Journal = {Archive of Formal Proofs},
Keywords = {distributed computing, fault tolerance, byzantine failures, formal verification; heard-of model},
Title = {Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model},
......
......@@ -14,7 +14,7 @@
title = {Collections Framework},
journal = {Archive of Formal Proofs},
year = 2009,
note = {\url{http://afp.sf.net/entries/Collections.shtml}, Formal proof development},
note = {\url{http://isa-afp.org/entries/Collections.shtml}, Formal proof development},
}
@inproceedings{Lochbihler2013ITP,
......@@ -40,7 +40,7 @@
title = {Generating linear orders for datatypes},
journal = {Archive of Formal Proofs},
year = 2012,
note = {\url{http://afp.sf.net/entries/Datatype_Order_Generator.shtml}, Formal proof development},
note = {\url{http://isa-afp.org/entries/Datatype_Order_Generator.shtml}, Formal proof development},
}
@misc{HaftmannBulwahn2013codetut,
......
......@@ -66,7 +66,7 @@
title = {Collections Framework},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/collections.shtml}},
publisher = {\url{http://isa-afp.org/entries/collections.shtml}},
month = Dec,
year = 2009,
note = {Formal proof development},
......@@ -78,7 +78,7 @@
title = {Tree Automata},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/Tree-Automata.shtml}},
publisher = {\url{http://isa-afp.org/entries/Tree-Automata.shtml}},
month = Dec,
year = {2009},
note = {Formal proof development},
......@@ -90,7 +90,7 @@
title = {Finger Trees},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/Tree-Automata.shtml}},
publisher = {\url{http://isa-afp.org/entries/Tree-Automata.shtml}},
month = Oct,
year = {2010},
note = {Formal proof development},
......
......@@ -22,7 +22,7 @@ text {*
Submission should be via the web page @{url "https://ci.isabelle.systems/afp-submission/"}.
The tar file submission of the example you are reading is at
@{url "http://afp.sf.net/release/afp-Example-Submission-current.tar.gz"}.
@{url "http://isa-afp.org/release/afp-Example-Submission-current.tar.gz"}.
*}
section "Proof styles"
......
......@@ -82,7 +82,7 @@ done in our ``design model''
(see \autoref{ex:employee-design:uml}).
\endisatagafp
\isatagannexa
(see \url{http://afp.sourceforge.net/entries/Featherweight_OCL.shtml}).
(see \url{http://isa-afp.org/entries/Featherweight_OCL.shtml}).
\endisatagannexa
To be precise, this theory contains the formalization of the data-part
covered by the UML class model (see \autoref{fig:person-ana}):*}
......
......@@ -93,7 +93,7 @@ formal semantics of the core of OCL, called \FOCL\footnote{An updated,
machine-checked version and formally complete version of the
complete formalization is maintained by the Isabelle Archive of
Formal Proofs (AFP), see
\url{http://afp.sourceforge.net/entries/Featherweight_OCL.shtml}}. \FOCL
\url{http://isa-afp.org/entries/Featherweight_OCL.shtml}}. \FOCL
has a formal semantics in Isabelle/\HOL~\cite{nipkow.ea:isabelle:2002}.
\endisatagannexa
......
......@@ -22,8 +22,8 @@ For running the formalization you need
If you'd like to build the example interpretation with a While language you additionally need
- the [archive of formal proofs (AFP)](http://afp.sf.net/) installed as an Isabelle component.
See [http://afp.sf.net/using.shtml](http://afp.sf.net/using.shtml) for details on how to do that.
- the [archive of formal proofs (AFP)](http://isa-afp.org/) installed as an Isabelle component.
See [http://isa-afp.org/using.shtml](http://isa-afp.org/using.shtml) for details on how to do that.
For building the CompCertSSA compiler using our SSA construction algorithm
......
......@@ -23,7 +23,7 @@
journal = {Archive of Formal Proofs},
month = sep,
year = 2013,
note = {\url{http://afp.sf.net/entries/Native_Word.shtml},
note = {\url{http://isa-afp.org/entries/Native_Word.shtml},
Formal proof development},
ISSN = {2150-914x},
}
......@@ -270,7 +270,7 @@
title = {Formalizing the Logic-Automaton Connection },
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sourceforge.net/entries/Presburger-Automata.shtml}}
publisher = {\url{http://isa-afp.org/entries/Presburger-Automata.shtml}}
,
month = dec,
year = 2009,
......@@ -283,7 +283,7 @@
title = {Formalizing the Logic-Automaton Connection },
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sourceforge.net/entries/Presburger-Automata.shtml}}
publisher = {\url{http://isa-afp.org/entries/Presburger-Automata.shtml}}
,
month = dec,
year = 2009,
......@@ -1252,7 +1252,7 @@ pages={463-478}
title = {Binary Search Trees},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/BinarySearchTree.shtml}},
publisher = {\url{http://isa-afp.org/entries/BinarySearchTree.shtml}},
month = apr,
year = 2004,
note = {Formal proof development},
......@@ -1264,7 +1264,7 @@ pages={463-478}
title = {Binary Search Trees},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/BinarySearchTree.shtml}},
publisher = {\url{http://isa-afp.org/entries/BinarySearchTree.shtml}},
month = apr,
year = 2004,
note = {Formal proof development},
......@@ -1275,7 +1275,7 @@ pages={463-478}
author = {Peter Lammich},
title = {Collections Framework},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/Collections.shtml}},
publisher = {\url{http://isa-afp.org/entries/Collections.shtml}},
month = dec,
year = 2009,
note = {Formal proof development},
......@@ -1286,7 +1286,7 @@ pages={463-478}
author = {Peter Lammich},
title = {Collections Framework},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/Collections.shtml}},
publisher = {\url{http://isa-afp.org/entries/Collections.shtml}},
month = dec,
year = 2009,
note = {Formal proof development},
......@@ -1297,7 +1297,7 @@ pages={463-478}
author = {Peter Lammich},
title = {Tree Automata},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/Tree-Automata.shtml}},
publisher = {\url{http://isa-afp.org/entries/Tree-Automata.shtml}},
month = dec,
year = {2009},
note = {Formal proof development},
......@@ -1308,7 +1308,7 @@ pages={463-478}
author = {Peter Lammich},
title = {Tree Automata},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/Tree-Automata.shtml}},
publisher = {\url{http://isa-afp.org/entries/Tree-Automata.shtml}},
month = dec,
year = {2009},
note = {Formal proof development},
......@@ -1319,7 +1319,7 @@ pages={463-478}
author = {Peter Lammich},
title = {Refinement for Monadic Programs},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/Refine\_Monadic.shtml}},
publisher = {\url{http://isa-afp.org/entries/Refine\_Monadic.shtml}},
year = {2012},
note = {Formal proof development}
}
......@@ -1328,7 +1328,7 @@ pages={463-478}
author = {Peter Lammich},
title = {Refinement for Monadic Programs},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/Refine\_Monadic.shtml}},
publisher = {\url{http://isa-afp.org/entries/Refine\_Monadic.shtml}},
year = {2012},
note = {Formal proof development}
}
......@@ -1623,7 +1623,7 @@ pages={463-478}
title = {{AVL} Trees},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/AVL-Trees.shtml}},
publisher = {\url{http://isa-afp.org/entries/AVL-Trees.shtml}},
month = mar,
year = 2004,
note = {Formal proof development},
......@@ -1635,7 +1635,7 @@ pages={463-478}
title = {{AVL} Trees},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/AVL-Trees.shtml}},
publisher = {\url{http://isa-afp.org/entries/AVL-Trees.shtml}},
month = mar,
year = 2004,
note = {Formal proof development},
......@@ -1646,7 +1646,7 @@ pages={463-478}
author = {Benedikt Nordhoff and Peter Lammich},
title = {Formalization of {D}ijkstra's Algorithm},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/DiskPaxos.shtml}},
publisher = {\url{http://isa-afp.org/entries/DiskPaxos.shtml}},
year = {2012},
note = {Formal proof development}
}
......@@ -1655,7 +1655,7 @@ pages={463-478}
author = {Benedikt Nordhoff and Peter Lammich},
title = {Formalization of {D}ijkstra's Algorithm},
booktitle = {Archive of Formal Proofs},
publisher = {\url{http://afp.sf.net/entries/DiskPaxos.shtml}},
publisher = {\url{http://isa-afp.org/entries/DiskPaxos.shtml}},
year = {2012},
note = {Formal proof development}
}
......
......@@ -210,7 +210,7 @@ institution="{TUCS}"
title = {Semantics and Data Refinement of Invariant Based Programs},
booktitle = {Archive of Formal Proofs},
editor = {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
publisher = {\url{http://afp.sf.net/entries/DataRefinementIBP.shtml}},
publisher = {\url{http://isa-afp.org/entries/DataRefinementIBP.shtml}},
month = May,
year = 2010,
note = {Formal proof development. Submitted},
......
......@@ -66,7 +66,7 @@ Thomas Reps and Susan Horwitz and Mooly Sagiv and Genevieve Rosay.
\newblock Towards certified slicing.
\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 \url{http://isa-afp.org/entries/Slicing.shtml}, September 2008.
\newblock Formal proof development.
\end{thebibliography}
......
......@@ -94,7 +94,7 @@
title = {Proving the Correctness of {DiskPaxos}},
journal = {Archive of Formal Proofs},
year = {2005},
url = {http://afp.sourceforge.net/entries/DiskPaxos.shtml},
url = {http://isa-afp.org/entries/DiskPaxos.shtml},
}
@Article{lamport:part-time,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment