diff --git a/admin/site/themes/afp/layouts/_default/index.json b/admin/site/themes/afp/layouts/_default/index.json
--- a/admin/site/themes/afp/layouts/_default/index.json
+++ b/admin/site/themes/afp/layouts/_default/index.json
@@ -1,26 +1,26 @@
{{ with $.Scratch.Get "index" }}
- {{- jsonify . -}}
+ {{- jsonify (dict "indent" " ") . -}}
{{ else }}
{{- $.Scratch.Add "index" slice -}}
{{- range $index, $element := where .Site.RegularPages "Type" "eq" "entries" -}}
{{- $authors := slice -}}
{{- $data := .Site.Data -}}
{{- range $element.Params.authors -}}
{{- $authors = $authors | append (index (index $data.authors .) "name") -}}
{{- end -}}
{{- $.Scratch.Add "index" (dict
"id" $index
"title" $element.Title
"abstract" (replaceRE "\n" " " $element.Params.abstract)
"topics" $element.Params.topics
"topic_links" (apply $element.Params.topics "urlize" ".")
"permalink" $element.Permalink
"date" (.Date.Format "2006-01-02")
"authors" $authors
"used_by" (len (index .Site.Taxonomies.dependencies (urlize $element.File.BaseFileName)))
"shortname" $element.File.BaseFileName
"link" $element.RelPermalink)
-}}
{{- end -}}
- {{- $.Scratch.Get "index" | jsonify -}}
+ {{- $.Scratch.Get "index" | jsonify (dict "indent" " ") -}}
{{ end }}
\ No newline at end of file
diff --git a/etc/build.props b/etc/build.props
--- a/etc/build.props
+++ b/etc/build.props
@@ -1,25 +1,26 @@
title = AFP/Tools
module = $AFP_BASE/tools/lib/classes/afp_tools.jar
requirements = \
env:ISABELLE_SCALA_JAR \
$ISABELLE_HOME_USER/contrib/ci-extras-1/lib/ci-extras.jar
sources = \
tools/admin/afp_build_hugo.scala \
tools/migration/afp_migrate_metadata.scala \
tools/afp_build.scala \
+ tools/afp_check_metadata.scala \
tools/afp_check_roots.scala \
tools/afp_dependencies.scala \
tools/afp_site_gen.scala \
tools/afp_structure.scala \
tools/afp_tool.scala \
tools/hugo.scala \
tools/metadata.scala \
tools/rake.scala \
tools/toml.scala \
tools/utils.scala
resources = \
tools/SmartStoplist.txt:SmartStoplist.txt \
tools/migration/public_suffix_list.dat:public_suffix_list.dat
services = \
afp.Tools \
afp.Build_Tools
diff --git a/metadata/authors.toml b/metadata/authors.toml
--- a/metadata/authors.toml
+++ b/metadata/authors.toml
@@ -1,3495 +1,3502 @@
[lange]
name = "Christoph Lange"
[lange.emails]
lange_email = "math.semantic.web@gmail.com"
[lange.homepages]
[petrovic]
name = "Danijela Petrovic"
[petrovic.emails]
[petrovic.homepages]
petrovic_homepage = "http://www.matf.bg.ac.rs/~danijela"
[schimpf]
name = "Alexander Schimpf"
[schimpf.emails]
schimpf_email = "schimpfa@informatik.uni-freiburg.de"
[schimpf.homepages]
[murao]
name = "H. Murao"
[murao.emails]
[murao.homepages]
[bourke]
name = "Timothy Bourke"
[bourke.emails]
bourke_email = "tim@tbrk.org"
[bourke.homepages]
bourke_homepage = "http://www.tbrk.org"
[schaeffeler]
name = "Maximilian Schäffeler"
[schaeffeler.emails]
schaeffeler_email = "schaeffm@in.tum.de"
[schaeffeler.homepages]
[liut]
name = "Tao Liu"
[liut.emails]
[liut.homepages]
[sickert]
name = "Salomon Sickert"
[sickert.emails]
sickert_email = "s.sickert@tum.de"
[sickert.homepages]
sickert_homepage = "https://www7.in.tum.de/~sickert"
[lutz]
name = "Bianca Lutz"
[lutz.emails]
lutz_email = "sowilo@cs.tu-berlin.de"
[lutz.homepages]
[rizkallah]
name = "Christine Rizkallah"
[rizkallah.emails]
[rizkallah.homepages]
rizkallah_homepage = "https://www.mpi-inf.mpg.de/~crizkall/"
[pollak]
name = "Florian Pollak"
[pollak.emails]
pollak_email = "florian.pollak@gmail.com"
[pollak.homepages]
[sulejmani]
name = "Ujkan Sulejmani"
[sulejmani.emails]
[sulejmani.homepages]
[biendarra]
name = "Julian Biendarra"
[biendarra.emails]
[biendarra.homepages]
[saile]
name = "Christian Saile"
[saile.emails]
[saile.homepages]
saile_homepage = "http://dss.in.tum.de/staff/christian-saile.html"
[friedrich]
name = "Stefan Friedrich"
[friedrich.emails]
[friedrich.homepages]
[maximova]
name = "Alexandra Maximova"
[maximova.emails]
maximova_email = "amaximov@student.ethz.ch"
[maximova.homepages]
[stricker]
name = "Christian Stricker"
[stricker.emails]
[stricker.homepages]
stricker_homepage = "http://dss.in.tum.de/staff/christian-stricker.html"
[dyckhoff]
name = "Roy Dyckhoff"
[dyckhoff.emails]
[dyckhoff.homepages]
dyckhoff_homepage = "https://rd.host.cs.st-andrews.ac.uk"
[weidner]
name = "Arno Wilhelm-Weidner"
[weidner.emails]
weidner_email = "arno.wilhelm-weidner@tu-berlin.de"
[weidner.homepages]
[thomson]
name = "Fox Thomson"
[thomson.emails]
thomson_email = "foxthomson0@gmail.com"
[thomson.homepages]
[he]
name = "Yijun He"
[he.emails]
he_email = "yh403@cam.ac.uk"
[he.homepages]
[kammueller]
name = "Florian Kammüller"
[kammueller.emails]
kammueller_email = "flokam@cs.tu-berlin.de"
kammueller_email1 = "florian.kammuller@gmail.com"
[kammueller.homepages]
kammueller_homepage = "http://www.cs.mdx.ac.uk/people/florian-kammueller/"
[oostrom]
name = "Vincent van Oostrom"
[oostrom.emails]
[oostrom.homepages]
[klein]
name = "Gerwin Klein"
[klein.emails]
klein_email = "kleing@unsw.edu.au"
[klein.homepages]
klein_homepage = "http://www.cse.unsw.edu.au/~kleing/"
[simic]
name = "Danijela Simić"
[simic.emails]
simic_email = "danijela@matf.bg.ac.rs"
[simic.homepages]
simic_homepage = "http://poincare.matf.bg.ac.rs/~danijela"
[gao]
name = "Xin Gao"
[gao.emails]
[gao.homepages]
[guttmann]
name = "Walter Guttmann"
[guttmann.emails]
guttmann_email = "walter.guttmann@canterbury.ac.nz"
[guttmann.homepages]
guttmann_homepage = "https://www.cosc.canterbury.ac.nz/walter.guttmann/"
[mantel]
name = "Heiko Mantel"
[mantel.emails]
mantel_email = "mantel@mais.informatik.tu-darmstadt.de"
[mantel.homepages]
[schlichtkrull]
name = "Anders Schlichtkrull"
[schlichtkrull.emails]
schlichtkrull_email = "andschl@dtu.dk"
[schlichtkrull.homepages]
schlichtkrull_homepage = "https://people.compute.dtu.dk/andschl/"
[jaskolka]
name = "Jason Jaskolka"
[jaskolka.emails]
jaskolka_email = "jason.jaskolka@carleton.ca"
[jaskolka.homepages]
jaskolka_homepage = "https://carleton.ca/jaskolka/"
[rau]
name = "Martin Rau"
[rau.emails]
rau_email = "martin.rau@tum.de"
rau_email1 = "mrtnrau@googlemail.com"
[rau.homepages]
[bottesch]
name = "Ralph Bottesch"
[bottesch.emails]
bottesch_email = "ralph.bottesch@uibk.ac.at"
[bottesch.homepages]
bottesch_homepage = "http://cl-informatik.uibk.ac.at/users/bottesch/"
[bella]
name = "Giampaolo Bella"
[bella.emails]
bella_email = "giamp@dmi.unict.it"
[bella.homepages]
bella_homepage = "http://www.dmi.unict.it/~giamp/"
[dirix]
name = "Stefan Dirix"
[dirix.emails]
[dirix.homepages]
[nielsen]
name = "Finn Nielsen"
[nielsen.emails]
nielsen_email = "finn.nielsen@uni-muenster.de"
[nielsen.homepages]
[mansky]
name = "Susannah Mansky"
[mansky.emails]
mansky_email = "sjohnsn2@illinois.edu"
mansky_email1 = "susannahej@gmail.com"
[mansky.homepages]
[dunaev]
name = "Georgy Dunaev"
[dunaev.emails]
dunaev_email = "georgedunaev@gmail.com"
[dunaev.homepages]
[li]
name = "Wenda Li"
[li.emails]
li_email = "wl302@cam.ac.uk"
li_email1 = "liwenda1990@hotmail.com"
[li.homepages]
li_homepage = "https://www.cl.cam.ac.uk/~wl302/"
[stevens]
name = "Lukas Stevens"
[stevens.emails]
[stevens.homepages]
stevens_homepage = "https://www21.in.tum.de/team/stevensl"
[tourret]
name = "Sophie Tourret"
[tourret.emails]
tourret_email = "stourret@mpi-inf.mpg.de"
[tourret.homepages]
tourret_homepage = "https://www.mpi-inf.mpg.de/departments/automation-of-logic/people/sophie-tourret/"
[yu]
name = "Lei Yu"
[yu.emails]
yu_email = "ly271@cam.ac.uk"
[yu.homepages]
[grewe]
name = "Sylvia Grewe"
[grewe.emails]
grewe_email = "grewe@cs.tu-darmstadt.de"
[grewe.homepages]
[coghetto]
name = "Roland Coghetto"
[coghetto.emails]
coghetto_email = "roland_coghetto@hotmail.com"
[coghetto.homepages]
[schirmer]
name = "Norbert Schirmer"
[schirmer.emails]
schirmer_email = "norbert.schirmer@web.de"
[schirmer.homepages]
[immler]
name = "Fabian Immler"
[immler.emails]
immler_email = "immler@in.tum.de"
immler_email1 = "fimmler@cs.cmu.edu"
[immler.homepages]
immler_homepage = "https://home.in.tum.de/~immler/"
[tiu]
name = "Alwen Tiu"
[tiu.emails]
tiu_email = "ATiu@ntu.edu.sg"
[tiu.homepages]
tiu_homepage = "http://users.cecs.anu.edu.au/~tiu/"
[henrio]
name = "Ludovic Henrio"
[henrio.emails]
henrio_email = "Ludovic.Henrio@sophia.inria.fr"
[henrio.homepages]
[urban]
name = "Christian Urban"
[urban.emails]
urban_email = "christian.urban@kcl.ac.uk"
[urban.homepages]
urban_homepage = "https://nms.kcl.ac.uk/christian.urban/"
[michaelis]
name = "Julius Michaelis"
[michaelis.emails]
michaelis_email = "isabelleopenflow@liftm.de"
michaelis_email1 = "maintainafpppt@liftm.de"
michaelis_email2 = "bdd@liftm.de"
michaelis_email3 = "afp@liftm.de"
[michaelis.homepages]
michaelis_homepage = "http://liftm.de/"
[scott]
name = "Dana Scott"
[scott.emails]
[scott.homepages]
scott_homepage = "http://www.cs.cmu.edu/~scott/"
[wenzel]
name = "Makarius Wenzel"
[wenzel.emails]
wenzel_email = "Makarius.wenzel@lri.fr"
[wenzel.homepages]
[dardinier]
name = "Thibault Dardinier"
[dardinier.emails]
dardinier_email = "thibault.dardinier@inf.ethz.ch"
[dardinier.homepages]
dardinier_homepage = "https://dardinier.me/"
[lallemand]
name = "Joseph Lallemand"
[lallemand.emails]
lallemand_email = "joseph.lallemand@loria.fr"
[lallemand.homepages]
[schmoetten]
name = "Richard Schmoetten"
[schmoetten.emails]
schmoetten_email = "s1311325@sms.ed.ac.uk"
[schmoetten.homepages]
[cohen]
name = "Ernie Cohen"
[cohen.emails]
cohen_email = "ecohen@amazon.com"
[cohen.homepages]
[chapman]
name = "Peter Chapman"
[chapman.emails]
chapman_email = "pc@cs.st-andrews.ac.uk"
[chapman.homepages]
[rickmann]
name = "Christina Rickmann"
[rickmann.emails]
rickmann_email = "c.rickmann@tu-berlin.de"
[rickmann.homepages]
[raya]
name = "Rodrigo Raya"
[raya.emails]
[raya.homepages]
raya_homepage = "https://people.epfl.ch/rodrigo.raya"
[kadzioka]
name = "Jakub Kądziołka"
[kadzioka.emails]
kadzioka_email = "kuba@kadziolka.net"
[kadzioka.homepages]
[foster]
name = "Michael Foster"
[foster.emails]
foster_email = "m.foster@sheffield.ac.uk"
[foster.homepages]
[zhann]
name = "Naijun Zhan"
[zhann.emails]
[zhann.homepages]
[fuenmayor]
name = "David Fuenmayor"
[fuenmayor.emails]
fuenmayor_email = "davfuenmayor@gmail.com"
[fuenmayor.homepages]
[iwama]
name = "Fumiya Iwama"
[iwama.emails]
iwama_email = "d1623001@s.konan-u.ac.jp"
[iwama.homepages]
[feliachi]
name = "Abderrahmane Feliachi"
[feliachi.emails]
feliachi_email = "abderrahmane.feliachi@lri.fr"
[feliachi.homepages]
[sudbrock]
name = "Henning Sudbrock"
[sudbrock.emails]
sudbrock_email = "sudbrock@mais.informatik.tu-darmstadt.de"
[sudbrock.homepages]
[bauer]
name = "Gertrud Bauer"
[bauer.emails]
[bauer.homepages]
[lux]
name = "Alexander Lux"
[lux.emails]
lux_email = "lux@mais.informatik.tu-darmstadt.de"
[lux.homepages]
[seidler]
name = "Henning Seidler"
[seidler.emails]
seidler_email = "henning.seidler@mailbox.tu-berlin.de"
[seidler.homepages]
[desharnais]
name = "Martin Desharnais"
[desharnais.emails]
desharnais_email = "martin.desharnais@unibw.de"
[desharnais.homepages]
desharnais_homepage = "https://martin.desharnais.me"
[wasserrab]
name = "Daniel Wasserrab"
[wasserrab.emails]
[wasserrab.homepages]
wasserrab_homepage = "http://pp.info.uni-karlsruhe.de/personhp/daniel_wasserrab.php"
[fell]
name = "Julian Fell"
[fell.emails]
fell_email = "julian.fell@uq.net.au"
[fell.homepages]
[zhan]
name = "Bohua Zhan"
[zhan.emails]
zhan_email = "bzhan@ios.ac.cn"
[zhan.homepages]
zhan_homepage = "http://lcs.ios.ac.cn/~bzhan/"
[stephan]
name = "Werner Stephan"
[stephan.emails]
stephan_email = "stephan@dfki.de"
[stephan.homepages]
[david]
name = "Marco David"
[david.emails]
david_email = "marco.david@hotmail.de"
[david.homepages]
[olm]
name = "Markus Müller-Olm"
[olm.emails]
[olm.homepages]
olm_homepage = "http://cs.uni-muenster.de/u/mmo/"
[havle]
name = "Oto Havle"
[havle.emails]
havle_email = "oha@sysgo.com"
[havle.homepages]
[margetson]
name = "James Margetson"
[margetson.emails]
[margetson.homepages]
[scharager]
name = "Matias Scharager"
[scharager.emails]
scharager_email = "mscharag@cs.cmu.edu"
[scharager.homepages]
[haftmann]
name = "Florian Haftmann"
[haftmann.emails]
haftmann_email = "florian.haftmann@informatik.tu-muenchen.de"
[haftmann.homepages]
haftmann_homepage = "http://isabelle.in.tum.de/~haftmann"
[schoepe]
name = "Daniel Schoepe"
[schoepe.emails]
schoepe_email = "daniel@schoepe.org"
[schoepe.homepages]
[nagele]
name = "Julian Nagele"
[nagele.emails]
nagele_email = "julian.nagele@uibk.ac.at"
[nagele.homepages]
[hoefner]
name = "Peter Höfner"
[hoefner.emails]
hoefner_email = "peter@hoefner-online.de"
[hoefner.homepages]
hoefner_homepage = "http://www.hoefner-online.de/"
[derrick]
name = "John Derrick"
[derrick.emails]
derrick_email = "j.derrick@sheffield.ac.uk"
[derrick.homepages]
[beeren]
name = "Joel Beeren"
[beeren.emails]
[beeren.homepages]
[echenim]
name = "Mnacho Echenim"
[echenim.emails]
echenim_email = "mnacho.echenim@univ-grenoble-alpes.fr"
[echenim.homepages]
echenim_homepage = "https://lig-membres.imag.fr/mechenim/"
[vytiniotis]
name = "Dimitrios Vytiniotis"
[vytiniotis.emails]
[vytiniotis.homepages]
vytiniotis_homepage = "http://research.microsoft.com/en-us/people/dimitris/"
[beringer]
name = "Lennart Beringer"
[beringer.emails]
beringer_email = "lennart.beringer@ifi.lmu.de"
[beringer.homepages]
[wickerson]
name = "John Wickerson"
[wickerson.emails]
[wickerson.homepages]
wickerson_homepage = "http://www.doc.ic.ac.uk/~jpw48"
[eberl]
name = "Manuel Eberl"
[eberl.emails]
eberl_email = "manuel@pruvisto.org"
eberl_email1 = "manuel.eberl@tum.de"
[eberl.homepages]
eberl_homepage = "https://pruvisto.org/"
eberl_homepage2 = "https://www.in.tum.de/~eberlm"
[noce]
name = "Pasquale Noce"
[noce.emails]
noce_email = "pasquale.noce.lavoro@gmail.com"
[noce.homepages]
[gunther]
name = "Emmanuel Gunther"
[gunther.emails]
gunther_email = "gunther@famaf.unc.edu.ar"
[gunther.homepages]
[nemouchi]
name = "Yakoub Nemouchi"
[nemouchi.emails]
nemouchi_email = "nemouchi@lri.fr"
nemouchi_email1 = "yakoub.nemouchi@york.ac.uk"
[nemouchi.homepages]
[stueber]
name = "Anke Stüber"
[stueber.emails]
stueber_email = "anke.stueber@campus.tu-berlin.de"
[stueber.homepages]
[sternagel]
name = "Christian Sternagel"
[sternagel.emails]
sternagel_email = "c.sternagel@gmail.com"
sternagel_email1 = "christian.sternagel@uibk.ac.at"
[sternagel.homepages]
sternagel_homepage = "http://cl-informatik.uibk.ac.at/users/griff/"
[sachtleben]
name = "Robert Sachtleben"
[sachtleben.emails]
sachtleben_email = "rob_sac@uni-bremen.de"
[sachtleben.homepages]
[kastermans]
name = "Bart Kastermans"
[kastermans.emails]
[kastermans.homepages]
kastermans_homepage = "http://kasterma.net"
[pal]
name = "Abhik Pal"
[pal.emails]
[pal.homepages]
[thiemann]
name = "René Thiemann"
[thiemann.emails]
thiemann_email = "rene.thiemann@uibk.ac.at"
[thiemann.homepages]
thiemann_homepage = "http://cl-informatik.uibk.ac.at/users/thiemann/"
[campo]
name = "Alejandro del Campo"
[campo.emails]
campo_email = "alejandro.del-campo@alum.unirioja.es"
[campo.homepages]
[raska]
name = "Martin Raška"
[raska.emails]
[raska.homepages]
[stannett]
name = "Mike Stannett"
[stannett.emails]
stannett_email = "m.stannett@sheffield.ac.uk"
[stannett.homepages]
[back]
name = "Ralph-Johan Back"
[back.emails]
[back.homepages]
back_homepage = "http://users.abo.fi/Ralph-Johan.Back/"
[bruegger]
name = "Lukas Brügger"
[bruegger.emails]
bruegger_email = "lukas.a.bruegger@gmail.com"
[bruegger.homepages]
[kuncak]
name = "Viktor Kuncak"
[kuncak.emails]
[kuncak.homepages]
kuncak_homepage = "http://lara.epfl.ch/~kuncak/"
[gaudel]
name = "Marie-Claude Gaudel"
[gaudel.emails]
gaudel_email = "mcg@lri.fr"
[gaudel.homepages]
[sison]
name = "Robert Sison"
[sison.emails]
[sison.homepages]
[benzmueller]
name = "Christoph Benzmüller"
[benzmueller.emails]
benzmueller_email = "c.benzmueller@gmail.com"
benzmueller_email1 = "c.benzmueller@fu-berlin.de"
[benzmueller.homepages]
benzmueller_homepage = "http://christoph-benzmueller.de"
benzmueller_homepage1 = "http://page.mi.fu-berlin.de/cbenzmueller/"
[from]
name = "Asta Halkjær From"
[from.emails]
from_email = "ahfrom@dtu.dk"
[from.homepages]
from_homepage = "https://people.compute.dtu.dk/ahfrom/"
[tuongj]
name = "Joseph Tuong"
[tuongj.emails]
[tuongj.homepages]
[zeller]
name = "Peter Zeller"
[zeller.emails]
zeller_email = "p_zeller@cs.uni-kl.de"
[zeller.homepages]
[schmidinger]
name = "Lukas Schmidinger"
[schmidinger.emails]
[schmidinger.homepages]
[ravindran]
name = "Binoy Ravindran"
[ravindran.emails]
[ravindran.homepages]
[rizaldi]
name = "Albert Rizaldi"
[rizaldi.emails]
rizaldi_email = "albert.rizaldi@ntu.edu.sg"
[rizaldi.homepages]
[sabouret]
name = "Nicolas Sabouret"
[sabouret.emails]
[sabouret.homepages]
[butler]
name = "David Butler"
[butler.emails]
butler_email = "dbutler@turing.ac.uk"
[butler.homepages]
butler_homepage = "https://www.turing.ac.uk/people/doctoral-students/david-butler"
[sprenger]
name = "Christoph Sprenger"
[sprenger.emails]
sprenger_email = "sprenger@inf.ethz.ch"
[sprenger.homepages]
[bordg]
name = "Anthony Bordg"
[bordg.emails]
bordg_email = "apdb3@cam.ac.uk"
[bordg.homepages]
bordg_homepage = "https://sites.google.com/site/anthonybordg/"
[bhatt]
name = "Bhargav Bhatt"
[bhatt.emails]
bhatt_email = "bhargav.bhatt@inf.ethz.ch"
[bhatt.homepages]
[gonzalez]
name = "Edgar Gonzàlez"
[gonzalez.emails]
gonzalez_email = "edgargip@google.com"
[gonzalez.homepages]
[adelsberger]
name = "Stephan Adelsberger"
[adelsberger.emails]
adelsberger_email = "stvienna@gmail.com"
[adelsberger.homepages]
adelsberger_homepage = "http://nm.wu.ac.at/nm/sadelsbe"
[schleicher]
name = "Dierk Schleicher"
[schleicher.emails]
[schleicher.homepages]
[ying]
name = "Shenggang Ying"
[ying.emails]
[ying.homepages]
[brien]
name = "Nicolas Robinson-O'Brien"
[brien.emails]
[brien.homepages]
[kobayashi]
name = "Hidetsune Kobayashi"
[kobayashi.emails]
[kobayashi.homepages]
[krauss]
name = "Alexander Krauss"
[krauss.emails]
krauss_email = "krauss@in.tum.de"
[krauss.homepages]
krauss_homepage = "http://www.in.tum.de/~krauss"
[somaini]
name = "Ivano Somaini"
[somaini.emails]
[somaini.homepages]
[seidl]
name = "Benedikt Seidl"
[seidl.emails]
seidl_email = "benedikt.seidl@tum.de"
[seidl.homepages]
[edmonds]
name = "Chelsea Edmonds"
[edmonds.emails]
edmonds_email = "cle47@cam.ac.uk"
[edmonds.homepages]
edmonds_homepage = "https://www.cst.cam.ac.uk/people/cle47"
[debrat]
name = "Henri Debrat"
[debrat.emails]
debrat_email = "henri.debrat@loria.fr"
[debrat.homepages]
[holub]
name = "Štěpán Holub"
[holub.emails]
holub_email = "holub@karlin.mff.cuni.cz"
[holub.homepages]
holub_homepage = "https://www2.karlin.mff.cuni.cz/~holub/"
[beresford]
name = "Alastair R. Beresford"
[beresford.emails]
beresford_email = "arb33@cam.ac.uk"
[beresford.homepages]
[terraf]
name = "Pedro Sánchez Terraf"
[terraf.emails]
terraf_email = "psterraf@unc.edu.ar"
[terraf.homepages]
terraf_homepage = "https://cs.famaf.unc.edu.ar/~pedro/home_en.html"
[raumer]
name = "Jakob von Raumer"
[raumer.emails]
raumer_email = "psxjv4@nottingham.ac.uk"
[raumer.homepages]
[pagano]
name = "Miguel Pagano"
[pagano.emails]
pagano_email = "miguel.pagano@unc.edu.ar"
[pagano.homepages]
pagano_homepage = "https://cs.famaf.unc.edu.ar/~mpagano/"
[coglio]
name = "Alessandro Coglio"
[coglio.emails]
coglio_email = "coglio@kestrel.edu"
[coglio.homepages]
coglio_homepage = "http://www.kestrel.edu/~coglio"
[caballero]
name = "José Manuel Rodríguez Caballero"
[caballero.emails]
caballero_email = "jose.manuel.rodriguez.caballero@ut.ee"
[caballero.homepages]
caballero_homepage = "https://josephcmac.github.io/"
[grechuk]
name = "Bogdan Grechuk"
[grechuk.emails]
grechuk_email = "grechukbogdan@yandex.ru"
[grechuk.homepages]
[sewell]
name = "Thomas Sewell"
[sewell.emails]
[sewell.homepages]
[leustean]
name = "Laurentiu Leustean"
[leustean.emails]
[leustean.homepages]
[rosskopf]
name = "Simon Roßkopf"
[rosskopf.emails]
rosskopf_email = "rosskops@in.tum.de"
[rosskopf.homepages]
rosskopf_homepage = "http://www21.in.tum.de/~rosskops"
[aspinall]
name = "David Aspinall"
[aspinall.emails]
[aspinall.homepages]
aspinall_homepage = "http://homepages.inf.ed.ac.uk/da/"
[ausaf]
name = "Fahad Ausaf"
[ausaf.emails]
[ausaf.homepages]
ausaf_homepage = "http://kcl.academia.edu/FahadAusaf"
[diekmann]
name = "Cornelius Diekmann"
[diekmann.emails]
diekmann_email = "diekmann@net.in.tum.de"
[diekmann.homepages]
diekmann_homepage = "http://net.in.tum.de/~diekmann"
[fouillard]
name = "Valentin Fouillard"
[fouillard.emails]
fouillard_email = "valentin.fouillard@limsi.fr"
[fouillard.homepages]
[willenbrink]
name = "Sebastian Willenbrink"
[willenbrink.emails]
willenbrink_email = "sebastian.willenbrink@tum.de"
[willenbrink.homepages]
[xu]
name = "Jian Xu"
[xu.emails]
[xu.homepages]
[wang]
name = "Shuling Wang"
[wang.emails]
[wang.homepages]
[ridge]
name = "Tom Ridge"
[ridge.emails]
[ridge.homepages]
[kleppmann]
name = "Martin Kleppmann"
[kleppmann.emails]
kleppmann_email = "martin.kleppmann@cl.cam.ac.uk"
[kleppmann.homepages]
[kreuzer]
name = "Katharina Kreuzer"
[kreuzer.emails]
kreuzer_email = "kreuzerk@in.tum.de"
[kreuzer.homepages]
kreuzer_homepage = "https://www21.in.tum.de/team/kreuzer/"
[traut]
name = "Christoph Traut"
[traut.emails]
[traut.homepages]
[blanchette]
name = "Jasmin Christian Blanchette"
[blanchette.emails]
blanchette_email = "jasmin.blanchette@gmail.com"
blanchette_email1 = "j.c.blanchette@vu.nl"
[blanchette.homepages]
blanchette_homepage = "http://www21.in.tum.de/~blanchet"
blanchette_homepage1 = "https://www.cs.vu.nl/~jbe248/"
[van]
name = "Hai Nguyen Van"
[van.emails]
van_email = "hai.nguyenvan.phie@gmail.com"
[van.homepages]
[brunner]
name = "Julian Brunner"
[brunner.emails]
brunner_email = "brunnerj@in.tum.de"
[brunner.homepages]
brunner_homepage = "http://www21.in.tum.de/~brunnerj/"
[reiche]
name = "Sebastian Reiche"
[reiche.emails]
[reiche.homepages]
reiche_homepage = "https://www.linkedin.com/in/sebastian-reiche-0b2093178"
[eriksson]
name = "Lars-Henrik Eriksson"
[eriksson.emails]
eriksson_email = "lhe@it.uu.se"
[eriksson.homepages]
[nipkow]
name = "Tobias Nipkow"
[nipkow.emails]
nipkow_email = "nipkow@in.tum.de"
[nipkow.homepages]
nipkow_homepage = "https://www.in.tum.de/~nipkow/"
[divason]
name = "Jose Divasón"
[divason.emails]
divason_email = "jose.divason@unirioja.es"
[divason.homepages]
divason_homepage = "https://www.unirioja.es/cu/jodivaso/"
[barsotti]
name = "Damián Barsotti"
[barsotti.emails]
[barsotti.homepages]
barsotti_homepage = "http://www.cs.famaf.unc.edu.ar/~damian/"
[nagashima]
name = "Yutaka Nagashima"
[nagashima.emails]
nagashima_email = "Yutaka.Nagashima@data61.csiro.au"
[nagashima.homepages]
[avigad]
name = "Jeremy Avigad"
[avigad.emails]
avigad_email = "avigad@cmu.edu"
[avigad.homepages]
avigad_homepage = "http://www.andrew.cmu.edu/user/avigad/"
[abdulaziz]
name = "Mohammad Abdulaziz"
[abdulaziz.emails]
abdulaziz_email = "mohammad.abdulaziz@in.tum.de"
abdulaziz_email1 = "mohammad.abdulaziz8@gmail.com"
[abdulaziz.homepages]
abdulaziz_homepage = "http://home.in.tum.de/~mansour/"
[kuncar]
name = "Ondřej Kunčar"
[kuncar.emails]
[kuncar.homepages]
kuncar_homepage = "http://www21.in.tum.de/~kuncar/"
[borgstroem]
name = "Johannes Borgström"
[borgstroem.emails]
borgstroem_email = "johannes.borgstrom@it.uu.se"
[borgstroem.homepages]
[kurz]
name = "Friedrich Kurz"
[kurz.emails]
kurz_email = "friedrich.kurz@tum.de"
[kurz.homepages]
[noschinski]
name = "Lars Noschinski"
[noschinski.emails]
noschinski_email = "noschinl@gmail.com"
[noschinski.homepages]
noschinski_homepage = "http://www21.in.tum.de/~noschinl/"
[liy]
name = "Yangjia Li"
[liy.emails]
[liy.homepages]
[wimmer]
name = "Simon Wimmer"
[wimmer.emails]
wimmer_email = "simon.wimmer@tum.de"
[wimmer.homepages]
wimmer_homepage = "http://home.in.tum.de/~wimmers/"
[gammie]
name = "Peter Gammie"
[gammie.emails]
gammie_email = "peteg42@gmail.com"
[gammie.homepages]
gammie_homepage = "http://peteg.org"
[snelting]
name = "Gregor Snelting"
[snelting.emails]
[snelting.homepages]
snelting_homepage = "http://pp.info.uni-karlsruhe.de/personhp/gregor_snelting.php"
[stark]
name = "Eugene W. Stark"
[stark.emails]
stark_email = "stark@cs.stonybrook.edu"
[stark.homepages]
[engelhardt]
name = "Kai Engelhardt"
[engelhardt.emails]
[engelhardt.homepages]
[fleury]
name = "Mathias Fleury"
[fleury.emails]
fleury_email = "fleury@mpi-inf.mpg.de"
fleury_email1 = "mathias.fleury@jku.at"
[fleury.homepages]
fleury_homepage = "http://fmv.jku.at/fleury"
[griebel]
name = "Simon Griebel"
[griebel.emails]
griebel_email = "s.griebel@tum.de"
[griebel.homepages]
[zhang]
name = "Yu Zhang"
[zhang.emails]
[zhang.homepages]
[spichkova]
name = "Maria Spichkova"
[spichkova.emails]
spichkova_email = "maria.spichkova@rmit.edu.au"
[spichkova.homepages]
[andronick]
name = "June Andronick"
[andronick.emails]
[andronick.homepages]
[lammich]
name = "Peter Lammich"
[lammich.emails]
lammich_email = "lammich@in.tum.de"
lammich_email1 = "peter.lammich@uni-muenster.de"
[lammich.homepages]
lammich_homepage = "http://www21.in.tum.de/~lammich"
[maricf]
name = "Filip Marić"
[maricf.emails]
maricf_email = "filip@matf.bg.ac.rs"
[maricf.homepages]
maricf_homepage = "http://www.matf.bg.ac.rs/~filip"
[popescu]
name = "Andrei Popescu"
[popescu.emails]
popescu_email = "a.popescu@sheffield.ac.uk"
popescu_email1 = "uuomul@yahoo.com"
popescu_email2 = "a.popescu@mdx.ac.uk"
[popescu.homepages]
popescu_homepage = "https://www.andreipopescu.uk"
[chen]
name = "L. Chen"
[chen.emails]
[chen.homepages]
[helke]
name = "Steffen Helke"
[helke.emails]
helke_email = "helke@cs.tu-berlin.de"
[helke.homepages]
[pohjola]
name = "Johannes Åman Pohjola"
[pohjola.emails]
[pohjola.homepages]
[yingm]
name = "Mingsheng Ying"
[yingm.emails]
[yingm.homepages]
[fosterj]
name = "J. Nathan Foster"
[fosterj.emails]
[fosterj.homepages]
fosterj_homepage = "http://www.cs.cornell.edu/~jnfoster/"
[verbeek]
name = "Freek Verbeek"
[verbeek.emails]
verbeek_email = "Freek.Verbeek@ou.nl"
verbeek_email1 = "freek@vt.edu"
[verbeek.homepages]
[struth]
name = "Georg Struth"
[struth.emails]
struth_email = "g.struth@sheffield.ac.uk"
[struth.homepages]
struth_homepage = "http://staffwww.dcs.shef.ac.uk/people/G.Struth/"
[mitsch]
name = "Stefan Mitsch"
[mitsch.emails]
mitsch_email = "smitsch@cs.cmu.edu"
[mitsch.homepages]
[nordhoff]
name = "Benedikt Nordhoff"
[nordhoff.emails]
nordhoff_email = "b.n@wwu.de"
nordhoff_email1 = "b_nord01@uni-muenster.de"
[nordhoff.homepages]
[kirchner]
name = "Daniel Kirchner"
[kirchner.emails]
kirchner_email = "daniel@ekpyron.org"
[kirchner.homepages]
[merz]
name = "Stephan Merz"
[merz.emails]
merz_email = "Stephan.Merz@loria.fr"
[merz.homepages]
merz_homepage = "http://www.loria.fr/~merz"
[fernandez]
name = "Matthew Fernandez"
[fernandez.emails]
[fernandez.homepages]
[kolanski]
name = "Rafal Kolanski"
[kolanski.emails]
kolanski_email = "rafal.kolanski@nicta.com.au"
[kolanski.homepages]
[strnisa]
name = "Rok Strniša"
[strnisa.emails]
strnisa_email = "rok@strnisa.com"
[strnisa.homepages]
strnisa_homepage = "http://rok.strnisa.com/lj/"
[liuy]
name = "Yang Liu"
[liuy.emails]
liuy_email = "yangliu@ntu.edu.sg"
[liuy.homepages]
[jacobsen]
name = "Frederik Krogsdal Jacobsen"
[jacobsen.emails]
jacobsen_email = "fkjac@dtu.dk"
[jacobsen.homepages]
jacobsen_homepage = "http://people.compute.dtu.dk/fkjac/"
[crighton]
name = "Aaron Crighton"
[crighton.emails]
crighton_email = "crightoa@mcmaster.ca"
[crighton.homepages]
[matiyasevich]
name = "Yuri Matiyasevich"
[matiyasevich.emails]
[matiyasevich.homepages]
[kaliszyk]
name = "Cezary Kaliszyk"
[kaliszyk.emails]
kaliszyk_email = "cezary.kaliszyk@uibk.ac.at"
[kaliszyk.homepages]
kaliszyk_homepage = "http://cl-informatik.uibk.ac.at/users/cek/"
[voisin]
name = "Frederic Voisin"
[voisin.emails]
[voisin.homepages]
[kaufmann]
name = "Daniela Kaufmann"
[kaufmann.emails]
[kaufmann.homepages]
kaufmann_homepage = "http://fmv.jku.at/kaufmann"
[milehins]
name = "Mihails Milehins"
[milehins.emails]
milehins_email = "mihailsmilehins@gmail.com"
[milehins.homepages]
[cordwell]
name = "Katherine Cordwell"
[cordwell.emails]
cordwell_email = "kcordwel@cs.cmu.edu"
[cordwell.homepages]
cordwell_homepage = "https://www.cs.cmu.edu/~kcordwel/"
[smaus]
name = "Jan-Georg Smaus"
[smaus.emails]
[smaus.homepages]
smaus_homepage = "http://www.irit.fr/~Jan-Georg.Smaus"
[sefidgar]
name = "S. Reza Sefidgar"
[sefidgar.emails]
sefidgar_email = "reza.sefidgar@inf.ethz.ch"
[sefidgar.homepages]
[steinberg]
name = "Matías Steinberg"
[steinberg.emails]
steinberg_email = "matias.steinberg@mi.unc.edu.ar"
[steinberg.homepages]
[furusawa]
name = "Hitoshi Furusawa"
[furusawa.emails]
[furusawa.homepages]
furusawa_homepage = "http://www.sci.kagoshima-u.ac.jp/~furusawa/"
[unruh]
name = "Dominique Unruh"
[unruh.emails]
unruh_email = "unruh@ut.ee"
[unruh.homepages]
unruh_homepage = "https://www.ut.ee/~unruh/"
[yamada]
name = "Akihisa Yamada"
[yamada.emails]
yamada_email = "akihisa.yamada@uibk.ac.at"
yamada_email1 = "ayamada@trs.cm.is.nagoya-u.ac.jp"
yamada_email2 = "akihisa.yamada@aist.go.jp"
yamada_email3 = "akihisayamada@nii.ac.jp"
[yamada.homepages]
yamada_homepage = "http://group-mmm.org/~ayamada/"
[smola]
name = "Filip Smola"
[smola.emails]
smola_email = "f.smola@sms.ed.ac.uk"
[smola.homepages]
[pusch]
name = "Cornelia Pusch"
[pusch.emails]
[pusch.homepages]
[ogawa]
name = "Mizuhito Ogawa"
[ogawa.emails]
[ogawa.homepages]
[bulwahn]
name = "Lukas Bulwahn"
[bulwahn.emails]
bulwahn_email = "lukas.bulwahn@gmail.com"
[bulwahn.homepages]
[obua]
name = "Steven Obua"
[obua.emails]
obua_email = "steven@recursivemind.com"
[obua.homepages]
[bayer]
name = "Jonas Bayer"
[bayer.emails]
bayer_email = "jonas.bayer999@gmail.com"
[bayer.homepages]
[brun]
name = "Matthias Brun"
[brun.emails]
brun_email = "matthias.brun@inf.ethz.ch"
[brun.homepages]
[aransay]
name = "Jesús Aransay"
[aransay.emails]
aransay_email = "jesus-maria.aransay@unirioja.es"
[aransay.homepages]
aransay_homepage = "https://www.unirioja.es/cu/jearansa"
[gioiosa]
name = "Gianpaolo Gioiosa"
[gioiosa.emails]
[gioiosa.homepages]
[karayel]
name = "Emin Karayel"
[karayel.emails]
karayel_email = "me@eminkarayel.de"
[karayel.homepages]
karayel_homepage = "https://orcid.org/0000-0003-3290-5034"
[koller]
name = "Lukas Koller"
[koller.emails]
koller_email = "lukas.koller@tum.de"
[koller.homepages]
[starosta]
name = "Štěpán Starosta"
[starosta.emails]
starosta_email = "stepan.starosta@fit.cvut.cz"
[starosta.homepages]
starosta_homepage = "https://users.fit.cvut.cz/~staroste/"
[zhangx]
name = "Xingyuan Zhang"
[zhangx.emails]
[zhangx.homepages]
[katovsky]
name = "Alexander Katovsky"
[katovsky.emails]
katovsky_email = "apk32@cam.ac.uk"
katovsky_email1 = "alexander.katovsky@cantab.net"
[katovsky.homepages]
[roessle]
name = "Ian Roessle"
[roessle.emails]
[roessle.homepages]
[schoepf]
name = "Jonas Schöpf"
[schoepf.emails]
schoepf_email = "jonas.schoepf@uibk.ac.at"
[schoepf.homepages]
[gheri]
name = "Lorenzo Gheri"
[gheri.emails]
gheri_email = "lor.gheri@gmail.com"
[gheri.homepages]
[oosterhuis]
name = "Roelof Oosterhuis"
[oosterhuis.emails]
oosterhuis_email = "roelofoosterhuis@gmail.com"
[oosterhuis.homepages]
[robillard]
name = "Simon Robillard"
[robillard.emails]
[robillard.homepages]
robillard_homepage = "https://simon-robillard.net/"
[rauch]
name = "Nicole Rauch"
[rauch.emails]
rauch_email = "rauch@informatik.uni-kl.de"
[rauch.homepages]
[wolff]
name = "Burkhart Wolff"
[wolff.emails]
wolff_email = "burkhart.wolff@lri.fr"
[wolff.homepages]
wolff_homepage = "https://www.lri.fr/~wolff/"
[lattuada]
name = "Andrea Lattuada"
[lattuada.emails]
[lattuada.homepages]
lattuada_homepage = "https://andrea.lattuada.me"
[pierzchalski]
name = "Edward Pierzchalski"
[pierzchalski.emails]
[pierzchalski.homepages]
[chaieb]
name = "Amine Chaieb"
[chaieb.emails]
[chaieb.homepages]
[raszyk]
name = "Martin Raszyk"
[raszyk.emails]
raszyk_email = "martin.raszyk@inf.ethz.ch"
raszyk_email1 = "m.raszyk@gmail.com"
[raszyk.homepages]
[zee]
name = "Karen Zee"
[zee.emails]
zee_email = "kkz@mit.edu"
[zee.homepages]
zee_homepage = "http://www.mit.edu/~kkz/"
[jensen]
name = "Alexander Birch Jensen"
[jensen.emails]
jensen_email = "aleje@dtu.dk"
[jensen.homepages]
jensen_homepage = "https://people.compute.dtu.dk/aleje/"
[murray]
name = "Toby Murray"
[murray.emails]
murray_email = "toby.murray@unimelb.edu.au"
[murray.homepages]
murray_homepage = "https://people.eng.unimelb.edu.au/tobym/"
[hupel]
name = "Lars Hupel"
[hupel.emails]
hupel_email = "hupel@in.tum.de"
hupel_email1 = "lars@hupel.info"
[hupel.homepages]
hupel_homepage = "https://www21.in.tum.de/~hupel/"
hupel_homepage1 = "https://lars.hupel.info/"
[rowat]
name = "Colin Rowat"
[rowat.emails]
rowat_email = "c.rowat@bham.ac.uk"
[rowat.homepages]
[schneider]
name = "Joshua Schneider"
[schneider.emails]
schneider_email = "joshua.schneider@inf.ethz.ch"
[schneider.homepages]
[cousin]
name = "Marie Cousin"
[cousin.emails]
cousin_email = "marie.cousin@grenoble-inp.org"
[cousin.homepages]
[parsert]
name = "Julian Parsert"
[parsert.emails]
parsert_email = "julian.parsert@gmail.com"
parsert_email1 = "julian.parsert@uibk.ac.at"
[parsert.homepages]
parsert_homepage = "http://www.parsert.com/"
[aehlig]
name = "Klaus Aehlig"
[aehlig.emails]
[aehlig.homepages]
aehlig_homepage = "http://www.linta.de/~aehlig/"
[argyraki]
name = "Angeliki Koutsoukou-Argyraki"
[argyraki.emails]
argyraki_email = "ak2110@cam.ac.uk"
[argyraki.homepages]
argyraki_homepage = "https://www.cl.cam.ac.uk/~ak2110/"
argyraki_homepage2 = "https://www.cst.cam.ac.uk/people/ak2110"
[ye]
name = "Lina Ye"
[ye.emails]
ye_email = "lina.ye@lri.fr"
[ye.homepages]
[moeller]
name = "Bernhard Möller"
[moeller.emails]
[moeller.homepages]
moeller_homepage = "https://www.informatik.uni-augsburg.de/en/chairs/dbis/pmi/staff/moeller/"
[zankl]
name = "Harald Zankl"
[zankl.emails]
zankl_email = "Harald.Zankl@uibk.ac.at"
[zankl.homepages]
zankl_homepage = "http://cl-informatik.uibk.ac.at/users/hzankl"
[langenstein]
name = "Bruno Langenstein"
[langenstein.emails]
langenstein_email = "langenstein@dfki.de"
[langenstein.homepages]
[breitner]
name = "Joachim Breitner"
[breitner.emails]
breitner_email = "mail@joachim-breitner.de"
breitner_email1 = "joachim@cis.upenn.edu"
[breitner.homepages]
breitner_homepage = "http://pp.ipd.kit.edu/~breitner"
[thommes]
name = "Joseph Thommes"
[thommes.emails]
thommes_email = "joseph-thommes@gmx.de"
[thommes.homepages]
[loibl]
name = "Matthias Loibl"
[loibl.emails]
[loibl.homepages]
[cock]
name = "David Cock"
[cock.emails]
cock_email = "david.cock@nicta.com.au"
[cock.homepages]
[stuewe]
name = "Daniel Stüwe"
[stuewe.emails]
[stuewe.homepages]
[decova]
name = "Sára Decova"
[decova.emails]
[decova.homepages]
[nikiforov]
name = "Denis Nikiforov"
[nikiforov.emails]
nikiforov_email = "denis.nikif@gmail.com"
[nikiforov.homepages]
[traytel]
name = "Dmitriy Traytel"
[traytel.emails]
traytel_email = "traytel@in.tum.de"
traytel_email1 = "traytel@inf.ethz.ch"
traytel_email2 = "traytel@di.ku.dk"
[traytel.homepages]
traytel_homepage = "https://traytel.bitbucket.io/"
[tverdyshev]
name = "Sergey Tverdyshev"
[tverdyshev.emails]
tverdyshev_email = "stv@sysgo.com"
[tverdyshev.homepages]
[wassell]
name = "Mark Wassell"
[wassell.emails]
wassell_email = "mpwassell@gmail.com"
[wassell.homepages]
[ijbema]
name = "Mark Ijbema"
[ijbema.emails]
ijbema_email = "ijbema@fmf.nl"
[ijbema.homepages]
[wirt]
name = "Kai Wirt"
[wirt.emails]
[wirt.homepages]
[matache]
name = "Cristina Matache"
[matache.emails]
matache_email = "cris.matache@gmail.com"
[matache.homepages]
[ito]
name = "Yosuke Ito"
[ito.emails]
ito_email = "glacier345@gmail.com"
[ito.homepages]
[maric]
name = "Ognjen Marić"
[maric.emails]
maric_email = "ogi.afp@mynosefroze.com"
[maric.homepages]
[heimes]
name = "Lukas Heimes"
[heimes.emails]
heimes_email = "heimesl@student.ethz.ch"
[heimes.homepages]
[parrow]
name = "Joachim Parrow"
[parrow.emails]
parrow_email = "joachim.parrow@it.uu.se"
[parrow.homepages]
[naraschewski]
name = "Wolfgang Naraschewski"
[naraschewski.emails]
[naraschewski.homepages]
[amani]
name = "Sidney Amani"
[amani.emails]
amani_email = "sidney.amani@data61.csiro.au"
[amani.homepages]
[palmer]
name = "Jake Palmer"
[palmer.emails]
palmer_email = "jake.palmer@ed.ac.uk"
[palmer.homepages]
[bockenek]
name = "Joshua Bockenek"
[bockenek.emails]
[bockenek.homepages]
[lachnitt]
name = "Hanna Lachnitt"
[lachnitt.emails]
lachnitt_email = "lachnitt@stanford.edu"
[lachnitt.homepages]
[rabe]
name = "Markus N. Rabe"
[rabe.emails]
[rabe.homepages]
rabe_homepage = "http://www.react.uni-saarland.de/people/rabe.html"
[munive]
name = "Jonathan Julian Huerta y Munive"
[munive.emails]
munive_email = "jjhuertaymunive1@sheffield.ac.uk"
munive_email1 = "jonjulian23@gmail.com"
[munive.homepages]
[gouezel]
name = "Sebastien Gouezel"
[gouezel.emails]
gouezel_email = "sebastien.gouezel@univ-rennes1.fr"
[gouezel.homepages]
gouezel_homepage = "http://www.math.sciences.univ-nantes.fr/~gouezel/"
[brucker]
name = "Achim D. Brucker"
[brucker.emails]
brucker_email = "a.brucker@exeter.ac.uk"
brucker_email1 = "brucker@spamfence.net"
brucker_email2 = "adbrucker@0x5f.org"
[brucker.homepages]
brucker_homepage = "https://www.brucker.ch/"
[sato]
name = "Tetsuya Sato"
[sato.emails]
sato_email = "tsato@c.titech.ac.jp"
[sato.homepages]
sato_homepage = "https://sites.google.com/view/tetsuyasato/"
[huffman]
name = "Brian Huffman"
[huffman.emails]
huffman_email = "huffman@in.tum.de"
huffman_email1 = "brianh@cs.pdx.edu"
[huffman.homepages]
huffman_homepage = "http://cs.pdx.edu/~brianh/"
[fleuriot]
name = "Jacques D. Fleuriot"
[fleuriot.emails]
fleuriot_email = "Jacques.Fleuriot@ed.ac.uk"
fleuriot_email1 = "jdf@ed.ac.uk"
[fleuriot.homepages]
fleuriot_homepage = "https://www.inf.ed.ac.uk/people/staff/Jacques_Fleuriot.html"
[hess]
name = "Andreas V. Hess"
[hess.emails]
hess_email = "avhe@dtu.dk"
hess_email1 = "andreasvhess@gmail.com"
[hess.homepages]
[marmsoler]
name = "Diego Marmsoler"
[marmsoler.emails]
marmsoler_email = "diego.marmsoler@tum.de"
[marmsoler.homepages]
marmsoler_homepage = "http://marmsoler.com"
[hibon]
name = "Quentin Hibon"
[hibon.emails]
hibon_email = "qh225@cl.cam.ac.uk"
[hibon.homepages]
[tasch]
name = "Markus Tasch"
[tasch.emails]
tasch_email = "tasch@mais.informatik.tu-darmstadt.de"
[tasch.homepages]
[doty]
name = "Matthew Wampler-Doty"
[doty.emails]
[doty.homepages]
[berghofer]
name = "Stefan Berghofer"
[berghofer.emails]
berghofer_email = "berghofe@in.tum.de"
[berghofer.homepages]
berghofer_homepage = "http://www.in.tum.de/~berghofe"
[hirata]
name = "Michikazu Hirata"
[hirata.emails]
hirata_email = "hirata.m.ac@m.titech.ac.jp"
[hirata.homepages]
[sylvestre]
name = "Jeremy Sylvestre"
[sylvestre.emails]
sylvestre_email = "jeremy.sylvestre@ualberta.ca"
sylvestre_email1 = "jsylvest@ualberta.ca"
[sylvestre.homepages]
sylvestre_homepage = "http://ualberta.ca/~jsylvest/"
[lindenberg]
name = "Christina Lindenberg"
[lindenberg.emails]
[lindenberg.homepages]
[joosten]
name = "Sebastiaan J. C. Joosten"
[joosten.emails]
joosten_email = "sebastiaan.joosten@uibk.ac.at"
joosten_email1 = "sjcjoosten@gmail.com"
joosten_email2 = "s.j.c.joosten@utwente.nl"
[joosten.homepages]
joosten_homepage = "https://sjcjoosten.nl/"
[blumson]
name = "Ben Blumson"
[blumson.emails]
blumson_email = "benblumson@gmail.com"
[blumson.homepages]
blumson_homepage = "https://philpeople.org/profiles/ben-blumson"
[hosking]
name = "Tony Hosking"
[hosking.emails]
[hosking.homepages]
hosking_homepage = "https://www.cs.purdue.edu/homes/hosking/"
[preoteasa]
name = "Viorel Preoteasa"
[preoteasa.emails]
preoteasa_email = "viorel.preoteasa@aalto.fi"
[preoteasa.homepages]
preoteasa_homepage = "http://users.abo.fi/vpreotea/"
[gutkovas]
name = "Ramunas Gutkovas"
[gutkovas.emails]
gutkovas_email = "ramunas.gutkovas@it.uu.se"
[gutkovas.homepages]
[minamide]
name = "Yasuhiko Minamide"
[minamide.emails]
minamide_email = "minamide@is.titech.ac.jp"
[minamide.homepages]
minamide_homepage = "https://sv.c.titech.ac.jp/minamide/index.en.html"
[waldmann]
name = "Uwe Waldmann"
[waldmann.emails]
waldmann_email = "waldmann@mpi-inf.mpg.de"
[waldmann.homepages]
[lewis]
name = "Corey Lewis"
[lewis.emails]
lewis_email = "corey.lewis@data61.csiro.au"
[lewis.homepages]
[peters]
name = "Kirstin Peters"
[peters.emails]
peters_email = "kirstin.peters@tu-berlin.de"
[peters.homepages]
[ortner]
name = "Veronika Ortner"
[ortner.emails]
[ortner.homepages]
[fiedler]
name = "Ben Fiedler"
[fiedler.emails]
fiedler_email = "ben.fiedler@inf.ethz.ch"
[fiedler.homepages]
[becker]
name = "Heiko Becker"
[becker.emails]
becker_email = "hbecker@mpi-sws.org"
[becker.homepages]
[bracevac]
name = "Oliver Bračevac"
[bracevac.emails]
bracevac_email = "bracevac@st.informatik.tu-darmstadt.de"
[bracevac.homepages]
[bohrer]
name = "Rose Bohrer"
[bohrer.emails]
bohrer_email = "rose.bohrer.cs@gmail.com"
[bohrer.homepages]
[londono]
name = "Alejandro Gómez-Londoño"
[londono.emails]
londono_email = "alejandro.gomez@chalmers.se"
[londono.homepages]
[armstrong]
name = "Alasdair Armstrong"
[armstrong.emails]
[armstrong.homepages]
[glabbeek]
name = "Rob van Glabbeek"
[glabbeek.emails]
[glabbeek.homepages]
glabbeek_homepage = "http://theory.stanford.edu/~rvg/"
[jiangd]
name = "Dongchen Jiang"
[jiangd.emails]
jiangd_email = "dongchenjiang@googlemail.com"
[jiangd.homepages]
[meis]
name = "Rene Meis"
[meis.emails]
meis_email = "rene.meis@uni-muenster.de"
meis_email1 = "rene.meis@uni-due.de"
[meis.homepages]
[hofmann]
name = "Martin Hofmann"
[hofmann.emails]
[hofmann.homepages]
hofmann_homepage = "http://www.tcs.informatik.uni-muenchen.de/~mhofmann"
[kerber]
name = "Manfred Kerber"
[kerber.emails]
kerber_email = "mnfrd.krbr@gmail.com"
[kerber.homepages]
kerber_homepage = "http://www.cs.bham.ac.uk/~mmk"
[linker]
name = "Sven Linker"
[linker.emails]
linker_email = "s.linker@liverpool.ac.uk"
[linker.homepages]
[balbach]
name = "Frank J. Balbach"
[balbach.emails]
balbach_email = "frank-balbach@gmx.de"
[balbach.homepages]
[weber]
name = "Tjark Weber"
[weber.emails]
weber_email = "tjark.weber@it.uu.se"
[weber.homepages]
weber_homepage = "http://user.it.uu.se/~tjawe125/"
[hellauer]
name = "Fabian Hellauer"
[hellauer.emails]
hellauer_email = "hellauer@in.tum.de"
[hellauer.homepages]
[reiter]
name = "Markus Reiter"
[reiter.emails]
[reiter.homepages]
[herzberg]
name = "Michael Herzberg"
[herzberg.emails]
herzberg_email = "mail@michael-herzberg.de"
[herzberg.homepages]
herzberg_homepage = "http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg"
[overbeek]
name = "Roy Overbeek"
[overbeek.emails]
overbeek_email = "Roy.Overbeek@cwi.nl"
[overbeek.homepages]
[koerner]
name = "Stefan Körner"
[koerner.emails]
koerner_email = "s_koer03@uni-muenster.de"
[koerner.homepages]
[tan]
name = "Yong Kiam Tan"
[tan.emails]
tan_email = "yongkiat@cs.cmu.edu"
[tan.homepages]
tan_homepage = "https://www.cs.cmu.edu/~yongkiat/"
[esparza]
name = "Javier Esparza"
[esparza.emails]
[esparza.homepages]
esparza_homepage = "https://www7.in.tum.de/~esparza/"
[platzer]
name = "André Platzer"
[platzer.emails]
platzer_email = "aplatzer@cs.cmu.edu"
[platzer.homepages]
platzer_homepage = "https://www.cs.cmu.edu/~aplatzer/"
[matichuk]
name = "Daniel Matichuk"
[matichuk.emails]
[matichuk.homepages]
[rawson]
name = "Michael Rawson"
[rawson.emails]
rawson_email = "michaelrawson76@gmail.com"
rawson_email1 = "mr644@cam.ac.uk"
[rawson.homepages]
[bisping]
name = "Benjamin Bisping"
[bisping.emails]
bisping_email = "benjamin.bisping@campus.tu-berlin.de"
[bisping.homepages]
[sanan]
name = "David Sanan"
[sanan.emails]
sanan_email = "sanan@ntu.edu.sg"
[sanan.homepages]
[jungnickel]
name = "Tim Jungnickel"
[jungnickel.emails]
jungnickel_email = "tim.jungnickel@tu-berlin.de"
[jungnickel.homepages]
[ammer]
name = "Thomas Ammer"
[ammer.emails]
[ammer.homepages]
[mulligan]
name = "Dominic P. Mulligan"
[mulligan.emails]
mulligan_email = "dominic.p.mulligan@googlemail.com"
mulligan_email1 = "Dominic.Mulligan@arm.com"
[mulligan.homepages]
[georgescu]
name = "George Georgescu"
[georgescu.emails]
[georgescu.homepages]
[aissat]
name = "Romain Aissat"
[aissat.emails]
[aissat.homepages]
[gore]
name = "Rajeev Gore"
[gore.emails]
gore_email = "rajeev.gore@anu.edu.au"
[gore.homepages]
[gomes]
name = "Victor B. F. Gomes"
[gomes.emails]
gomes_email = "victor.gomes@cl.cam.ac.uk"
gomes_email2 = "victorborgesfg@gmail.com"
gomes_email4 = "vborgesferreiragomes1@sheffield.ac.uk"
[gomes.homepages]
gomes_homepage = "http://www.dcs.shef.ac.uk/~victor"
[trachtenherz]
name = "David Trachtenherz"
[trachtenherz.emails]
[trachtenherz.homepages]
[lohner]
name = "Denis Lohner"
[lohner.emails]
lohner_email = "denis.lohner@kit.edu"
[lohner.homepages]
lohner_homepage = "http://pp.ipd.kit.edu/person.php?id=88"
[richter]
name = "Stefan Richter"
[richter.emails]
richter_email = "richter@informatik.rwth-aachen.de"
[richter.homepages]
richter_homepage = "http://www-lti.informatik.rwth-aachen.de/~richter/"
[nemeti]
name = "István Németi"
[nemeti.emails]
[nemeti.homepages]
nemeti_homepage = "http://www.renyi.hu/~nemeti/"
[bentkamp]
name = "Alexander Bentkamp"
[bentkamp.emails]
bentkamp_email = "bentkamp@gmail.com"
bentkamp_email1 = "a.bentkamp@vu.nl"
[bentkamp.homepages]
bentkamp_homepage = "https://www.cs.vu.nl/~abp290/"
[zeyda]
name = "Frank Zeyda"
[zeyda.emails]
zeyda_email = "frank.zeyda@york.ac.uk"
[zeyda.homepages]
[tuerk]
name = "Thomas Tuerk"
[tuerk.emails]
[tuerk.homepages]
[ribeiro]
name = "Pedro Ribeiro"
[ribeiro.emails]
[ribeiro.homepages]
[raedle]
name = "Jonas Rädle"
[raedle.emails]
raedle_email = "jonas.raedle@gmail.com"
raedle_email1 = "jonas.raedle@tum.de"
[raedle.homepages]
[peltier]
name = "Nicolas Peltier"
[peltier.emails]
peltier_email = "Nicolas.Peltier@imag.fr"
[peltier.homepages]
peltier_homepage = "http://membres-lig.imag.fr/peltier/"
[kappelmann]
name = "Kevin Kappelmann"
[kappelmann.emails]
kappelmann_email = "kevin.kappelmann@tum.de"
[kappelmann.homepages]
kappelmann_homepage = "https://www21.in.tum.de/team/kappelmk/"
[hoelzl]
name = "Johannes Hölzl"
[hoelzl.emails]
hoelzl_email = "hoelzl@in.tum.de"
[hoelzl.homepages]
hoelzl_homepage = "http://home.in.tum.de/~hoelzl"
[ballarin]
name = "Clemens Ballarin"
[ballarin.emails]
ballarin_email = "ballarin@in.tum.de"
[ballarin.homepages]
ballarin_homepage = "http://www21.in.tum.de/~ballarin/"
[wu]
name = "Chunhan Wu"
[wu.emails]
[wu.homepages]
[paulson]
name = "Lawrence C. Paulson"
[paulson.emails]
paulson_email = "lp15@cam.ac.uk"
[paulson.homepages]
paulson_homepage = "https://www.cl.cam.ac.uk/~lp15/"
[paleo]
name = "Bruno Woltzenlogel Paleo"
[paleo.emails]
[paleo.homepages]
paleo_homepage = "http://www.logic.at/staff/bruno/"
[wagner]
name = "Max Wagner"
[wagner.emails]
wagner_email = "max@trollbu.de"
[wagner.homepages]
[lochbihler]
name = "Andreas Lochbihler"
[lochbihler.emails]
lochbihler_email = "andreas.lochbihler@digitalasset.com"
lochbihler_email1 = "mail@andreas-lochbihler.de"
[lochbihler.homepages]
lochbihler_homepage = "http://www.andreas-lochbihler.de/"
[porter]
name = "Benjamin Porter"
[porter.emails]
[porter.homepages]
[boehme]
name = "Sascha Böhme"
[boehme.emails]
boehme_email = "boehmes@in.tum.de"
[boehme.homepages]
boehme_homepage = "http://www21.in.tum.de/~boehmes/"
[hou]
name = "Zhe Hou"
[hou.emails]
hou_email = "zhe.hou@ntu.edu.sg"
[hou.homepages]
[mitchell]
name = "Neil Mitchell"
[mitchell.emails]
[mitchell.homepages]
[gay]
name = "Richard Gay"
[gay.emails]
gay_email = "gay@mais.informatik.tu-darmstadt.de"
[gay.homepages]
[oldenburg]
name = "Lennart Oldenburg"
[oldenburg.emails]
[oldenburg.homepages]
[lochmann]
name = "Alexander Lochmann"
[lochmann.emails]
lochmann_email = "alexander.lochmann@uibk.ac.at"
[lochmann.homepages]
[lim]
name = "Japheth Lim"
[lim.emails]
[lim.homepages]
[keinholz]
name = "Jonas Keinholz"
[keinholz.emails]
[keinholz.homepages]
[taylor]
name = "Ramsay G. Taylor"
[taylor.emails]
taylor_email = "r.g.taylor@sheffield.ac.uk"
[taylor.homepages]
[bauereiss]
name = "Thomas Bauereiss"
[bauereiss.emails]
bauereiss_email = "thomas@bauereiss.name"
[bauereiss.homepages]
[lee]
name = "Holden Lee"
[lee.emails]
lee_email = "holdenl@princeton.edu"
[lee.homepages]
[weerwag]
name = "Timmy Weerwag"
[weerwag.emails]
[weerwag.homepages]
[sudhof]
name = "Henry Sudhof"
[sudhof.emails]
sudhof_email = "hsudhof@cs.tu-berlin.de"
[sudhof.homepages]
[nedzelsky]
name = "Michael Nedzelsky"
[nedzelsky.emails]
nedzelsky_email = "MichaelNedzelsky@yandex.ru"
[nedzelsky.homepages]
[romanos]
name = "Ralph Romanos"
[romanos.emails]
romanos_email = "ralph.romanos@student.ecp.fr"
[romanos.homepages]
[doczkal]
name = "Christian Doczkal"
[doczkal.emails]
doczkal_email = "doczkal@ps.uni-saarland.de"
[doczkal.homepages]
[buyse]
name = "Maxime Buyse"
[buyse.emails]
buyse_email = "maxime.buyse@polytechnique.edu"
[buyse.homepages]
[guiol]
name = "Hervé Guiol"
[guiol.emails]
guiol_email = "herve.guiol@univ-grenoble-alpes.fr"
[guiol.homepages]
[brodmann]
name = "Paul-David Brodmann"
[brodmann.emails]
brodmann_email = "p.brodmann@tu-berlin.de"
[brodmann.homepages]
[moedersheim]
name = "Sebastian Mödersheim"
[moedersheim.emails]
moedersheim_email = "samo@dtu.dk"
[moedersheim.homepages]
moedersheim_homepage = "https://people.compute.dtu.dk/samo/"
[hu]
name = "Shuwei Hu"
[hu.emails]
hu_email = "shuwei.hu@tum.de"
[hu.homepages]
[wand]
name = "Daniel Wand"
[wand.emails]
wand_email = "dwand@mpi-inf.mpg.de"
[wand.homepages]
[velykis]
name = "Andrius Velykis"
[velykis.emails]
[velykis.homepages]
velykis_homepage = "http://andrius.velykis.lt"
[felgenhauer]
name = "Bertram Felgenhauer"
[felgenhauer.emails]
felgenhauer_email = "bertram.felgenhauer@uibk.ac.at"
felgenhauer_email1 = "int-e@gmx.de"
[felgenhauer.homepages]
[sauer]
name = "Jens Sauer"
[sauer.emails]
sauer_email = "sauer@mais.informatik.tu-darmstadt.de"
[sauer.homepages]
[dittmann]
name = "Christoph Dittmann"
[dittmann.emails]
dittmann_email = "isabelle@christoph-d.de"
[dittmann.homepages]
dittmann_homepage = "http://logic.las.tu-berlin.de/Members/Dittmann/"
[muendler]
name = "Niels Mündler"
[muendler.emails]
muendler_email = "n.muendler@tum.de"
[muendler.homepages]
[somogyi]
name = "Dániel Somogyi"
[somogyi.emails]
[somogyi.homepages]
[makarios]
name = "T. J. M. Makarios"
[makarios.emails]
makarios_email = "tjm1983@gmail.com"
[makarios.homepages]
[nishihara]
name = "Toshiaki Nishihara"
[nishihara.emails]
[nishihara.homepages]
[losa]
name = "Giuliano Losa"
[losa.emails]
losa_email = "giuliano.losa@epfl.ch"
losa_email1 = "giuliano@galois.com"
losa_email2 = "giuliano@losa.fr"
[losa.homepages]
[grov]
name = "Gudmund Grov"
[grov.emails]
grov_email = "ggrov@inf.ed.ac.uk"
[grov.homepages]
grov_homepage = "http://homepages.inf.ed.ac.uk/ggrov"
[bharadwaj]
name = "Abhijith Bharadwaj"
[bharadwaj.emails]
[bharadwaj.homepages]
[clouston]
name = "Ranald Clouston"
[clouston.emails]
clouston_email = "ranald.clouston@cs.au.dk"
[clouston.homepages]
[jaskelioff]
name = "Mauro Jaskelioff"
[jaskelioff.emails]
[jaskelioff.homepages]
jaskelioff_homepage = "http://www.fceia.unr.edu.ar/~mauro/"
[caminati]
name = "Marco B. Caminati"
[caminati.emails]
[caminati.homepages]
[bengtson]
name = "Jesper Bengtson"
[bengtson.emails]
[bengtson.homepages]
bengtson_homepage = "http://www.itu.dk/people/jebe"
[boutry]
name = "Pierre Boutry"
[boutry.emails]
boutry_email = "boutry@unistra.fr"
[boutry.homepages]
[sternagelt]
name = "Thomas Sternagel"
[sternagelt.emails]
[sternagelt.homepages]
[guerraoui]
name = "Rachid Guerraoui"
[guerraoui.emails]
guerraoui_email = "rachid.guerraoui@epfl.ch"
[guerraoui.homepages]
[dongol]
name = "Brijesh Dongol"
[dongol.emails]
dongol_email = "brijesh.dongol@brunel.ac.uk"
[dongol.homepages]
[tuong]
name = "Frédéric Tuong"
[tuong.emails]
tuong_email = "tuong@users.gforge.inria.fr"
tuong_email1 = "ftuong@lri.fr"
[tuong.homepages]
tuong_homepage = "https://www.lri.fr/~ftuong/"
[ullrich]
name = "Sebastian Ullrich"
[ullrich.emails]
ullrich_email = "sebasti@nullri.ch"
[ullrich.homepages]
[essmann]
name = "Robin Eßmann"
[essmann.emails]
essmann_email = "robin.essmann@tum.de"
[essmann.homepages]
[liu]
name = "Junyi Liu"
[liu.emails]
[liu.homepages]
[villadsen]
name = "Jørgen Villadsen"
[villadsen.emails]
villadsen_email = "jovi@dtu.dk"
[villadsen.homepages]
villadsen_homepage = "https://people.compute.dtu.dk/jovi/"
[fosters]
name = "Simon Foster"
[fosters.emails]
fosters_email = "simon.foster@york.ac.uk"
[fosters.homepages]
fosters_homepage = "https://www-users.cs.york.ac.uk/~simonf/"
[dubut]
name = "Jérémy Dubut"
[dubut.emails]
dubut_email = "dubut@nii.ac.jp"
[dubut.homepages]
dubut_homepage = "http://group-mmm.org/~dubut/"
[jiang]
name = "Nan Jiang"
[jiang.emails]
jiang_email = "nanjiang@whu.edu.cn"
[jiang.homepages]
[hetzl]
name = "Stefan Hetzl"
[hetzl.emails]
hetzl_email = "hetzl@logic.at"
[hetzl.homepages]
hetzl_homepage = "http://www.logic.at/people/hetzl/"
[parkinson]
name = "Matthew Parkinson"
[parkinson.emails]
[parkinson.homepages]
parkinson_homepage = "http://research.microsoft.com/people/mattpark/"
[maletzky]
name = "Alexander Maletzky"
[maletzky.emails]
maletzky_email = "alexander.maletzky@risc.jku.at"
maletzky_email1 = "alexander.maletzky@risc-software.at"
[maletzky.homepages]
maletzky_homepage = "https://risc.jku.at/m/alexander-maletzky/"
[keefe]
name = "Greg O'Keefe"
[keefe.emails]
[keefe.homepages]
keefe_homepage = "http://users.rsise.anu.edu.au/~okeefe/"
[brandt]
name = "Felix Brandt"
[brandt.emails]
[brandt.homepages]
brandt_homepage = "http://dss.in.tum.de/staff/brandt.html"
[blasum]
name = "Holger Blasum"
[blasum.emails]
blasum_email = "holger.blasum@sysgo.com"
[blasum.homepages]
[messner]
name = "Florian Messner"
[messner.emails]
messner_email = "florian.g.messner@uibk.ac.at"
[messner.homepages]
[diaz]
name = "Javier Díaz"
[diaz.emails]
diaz_email = "javier.diaz.manzi@gmail.com"
[diaz.homepages]
[prathamesh]
name = "T.V.H. Prathamesh"
[prathamesh.emails]
prathamesh_email = "prathamesh@imsc.res.in"
[prathamesh.homepages]
[nestmann]
name = "Uwe Nestmann"
[nestmann.emails]
[nestmann.homepages]
nestmann_homepage = "https://www.mtv.tu-berlin.de/nestmann/"
[siek]
name = "Jeremy Siek"
[siek.emails]
siek_email = "jsiek@indiana.edu"
[siek.homepages]
siek_homepage = "http://homes.soic.indiana.edu/jsiek/"
[stock]
name = "Benedikt Stock"
[stock.emails]
stock_email = "benedikt1999@freenet.de"
[stock.homepages]
[boyton]
name = "Andrew Boyton"
[boyton.emails]
boyton_email = "andrew.boyton@nicta.com.au"
[boyton.homepages]
[taha]
name = "Safouan Taha"
[taha.emails]
taha_email = "safouan.taha@lri.fr"
[taha.homepages]
[ghourabi]
name = "Fadoua Ghourabi"
[ghourabi.emails]
ghourabi_email = "fadouaghourabi@gmail.com"
[ghourabi.homepages]
[brinkop]
name = "Hauke Brinkop"
[brinkop.emails]
brinkop_email = "hauke.brinkop@googlemail.com"
[brinkop.homepages]
[neumann]
name = "René Neumann"
[neumann.emails]
neumann_email = "rene.neumann@in.tum.de"
[neumann.homepages]
[schmaltz]
name = "Julien Schmaltz"
[schmaltz.emails]
schmaltz_email = "Julien.Schmaltz@ou.nl"
[schmaltz.homepages]
[haslbeck]
name = "Max W. Haslbeck"
[haslbeck.emails]
haslbeck_email = "maximilian.haslbeck@uibk.ac.at"
haslbeck_email1 = "haslbecm@in.tum.de"
haslbeck_email2 = "max.haslbeck@gmx.de"
[haslbeck.homepages]
haslbeck_homepage = "http://cl-informatik.uibk.ac.at/users/mhaslbeck/"
[reynaud]
name = "Alban Reynaud"
[reynaud.emails]
[reynaud.homepages]
[boulanger]
name = "Frédéric Boulanger"
[boulanger.emails]
boulanger_email = "frederic.boulanger@centralesupelec.fr"
[boulanger.homepages]
[spasic]
name = "Mirko Spasić"
[spasic.emails]
spasic_email = "mirko@matf.bg.ac.rs"
[spasic.homepages]
[heller]
name = "Armin Heller"
[heller.emails]
[heller.homepages]
[watt]
name = "Conrad Watt"
[watt.emails]
watt_email = "caw77@cam.ac.uk"
[watt.homepages]
watt_homepage = "http://www.cl.cam.ac.uk/~caw77/"
[hayes]
name = "Ian J. Hayes"
[hayes.emails]
hayes_email = "ian.hayes@itee.uq.edu.au"
[hayes.homepages]
[haslbeckm]
name = "Maximilian P. L. Haslbeck"
[haslbeckm.emails]
haslbeckm_email = "haslbema@in.tum.de"
[haslbeckm.homepages]
haslbeckm_homepage = "http://in.tum.de/~haslbema/"
[bortin]
name = "Maksym Bortin"
[bortin.emails]
bortin_email = "maksym.bortin@nicta.com.au"
[bortin.homepages]
[klenze]
name = "Tobias Klenze"
[klenze.emails]
klenze_email = "tobias.klenze@inf.ethz.ch"
[klenze.homepages]
+[toth]
+name = "Balazs Toth"
+
+[toth.emails]
+toth_email = "balazs.toth@tum.de"
+
+[toth.homepages]
diff --git a/metadata/entries/Real_Time_Deque.toml b/metadata/entries/Real_Time_Deque.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Real_Time_Deque.toml
@@ -0,0 +1,30 @@
+title = "Real-Time Double-Ended Queue"
+date = 2022-06-23
+topics = [
+ "Computer science/Data structures",
+]
+abstract = """
+A double-ended queue (deque) is a queue where one
+can enqueue and dequeue at both ends. We define and verify the deque
+implementation by Chuang and Goldberg. It is purely
+functional and all operations run in constant time."""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.toth]
+email = "toth_email"
+
+[authors.nipkow]
+homepage = "nipkow_homepage"
+
+[contributors]
+
+[notify]
+nipkow = "nipkow_email"
+
+[history]
+
+[extra]
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,687 +1,688 @@
ADS_Functor
AI_Planning_Languages_Semantics
AODV
AVL-Trees
AWN
Abortable_Linearizable_Modules
Abs_Int_ITP2012
Abstract-Hoare-Logics
Abstract-Rewriting
Abstract_Completeness
Abstract_Soundness
Ackermanns_not_PR
Actuarial_Mathematics
Adaptive_State_Counting
Affine_Arithmetic
Aggregation_Algebras
Akra_Bazzi
Algebraic_Numbers
Algebraic_VCs
Allen_Calculus
Amicable_Numbers
Amortized_Complexity
AnselmGod
Applicative_Lifting
Approximation_Algorithms
Architectural_Design_Patterns
Aristotles_Assertoric_Syllogistic
Arith_Prog_Rel_Primes
ArrowImpossibilityGS
Attack_Trees
Auto2_HOL
Auto2_Imperative_HOL
AutoFocus-Stream
Automated_Stateful_Protocol_Verification
Automatic_Refinement
AxiomaticCategoryTheory
BDD
BD_Security_Compositional
BNF_CC
BNF_Operations
BTree
Banach_Steinhaus
Belief_Revision
Bell_Numbers_Spivey
BenOr_Kozen_Reif
Berlekamp_Zassenhaus
Bernoulli
Bertrands_Postulate
Bicategory
BinarySearchTree
Binding_Syntax_Theory
Binomial-Heaps
Binomial-Queues
BirdKMP
Blue_Eyes
Bondy
Boolean_Expression_Checkers
Bounded_Deducibility_Security
Buchi_Complementation
Budan_Fourier
Buffons_Needle
Buildings
BytecodeLogicJmlTypes
C2KA_DistributedSystems
CAVA_Automata
CAVA_LTL_Modelchecker
CCS
CISC-Kernel
CRDT
CSP_RefTK
CYK
CZH_Elementary_Categories
CZH_Foundations
CZH_Universal_Constructions
CakeML
CakeML_Codegen
Call_Arity
Card_Equiv_Relations
Card_Multisets
Card_Number_Partitions
Card_Partitions
Cartan_FP
Case_Labeling
Catalan_Numbers
Category
Category2
Category3
Cauchy
Cayley_Hamilton
Certification_Monads
Chandy_Lamport
Chord_Segments
Circus
Clean
Clique_and_Monotone_Circuits
ClockSynchInst
Closest_Pair_Points
CoCon
CoSMeDis
CoSMed
CofGroups
Coinductive
Coinductive_Languages
Collections
Combinable_Wands
Combinatorics_Words
Combinatorics_Words_Graph_Lemma
Combinatorics_Words_Lyndon
Comparison_Sort_Lower_Bound
Compiling-Exceptions-Correctly
Complete_Non_Orders
Completeness
Complex_Bounded_Operators
Complex_Geometry
Complx
ComponentDependencies
ConcurrentGC
ConcurrentIMP
Concurrent_Ref_Alg
Concurrent_Revisions
Conditional_Simplification
Conditional_Transfer_Rule
Consensus_Refined
Constructive_Cryptography
Constructive_Cryptography_CM
Constructor_Funs
Containers
CoreC++
Core_DOM
Core_SC_DOM
Correctness_Algebras
Cotangent_PFD_Formula
Count_Complex_Roots
CryptHOL
CryptoBasedCompositionalProperties
Cubic_Quartic_Equations
DFS_Framework
DOM_Components
DPT-SAT-Solver
DataRefinementIBP
Datatype_Order_Generator
Decl_Sem_Fun_PL
Decreasing-Diagrams
Decreasing-Diagrams-II
Dedekind_Real
Deep_Learning
Delta_System_Lemma
Density_Compiler
Dependent_SIFUM_Refinement
Dependent_SIFUM_Type_Systems
Depth-First-Search
Derangements
Deriving
Descartes_Sign_Rule
Design_Theory
Dict_Construction
Differential_Dynamic_Logic
Differential_Game_Logic
Digit_Expansions
Dijkstra_Shortest_Path
Diophantine_Eqns_Lin_Hom
Dirichlet_L
Dirichlet_Series
DiscretePricing
Discrete_Summation
DiskPaxos
Dominance_CHK
DPRM_Theorem
DynamicArchitectures
Dynamic_Tables
E_Transcendental
Echelon_Form
EdmondsKarp_Maxflow
Efficient-Mergesort
Elliptic_Curves_Group_Law
Encodability_Process_Calculi
Epistemic_Logic
Equivalence_Relation_Enumeration
Ergodic_Theory
Error_Function
Euler_MacLaurin
Euler_Partition
Eval_FO
Example-Submission
Extended_Finite_State_Machine_Inference
Extended_Finite_State_Machines
FFT
FLP
FOL-Fitting
FOL_Axiomatic
FOL_Harrison
FOL_Seq_Calc1
FOL_Seq_Calc2
FOL_Seq_Calc3
Factor_Algebraic_Polynomial
Factored_Transition_System_Bounding
Falling_Factorial_Sum
Farkas
FeatherweightJava
Featherweight_OCL
Fermat3_4
FileRefinement
FinFun
Finger-Trees
Finite-Map-Extras
Finite_Automata_HF
Finite_Fields
Finitely_Generated_Abelian_Groups
First_Order_Terms
First_Welfare_Theorem
Fishburn_Impossibility
Fisher_Yates
Fishers_Inequality
Flow_Networks
Floyd_Warshall
Flyspeck-Tame
FocusStreamsCaseStudies
Forcing
Formal_Puiseux_Series
Formal_SSA
Formula_Derivatives
Foundation_of_geometry
Fourier
FO_Theory_Rewriting
Free-Boolean-Algebra
Free-Groups
Frequency_Moments
Fresh_Identifiers
FunWithFunctions
FunWithTilings
Functional-Automata
Functional_Ordered_Resolution_Prover
Furstenberg_Topology
GPU_Kernel_PL
Gabow_SCC
GaleStewart_Games
Gale_Shapley
Game_Based_Crypto
Gauss-Jordan-Elim-Fun
Gauss_Jordan
Gauss_Sums
Gaussian_Integers
GenClock
General-Triangle
Generalized_Counting_Sort
Generic_Deriving
Generic_Join
GewirthPGCProof
Girth_Chromatic
GoedelGod
Goedel_HFSet_Semantic
Goedel_HFSet_Semanticless
Goedel_Incompleteness
Goodstein_Lambda
GraphMarkingIBP
Graph_Saturation
Graph_Theory
Green
Groebner_Bases
Groebner_Macaulay
Gromov_Hyperbolicity
Grothendieck_Schemes
Group-Ring-Module
HOL-CSP
HOLCF-Prelude
HRB-Slicing
Hahn_Jordan_Decomposition
Heard_Of
Hello_World
HereditarilyFinite
Hermite
Hermite_Lindemann
Hidden_Markov_Models
Higher_Order_Terms
Hoare_Time
Hood_Melville_Queue
HotelKeyCards
Huffman
Hybrid_Logic
Hybrid_Multi_Lane_Spatial_Logic
Hybrid_Systems_VCs
HyperCTL
Hyperdual
IEEE_Floating_Point
IFC_Tracking
IMAP-CRDT
IMO2019
IMP2
IMP2_Binary_Heap
IMP_Compiler
IP_Addresses
Imperative_Insertion_Sort
Impossible_Geometry
Incompleteness
Incredible_Proof_Machine
Independence_CH
Inductive_Confidentiality
Inductive_Inference
InfPathElimination
InformationFlowSlicing
InformationFlowSlicing_Inter
Integration
Interpolation_Polynomials_HOL_Algebra
Interpreter_Optimizations
Interval_Arithmetic_Word32
Intro_Dest_Elim
Iptables_Semantics
Irrational_Series_Erdos_Straus
Irrationality_J_Hancl
Irrationals_From_THEBOOK
IsaGeoCoq
Isabelle_C
Isabelle_Marries_Dirac
Isabelle_Meta_Model
IsaNet
Jacobson_Basic_Algebra
Jinja
JinjaDCI
JinjaThreads
JiveDataStoreModel
Jordan_Hoelder
Jordan_Normal_Form
KAD
KAT_and_DRA
KBPs
KD_Tree
Key_Agreement_Strong_Adversaries
Kleene_Algebra
Knights_Tour
Knot_Theory
Knuth_Bendix_Order
Knuth_Morris_Pratt
Koenigsberg_Friendship
Kruskal
Kuratowski_Closure_Complement
LLL_Basis_Reduction
LLL_Factorization
LOFT
LTL
LTL_Master_Theorem
LTL_Normal_Form
LTL_to_DRA
LTL_to_GBA
Lam-ml-Normalization
LambdaAuth
LambdaMu
Lambda_Free_EPO
Lambda_Free_KBOs
Lambda_Free_RPOs
Lambert_W
Landau_Symbols
Laplace_Transform
Latin_Square
LatticeProperties
Launchbury
Laws_of_Large_Numbers
Lazy-Lists-II
Lazy_Case
Lehmer
Lifting_Definition_Option
Lifting_the_Exponent
LightweightJava
LinearQuantifierElim
Linear_Inequalities
Linear_Programming
Linear_Recurrences
Liouville_Numbers
List-Index
List-Infinite
List_Interleaving
List_Inversions
List_Update
LocalLexing
Localization_Ring
Locally-Nameless-Sigma
Logging_Independent_Anonymity
Lowe_Ontological_Argument
Lower_Semicontinuous
Lp
LP_Duality
Lucas_Theorem
MDP-Algorithms
MDP-Rewards
MFMC_Countable
MFODL_Monitor_Optimized
MFOTL_Monitor
MSO_Regex_Equivalence
Markov_Models
Marriage
Mason_Stothers
Matrices_for_ODEs
Matrix
Matrix_Tensor
Matroids
Max-Card-Matching
Median_Method
Median_Of_Medians_Selection
Menger
Mereology
Mersenne_Primes
Metalogic_ProofChecker
MiniML
MiniSail
Minimal_SSA
Minkowskis_Theorem
Minsky_Machines
Modal_Logics_for_NTS
Modular_Assembly_Kit_Security
Modular_arithmetic_LLL_and_HNF_algorithms
Monad_Memo_DP
Monad_Normalisation
MonoBoolTranAlgebra
MonoidalCategory
Monomorphic_Monad
MuchAdoAboutTwo
Multiset_Ordering_NPC
Multi_Party_Computation
Multirelations
Myhill-Nerode
Name_Carrying_Type_Inference
Nash_Williams
Nat-Interval-Logic
Native_Word
Nested_Multisets_Ordinals
Network_Security_Policy_Verification
Neumann_Morgenstern_Utility
No_FTL_observers
Nominal2
Noninterference_CSP
Noninterference_Concurrent_Composition
Noninterference_Generic_Unwinding
Noninterference_Inductive_Unwinding
Noninterference_Ipurge_Unwinding
Noninterference_Sequential_Composition
NormByEval
Nullstellensatz
Octonions
OpSets
Open_Induction
Optics
Optimal_BST
Orbit_Stabiliser
Order_Lattice_Props
Ordered_Resolution_Prover
Ordinal
Ordinal_Partitions
Ordinals_and_Cardinals
Ordinary_Differential_Equations
PAC_Checker
Package_logic
PAL
PCF
PLM
POPLmark-deBruijn
PSemigroupsConvolution
Padic_Ints
Pairing_Heap
Paraconsistency
Parity_Game
Partial_Function_MR
Partial_Order_Reduction
Password_Authentication_Protocol
Pell
Perfect-Number-Thm
Perron_Frobenius
Physical_Quantities
Pi_Calculus
Pi_Transcendental
Planarity_Certificates
Pluennecke_Ruzsa_Inequality
Poincare_Bendixson
Poincare_Disc
Polynomial_Factorization
Polynomial_Interpolation
Polynomials
Pop_Refinement
Posix-Lexing
Possibilistic_Noninterference
Power_Sum_Polynomials
Pratt_Certificate
Prefix_Free_Code_Combinators
Presburger-Automata
Prim_Dijkstra_Simple
Prime_Distribution_Elementary
Prime_Harmonic_Series
Prime_Number_Theorem
Priority_Queue_Braun
Priority_Search_Trees
Probabilistic_Noninterference
Probabilistic_Prime_Tests
Probabilistic_System_Zoo
Probabilistic_Timed_Automata
Probabilistic_While
Program-Conflict-Analysis
Progress_Tracking
Projective_Geometry
Projective_Measurements
Promela
Proof_Strategy_Language
PropResPI
Propositional_Proof_Systems
Prpu_Maxflow
PseudoHoops
Psi_Calculi
Ptolemys_Theorem
Public_Announcement_Logic
QHLProver
QR_Decomposition
Quantales
Quasi_Borel_Spaces
Quaternions
Quick_Sort_Cost
RIPEMD-160-SPARK
ROBDD
RSAPSS
Ramsey-Infinite
Random_BSTs
Random_Graph_Subgraph_Threshold
Randomised_BSTs
Randomised_Social_Choice
Rank_Nullity_Theorem
Real_Impl
Real_Power
+Real_Time_Deque
Recursion-Addition
Recursion-Theory-I
Refine_Imperative_HOL
Refine_Monadic
RefinementReactive
Regex_Equivalence
Registers
Regression_Test_Selection
Regular-Sets
Regular_Algebras
Regular_Tree_Relations
Relation_Algebra
Relational-Incorrectness-Logic
Relational_Disjoint_Set_Forests
Relational_Forests
Relational_Method
Relational_Minimum_Spanning_Trees
Relational_Paths
Rep_Fin_Groups
ResiduatedTransitionSystem
Residuated_Lattices
Resolution_FOL
Rewrite_Properties_Reduction
Rewriting_Z
Ribbon_Proofs
Robbins-Conjecture
Robinson_Arithmetic
Root_Balanced_Tree
Roth_Arithmetic_Progressions
Routing
Roy_Floyd_Warshall
SATSolverVerification
SC_DOM_Components
SDS_Impossibility
SIFPL
SIFUM_Type_Systems
SPARCv8
Safe_Distance
Safe_OCL
Saturation_Framework
Saturation_Framework_Extensions
Schutz_Spacetime
Secondary_Sylow
Security_Protocol_Refinement
Selection_Heap_Sort
SenSocialChoice
Separata
Separation_Algebra
Separation_Logic_Imperative_HOL
SequentInvertibility
Shadow_DOM
Shadow_SC_DOM
Shivers-CFA
ShortestPath
Show
Sigma_Commit_Crypto
Signature_Groebner
Simpl
Simple_Firewall
Simplex
Simplicial_complexes_and_boolean_functions
SimplifiedOntologicalArgument
Skew_Heap
Skip_Lists
Slicing
Sliding_Window_Algorithm
Smith_Normal_Form
Smooth_Manifolds
Sophomores_Dream
Sort_Encodings
Source_Coding_Theorem
SpecCheck
Special_Function_Bounds
Splay_Tree
Sqrt_Babylonian
Stable_Matching
Statecharts
Stateful_Protocol_Composition_and_Typing
Stellar_Quorums
Stern_Brocot
Stewart_Apollonius
Stirling_Formula
Stochastic_Matrices
Stone_Algebras
Stone_Kleene_Relation_Algebras
Stone_Relation_Algebras
Store_Buffer_Reduction
Stream-Fusion
Stream_Fusion_Code
Strong_Security
Sturm_Sequences
Sturm_Tarski
Stuttering_Equivalence
Subresultants
Subset_Boolean_Algebras
SumSquares
Sunflowers
SuperCalc
Surprise_Paradox
Symmetric_Polynomials
Syntax_Independent_Logic
Szemeredi_Regularity
Szpilrajn
TESL_Language
TLA
Tail_Recursive_Functions
Tarskis_Geometry
Taylor_Models
Three_Circles
Timed_Automata
Topological_Semantics
Topology
TortoiseHare
Transcendence_Series_Hancl_Rucki
Transformer_Semantics
Transition_Systems_and_Automata
Transitive-Closure
Transitive-Closure-II
Transitive_Models
Treaps
Tree-Automata
Tree_Decomposition
Triangle
Trie
Twelvefold_Way
Tycon
Types_Tableaus_and_Goedels_God
Types_To_Sets_Extension
UPF
UPF_Firewall
UTP
Universal_Hash_Families
Universal_Turing_Machine
UpDown_Scheme
Valuation
Van_Emde_Boas_Trees
Van_der_Waerden
VectorSpace
VeriComp
Verified-Prover
Verified_SAT_Based_AI_Planning
VerifyThis2018
VerifyThis2019
Vickrey_Clarke_Groves
Virtual_Substitution
VolpanoSmith
VYDRA_MDL
WHATandWHERE_Security
WOOT_Strong_Eventual_Consistency
WebAssembly
Weight_Balanced_Trees
Weighted_Path_Order
Well_Quasi_Orders
Wetzels_Problem
Winding_Number_Eval
Word_Lib
WorkerWrapper
X86_Semantics
XML
Youngs_Inequality
ZFC_in_HOL
Zeta_3_Irrational
Zeta_Function
pGCL
diff --git a/thys/Real_Time_Deque/Big.thy b/thys/Real_Time_Deque/Big.thy
new file mode 100644
--- /dev/null
+++ b/thys/Real_Time_Deque/Big.thy
@@ -0,0 +1,121 @@
+section \Bigger End of Deque\
+
+theory Big
+imports Common
+begin
+
+text \\<^noindent> The bigger end of the deque during transformation can be in two phases:
+
+ \<^descr> \Reverse\: Using the \step\ function the originally contained elements, which will be kept in this end, are reversed.
+ \<^descr> \Common\: Specified in theory \Common\. Is used to reverse the elements from the previous phase again to get them in the original order.
+
+\<^noindent> Each phase contains a \current\ state, which holds the original elements of the deque end.
+\
+
+datatype (plugins del: size) 'a state =
+ Reverse "'a current" "'a stack" "'a list" nat
+ | Common "'a Common.state"
+
+text \\<^noindent> Functions:
+
+\<^descr> \step\: Executes one step of the transformation
+\<^descr> \size_new\: Returns the size that the deque end will have after the transformation is finished.
+\<^descr> \size\: Minimum of \size_new\ and the number of elements contained in the current state.
+\<^descr> \remaining_steps\: Returns how many steps are left until the transformation is finished.
+\<^descr> \list\: List abstraction of the elements which this end will contain after the transformation is finished
+\<^descr> \list_current\: List abstraction of the elements currently in this deque end.
+\
+
+fun list :: "'a state \ 'a list" where
+ "list (Common common) = Common.list common"
+| "list (Reverse (Current extra _ _ remained) big aux count) = (
+ let reversed = reverseN count (Stack.list big) aux in
+ extra @ (reverseN remained reversed [])
+ )"
+
+fun list_current :: "'a state \ 'a list" where
+ "list_current (Common common) = Common.list_current common"
+| "list_current (Reverse current _ _ _) = Current.list current"
+
+instantiation state ::(type) step
+begin
+
+fun step_state :: "'a state \ 'a state" where
+ "step (Common state) = Common (step state)"
+| "step (Reverse current _ aux 0) = Common (normalize (Copy current aux [] 0))"
+| "step (Reverse current big aux count) =
+ Reverse current (Stack.pop big) ((Stack.first big)#aux) (count - 1)"
+
+instance..
+end
+
+fun push :: "'a \ 'a state \ 'a state" where
+ "push x (Common state) = Common (Common.push x state)"
+| "push x (Reverse current big aux count) = Reverse (Current.push x current) big aux count"
+
+fun pop :: "'a state \ 'a * 'a state" where
+ "pop (Common state) = (let (x, state) = Common.pop state in (x, Common state))"
+| "pop (Reverse current big aux count) = (first current, Reverse (drop_first current) big aux count)"
+
+instantiation state ::(type) is_empty
+begin
+
+fun is_empty_state :: "'a state \ bool" where
+ "is_empty (Common state) = is_empty state"
+| "is_empty (Reverse current _ _ count) = (
+ case current of Current extra added old remained \
+ is_empty current \ remained \ count
+)"
+
+instance..
+end
+
+instantiation state ::(type) invar
+begin
+
+fun invar_state :: "'a state \ bool" where
+ "invar (Common state) \ invar state"
+| "invar (Reverse current big aux count) \ (
+ case current of Current extra added old remained \
+ invar current
+ \ List.length aux \ remained - count
+
+ \ count \ size big
+ \ Stack.list old = rev (take (size old) ((rev (Stack.list big)) @ aux))
+ \ take remained (Stack.list old) = rev (take remained (reverseN count (Stack.list big) aux))
+)"
+
+instance..
+end
+
+instantiation state ::(type) size
+begin
+
+fun size_state :: "'a state \ nat" where
+ "size (Common state) = size state"
+| "size (Reverse current _ _ _) = min (size current) (size_new current)"
+
+instance..
+end
+
+instantiation state ::(type) size_new
+begin
+
+fun size_new_state :: "'a state \ nat" where
+ "size_new (Common state) = size_new state"
+| "size_new (Reverse current _ _ _) = size_new current"
+
+instance..
+end
+
+instantiation state ::(type) remaining_steps
+begin
+
+fun remaining_steps_state :: "'a state \ nat" where
+ "remaining_steps (Common state) = remaining_steps state"
+| "remaining_steps (Reverse (Current _ _ _ remaining) _ _ count) = count + remaining + 1"
+
+instance..
+end
+
+end
\ No newline at end of file
diff --git a/thys/Real_Time_Deque/Big_Proof.thy b/thys/Real_Time_Deque/Big_Proof.thy
new file mode 100644
--- /dev/null
+++ b/thys/Real_Time_Deque/Big_Proof.thy
@@ -0,0 +1,332 @@
+section "Big Proofs"
+
+theory Big_Proof
+imports Big Common_Proof
+begin
+
+lemma step_list [simp]: "invar big \ list (step big) = list big"
+proof(induction big rule: step_state.induct)
+ case 1
+ then show ?case
+ by auto
+next
+ case 2
+ then show ?case
+ by(auto split: current.splits)
+next
+ case 3
+ then show ?case
+ by(auto simp: rev_take take_drop drop_Suc tl_take rev_drop split: current.splits)
+qed
+
+lemma step_list_current [simp]: "invar big \ list_current (step big) = list_current big"
+ by(induction big rule: step_state.induct)(auto split: current.splits)
+
+lemma push_list [simp]: "list (push x big) = x # list big"
+proof(induction x big rule: push.induct)
+ case (1 x state)
+ then show ?case
+ by auto
+next
+ case (2 x current big aux count)
+ then show ?case
+ by(induction x current rule: Current.push.induct) auto
+qed
+
+lemma list_Reverse: "\
+ 0 < size (Reverse current big aux count);
+ invar (Reverse current big aux count)
+\ \ first current # list (Reverse (drop_first current) big aux count) =
+ list (Reverse current big aux count)"
+proof(induction current rule: Current.pop.induct)
+ case (1 added old remained)
+ then have [simp]: "remained - Suc 0 < length (reverseN count (Stack.list big) aux)"
+ by(auto simp: le_diff_conv)
+
+ (* TODO: *)
+ then have "
+ \0 < size old; 0 < remained; added = 0; remained - count \ length aux; count \ size big;
+ Stack.list old =
+ rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big)));
+ take remained (rev (take (size old - size big) aux)) @
+ take (remained - min (length aux) (size old - size big))
+ (rev (take (size old) (rev (Stack.list big)))) =
+ rev (take (remained - count) aux) @ rev (take remained (rev (take count (Stack.list big))))\
+ \ hd (rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big)))) =
+ (rev (take count (Stack.list big)) @ aux) ! (remained - Suc 0)"
+ by (smt (verit) Suc_pred hd_drop_conv_nth hd_rev hd_take last_snoc length_rev length_take min.absorb2 rev_append reverseN_def size_list_length take_append take_hd_drop)
+
+ with 1 have [simp]: "Stack.first old = reverseN count (Stack.list big) aux ! (remained - Suc 0)"
+ by(auto simp: take_hd_drop first_hd)
+
+ from 1 show ?case
+ using reverseN_nth[of
+ "remained - Suc 0" "reverseN count (Stack.list big) aux" "Stack.first old" "[]"
+ ]
+ by auto
+next
+ case 2
+ then show ?case by auto
+qed
+
+lemma size_list [simp]: " \0 < size big; invar big; list big = []\ \ False"
+proof(induction big rule: list.induct)
+ case 1
+ then show ?case
+ using list_size by auto
+next
+ case 2
+ then show ?case
+ by (metis list.distinct(1) list_Reverse)
+qed
+
+lemma pop_list [simp]: "\0 < size big; invar big; Big.pop big = (x, big')\
+ \ x # list big' = list big"
+proof(induction big arbitrary: x rule: list.induct)
+ case 1
+ then show ?case
+ by(auto split: prod.splits)
+next
+ case 2
+ then show ?case
+ by (metis Big.pop.simps(2) list_Reverse prod.inject)
+qed
+
+lemma pop_list_tl: "\0 < size big; invar big; Big.pop big = (x, big')\
+ \ Big.list big' = tl (Big.list big)"
+ using pop_list cons_tl[of x "list big'" "list big"]
+ by force
+
+(* TODO: *)
+lemma invar_step: "invar (big :: 'a state) \ invar (step big)"
+proof(induction big rule: step_state.induct)
+ case 1
+ then show ?case
+ by(auto simp: invar_step)
+next
+ case (2 current big aux)
+
+ then obtain extra old remained where current:
+ "current = Current extra (length extra) old remained"
+ by(auto split: current.splits)
+
+ (* TODO: *)
+ with 2 have "\current = Current extra (length extra) old remained; remained \ length aux;
+ Stack.list old =
+ rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big)));
+ take remained (rev (take (size old - size big) aux)) @
+ take (remained - min (length aux) (size old - size big))
+ (rev (take (size old) (rev (Stack.list big)))) =
+ rev (take remained aux)\
+ \ remained \ size old"
+ by(metis length_rev length_take min.absorb_iff2 size_list_length take_append)
+
+ with 2 current have "remained - size old = 0"
+ by auto
+
+ with current 2 show ?case
+ by(auto simp: reverseN_drop drop_rev)
+next
+ case (3 current big aux count)
+ then have "0 < size big"
+ by(auto split: current.splits)
+
+ then have big_not_empty: "Stack.list big \ []"
+ by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
+
+ with 3 have a: "
+ rev (Stack.list big) @ aux =
+ rev (Stack.list (Stack.pop big)) @ Stack.first big # aux"
+ by(auto simp: rev_tl_hd first_hd split: current.splits)
+
+ from 3 have "0 < size big"
+ by(auto split: current.splits)
+
+ from 3 big_not_empty have "
+ reverseN (Suc count) (Stack.list big) aux =
+ reverseN count (Stack.list (Stack.pop big)) (Stack.first big # aux)"
+ using reverseN_tl_hd[of "Suc count" "Stack.list big" aux]
+ by(auto simp: Stack_Proof.list_not_empty split: current.splits)
+
+ with 3 a show ?case
+ by(auto split: current.splits)
+qed
+
+lemma invar_push: "invar big \ invar (push x big)"
+ by(induction x big rule: push.induct)(auto simp: invar_push split: current.splits)
+
+(* TODO: *)
+lemma invar_pop: "\
+ 0 < size big;
+ invar big;
+ pop big = (x, big')
+\ \ invar big'"
+proof(induction big arbitrary: x rule: pop.induct)
+ case (1 state)
+ then show ?case
+ by(auto simp: invar_pop split: prod.splits)
+next
+ case (2 current big aux count)
+ then show ?case
+ proof(induction current rule: Current.pop.induct)
+ case (1 added old remained)
+ have linarith: "\x y z. x - y \ z \ x - (Suc y) \ z"
+ by linarith
+
+ have a: " \remained \ count + length aux; 0 < remained; added = 0; x = Stack.first old;
+ big' = Reverse (Current [] 0 (Stack.pop old) (remained - Suc 0)) big aux count;
+ count \ size big; Stack.list old = rev aux @ Stack.list big;
+ take remained (rev aux) @ take (remained - length aux) (Stack.list big) =
+ drop (count + length aux - remained) (rev aux) @
+ drop (count - remained) (take count (Stack.list big));
+ \ size old \ length aux + size big\
+ \ tl (rev aux @ Stack.list big) = rev aux @ Stack.list big"
+ by (metis le_refl length_append length_rev size_list_length)
+
+ have b: "\remained \ length (reverseN count (Stack.list big) aux); 0 < size old;
+ 0 < remained; added = 0;
+ x = Stack.first old;
+ big' = Reverse (Current [] 0 (Stack.pop old) (remained - Suc 0)) big aux count;
+ remained - count \ length aux; count \ size big;
+ Stack.list old =
+ drop (length aux - (size old - size big)) (rev aux) @
+ drop (size big - size old) (Stack.list big);
+ take remained (drop (length aux - (size old - size big)) (rev aux)) @
+ take (remained + (length aux - (size old - size big)) - length aux)
+ (drop (size big - size old) (Stack.list big)) =
+ drop (length (reverseN count (Stack.list big) aux) - remained)
+ (rev (reverseN count (Stack.list big) aux))\
+ \ tl (drop (length aux - (size old - size big)) (rev aux) @
+ drop (size big - size old) (Stack.list big)) =
+ drop (length aux - (size old - Suc (size big))) (rev aux) @
+ drop (Suc (size big) - size old) (Stack.list big)"
+ apply(cases "size old - size big \ length aux"; cases "size old \ size big")
+ by(auto simp: tl_drop_2 Suc_diff_le le_diff_conv le_refl a)
+
+ from 1 have "remained \ length (reverseN count (Stack.list big) aux)"
+ by(auto)
+
+ with 1 show ?case
+ apply(auto simp: rev_take take_tl drop_Suc Suc_diff_le tl_drop linarith simp del: reverseN_def)
+ using b by simp
+ next
+ case (2 x xs added old remained)
+ then show ?case by auto
+ qed
+qed
+
+lemma push_list_current [simp]: "list_current (push x big) = x # list_current big"
+ by(induction x big rule: push.induct) auto
+
+lemma pop_list_current [simp]: "\invar big; 0 < size big; Big.pop big = (x, big')\
+ \ x # Big.list_current big' = Big.list_current big"
+proof(induction big arbitrary: x rule: pop.induct)
+ case (1 state)
+ then show ?case
+ by(auto simp: pop_list_current split: prod.splits)
+next
+ case (2 current big aux count)
+ then show ?case
+ proof(induction current rule: Current.pop.induct)
+ case (1 added old remained)
+
+ then have
+ "rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big))) \ []"
+ using
+ order_less_le_trans[of 0 "size old" "size big"]
+ order_less_le_trans[of 0 count "size big"]
+ by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
+
+ with 1 show ?case
+ by(auto simp: first_hd)
+ next
+ case (2 x xs added old remained)
+ then show ?case
+ by auto
+ qed
+qed
+
+lemma list_current_size: "\0 < size big; list_current big = []; invar big\ \ False"
+proof(induction big rule: list_current.induct)
+ case 1
+ then show ?case
+ using list_current_size
+ by simp
+next
+ case (2 current uu uv uw)
+ then show ?case
+ apply(cases current)
+ by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_empty)
+qed
+
+lemma step_size: "invar (big :: 'a state) \ size big = size (step big)"
+ by(induction big rule: step_state.induct)(auto split: current.splits)
+
+lemma size_empty: "\invar (big :: 'a state); size big = 0\ \ is_empty big"
+proof(induction big)
+ case Reverse
+ then show ?case
+ by(auto simp: min_def Stack_Proof.list_empty split: if_splits current.splits)
+next
+ case Common
+ then show ?case
+ by(auto simp: size_empty)
+qed
+
+lemma remaining_steps_step [simp]: "\invar (big :: 'a state); remaining_steps big > 0\
+ \ Suc (remaining_steps (step big)) = remaining_steps big"
+ by(induction big rule: step_state.induct)(auto split: current.splits)
+
+lemma remaining_steps_step_0 [simp]: "\invar (big :: 'a state); remaining_steps big = 0\
+ \ remaining_steps (step big) = 0"
+ by(induction big)(auto split: current.splits)
+
+lemma remaining_steps_push: "invar big \ remaining_steps (push x big) = remaining_steps big"
+ by(induction x big rule: push.induct)(auto split: current.splits)
+
+lemma remaining_steps_pop: "\invar big; 0 < size big; pop big = (x, big')\
+ \ remaining_steps big' \ remaining_steps big"
+proof(induction big rule: pop.induct)
+ case (1 state)
+ then show ?case
+ by(auto simp: remaining_steps_pop split: prod.splits)
+next
+ case (2 current big aux count)
+ then show ?case
+ by(induction current rule: Current.pop.induct) auto
+qed
+
+lemma size_push [simp]: "invar big \ size (push x big) = Suc (size big)"
+ by(induction x big rule: push.induct)(auto split: current.splits)
+
+lemma size_new_push [simp]: "invar big \ size_new (push x big) = Suc (size_new big)"
+ by(induction x big rule: Big.push.induct)(auto split: current.splits)
+
+lemma size_pop [simp]: "\invar big; 0 < size big; pop big = (x, big')\
+ \ Suc (size big') = size big"
+proof(induction big rule: pop.induct)
+ case 1
+ then show ?case
+ by(auto split: prod.splits)
+next
+ case (2 current big aux count)
+ then show ?case
+ by(induction current rule: Current.pop.induct) auto
+qed
+
+lemma size_new_pop [simp]: "\invar big; 0 < size_new big; pop big = (x, big')\
+ \ Suc (size_new big') = size_new big"
+proof(induction big rule: pop.induct)
+ case 1
+ then show ?case
+ by(auto split: prod.splits)
+next
+ case (2 current big aux count)
+ then show ?case
+ by(induction current rule: Current.pop.induct) auto
+qed
+
+lemma size_size_new: "\invar (big :: 'a state); 0 < size big\ \ 0 < size_new big"
+ by(induction big)(auto simp: size_size_new)
+
+end
diff --git a/thys/Real_Time_Deque/Common.thy b/thys/Real_Time_Deque/Common.thy
new file mode 100644
--- /dev/null
+++ b/thys/Real_Time_Deque/Common.thy
@@ -0,0 +1,150 @@
+section \Common\
+
+theory Common
+imports Current Idle
+begin
+
+text \
+\<^noindent> The last two phases of both deque ends during transformation:
+
+ \<^descr> \Copy\: Using the \step\ function the new elements of this deque end are brought back into the original order.
+ \<^descr> \Idle\: The transformation of the deque end is finished.
+
+\<^noindent> Each phase contains a \current\ state, that holds the original elements of the deque end.
+\
+
+datatype (plugins del: size)'a state =
+ Copy "'a current" "'a list" "'a list" nat
+ | Idle "'a current" "'a idle"
+
+text\
+\<^noindent> Functions:
+
+\<^descr> \push\, \pop\: Add and remove elements using the \current\ state.
+\<^descr> \list\: List abstraction of the elements which this end will contain after the transformation is finished
+\<^descr> \list_current\: List abstraction of the elements currently in this deque end.
+\<^descr> \step\: Executes one step of the transformation, while keeping the invariant.
+\<^descr> \remaining_steps\: Returns how many steps are left until the transformation is finished.
+\<^descr> \size_new\: Returns the size, that the deque end will have after the transformation is finished.
+\<^descr> \size\: Minimum of \size_new\ and the number of elements contained in the \current\ state.
+\
+(*
+fun reverseN :: "nat \ 'a list \ 'a list \ 'a list" where
+ "reverseN 0 xs acc = acc"
+| "reverseN n [] acc = acc"
+| "reverseN (Suc n) (x#xs) acc = reverseN n xs (x#acc)"
+*)
+definition reverseN where
+[simp]: "reverseN n xs acc \ rev (take n xs) @ acc"
+
+fun list :: "'a state \ 'a list" where
+ "list (Idle _ idle) = Idle.list idle"
+| "list (Copy (Current extra _ _ remained) old new moved)
+ = extra @ reverseN (remained - moved) old new"
+
+fun list_current :: "'a state \ 'a list" where
+ "list_current (Idle current _) = Current.list current"
+| "list_current (Copy current _ _ _) = Current.list current"
+
+(* TODO: Maybe inline function? *)
+fun normalize :: "'a state \ 'a state" where
+ "normalize (Copy current old new moved) = (
+ case current of Current extra added _ remained \
+ if moved \ remained
+ then Idle current (idle.Idle (Stack extra new) (added + moved))
+ else Copy current old new moved
+ )"
+| "normalize state = state"
+
+
+instantiation state ::(type) step
+begin
+
+fun step_state :: "'a state \ 'a state" where
+ "step (Idle current idle) = Idle current idle"
+| "step (Copy current aux new moved) = (
+ case current of Current _ _ _ remained \
+ normalize (
+ if moved < remained
+ then Copy current (tl aux) ((hd aux)#new) (moved + 1)
+ else Copy current aux new moved
+ )
+ )"
+
+instance..
+end
+
+fun push :: "'a \ 'a state \ 'a state" where
+ "push x (Idle current (idle.Idle stack stackSize)) =
+ Idle (Current.push x current) (idle.Idle (Stack.push x stack) (Suc stackSize))"
+| "push x (Copy current aux new moved) = Copy (Current.push x current) aux new moved"
+
+fun pop :: "'a state \ 'a * 'a state" where
+ "pop (Idle current idle) = (let (x, idle) = Idle.pop idle in (x, Idle (drop_first current) idle))"
+| "pop (Copy current aux new moved) =
+ (first current, normalize (Copy (drop_first current) aux new moved))"
+
+instantiation state ::(type) is_empty
+begin
+
+fun is_empty_state :: "'a state \ bool" where
+ "is_empty (Idle current idle) \ is_empty current \ is_empty idle"
+| "is_empty (Copy current _ _ _) \ is_empty current"
+
+instance..
+end
+
+instantiation state::(type) invar
+begin
+
+fun invar_state :: "'a state \ bool" where
+ "invar (Idle current idle) \
+ invar idle
+ \ invar current
+ \ size_new current = size idle
+ \ take (size idle) (Current.list current) =
+ take (size current) (Idle.list idle)"
+| "invar (Copy current aux new moved) \ (
+ case current of Current _ _ old remained \
+ moved < remained
+ \ moved = length new
+ \ remained \ length aux + moved
+ \ invar current
+ \ take remained (Stack.list old) = take (size old) (reverseN (remained - moved) aux new)
+ )"
+
+instance..
+end
+
+instantiation state::(type) size
+begin
+
+(* Use size for emptiness? *)
+fun size_state :: "'a state \ nat" where
+ "size (Idle current idle) = min (size current) (size idle)"
+| "size (Copy current _ _ _) = min (size current) (size_new current)"
+
+instance..
+end
+
+instantiation state::(type) size_new
+begin
+
+fun size_new_state :: "'a state \ nat" where
+ "size_new (Idle current _) = size_new current"
+| "size_new (Copy current _ _ _) = size_new current"
+
+instance..
+end
+
+instantiation state::(type) remaining_steps
+begin
+
+fun remaining_steps_state :: "'a state \ nat" where
+ "remaining_steps (Idle _ _) = 0"
+| "remaining_steps (Copy (Current _ _ _ remained) aux new moved) = remained - moved"
+
+instance..
+end
+
+end
diff --git a/thys/Real_Time_Deque/Common_Proof.thy b/thys/Real_Time_Deque/Common_Proof.thy
new file mode 100644
--- /dev/null
+++ b/thys/Real_Time_Deque/Common_Proof.thy
@@ -0,0 +1,484 @@
+section "Common Proofs"
+
+theory Common_Proof
+imports Common Idle_Proof Current_Proof
+begin
+
+lemma reverseN_drop: "reverseN n xs acc = drop (length xs - n) (rev xs) @ acc"
+ unfolding reverseN_def using rev_take by blast
+
+lemma reverseN_step: "xs \ [] \ reverseN n (tl xs) (hd xs # acc) = reverseN (Suc n) xs acc"
+ by (simp add: take_Suc)
+
+lemma reverseN_finish: "reverseN n [] acc = acc"
+ by (simp)
+
+lemma reverseN_tl_hd: "0 < n \ xs \ [] \ reverseN n xs ys = reverseN (n - (Suc 0)) (tl xs) (hd xs #ys)"
+ by (simp add: reverseN_step del: reverseN_def)
+
+lemma reverseN_nth: "n < length xs \ x = xs ! n \ x # reverseN n xs ys = reverseN (Suc n) xs ys"
+ by (simp add: take_Suc_conv_app_nth)
+
+lemma step_list [simp]: "invar common \ list (step common) = list common"
+proof(induction common rule: step_state.induct)
+ case (1 idle)
+ then show ?case by auto
+next
+ case (2 current aux new moved)
+
+ then show ?case
+ proof(cases current)
+ case (Current extra added old remained)
+
+ with 2 have aux_not_empty: "aux \ []"
+ by auto
+
+ from 2 Current show ?thesis
+ proof(cases "remained \ Suc moved")
+ case True
+
+ with 2 Current have "remained - length new = 1"
+ by auto
+
+ with True Current 2 aux_not_empty show ?thesis
+ by(auto simp: )
+ next
+ case False
+ with Current show ?thesis
+ by(auto simp: aux_not_empty reverseN_step Suc_diff_Suc simp del: reverseN_def)
+ qed
+ qed
+qed
+
+lemma step_list_current [simp]: "invar common \ list_current (step common) = list_current common"
+ by(cases common)(auto split: current.splits)
+
+lemma push_list [simp]: "list (push x common) = x # list common"
+proof(induction x common rule: push.induct)
+ case (1 x stack stackSize)
+ then show ?case
+ by auto
+next
+ case (2 x current aux new moved)
+ then show ?case
+ by(induction x current rule: Current.push.induct) auto
+qed
+
+lemma invar_step: "invar (common :: 'a state) \ invar (step common)"
+proof(induction "common" rule: invar_state.induct)
+ case (1 idle)
+ then show ?case
+ by auto
+next
+ case (2 current aux new moved)
+ then show ?case
+ proof(cases current)
+ case (Current extra added old remained)
+ then show ?thesis
+ proof(cases "aux = []")
+ case True
+ with 2 Current show ?thesis by auto
+ next
+ case False
+ note AUX_NOT_EMPTY = False
+
+ then show ?thesis
+ proof(cases "remained \ Suc (length new)")
+ case True
+ with 2 Current False
+ have "take (Suc (length new)) (Stack.list old) = take (size old) (hd aux # new)"
+ by(auto simp: le_Suc_eq take_Cons')
+
+ with 2 Current True show ?thesis
+ by auto
+ next
+ case False
+ with 2 Current AUX_NOT_EMPTY show ?thesis
+ by(auto simp: reverseN_step Suc_diff_Suc simp del: reverseN_def)
+ qed
+ qed
+ qed
+qed
+
+lemma invar_push: "invar common \ invar (push x common)"
+proof(induction x common rule: push.induct)
+ case (1 x current stack stackSize)
+ then show ?case
+ proof(induction x current rule: Current.push.induct)
+ case (1 x extra added old remained)
+ then show ?case
+ proof(induction x stack rule: Stack.push.induct)
+ case (1 x left right)
+ then show ?case by auto
+ qed
+ qed
+next
+ case (2 x current aux new moved)
+ then show ?case
+ proof(induction x current rule: Current.push.induct)
+ case (1 x extra added old remained)
+ then show ?case by auto
+ qed
+qed
+
+lemma invar_pop: "\
+ 0 < size common;
+ invar common;
+ pop common = (x, common')
+\ \ invar common'"
+proof(induction common arbitrary: x rule: pop.induct)
+ case (1 current idle)
+ then obtain idle' where idle: "Idle.pop idle = (x, idle')"
+ by(auto split: prod.splits)
+
+ obtain current' where current: "drop_first current = current'"
+ by auto
+
+ from 1 current idle show ?case
+ using Idle_Proof.size_pop[of idle x idle', symmetric]
+ size_new_pop[of current]
+ size_pop_sub[of current _ current']
+ by(auto simp: Idle_Proof.invar_pop invar_size_pop eq_snd_iff take_tl size_not_empty)
+next
+ case (2 current aux new moved)
+ then show ?case
+ proof(induction current rule: Current.pop.induct)
+ case (1 added old remained)
+ then show ?case
+ proof(cases "remained - Suc 0 \ length new")
+ case True
+
+ with 1 have [simp]:
+ "0 < size old"
+ "Stack.list old \ []"
+ "aux \ []"
+ "length new = remained - Suc 0"
+ by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
+
+ then have [simp]: "Suc 0 \ size old"
+ by linarith
+
+ from 1 have "0 < remained"
+ by auto
+
+ then have "take remained (Stack.list old)
+ = hd (Stack.list old) # take (remained - Suc 0) (tl (Stack.list old))"
+ by (metis Suc_pred \Stack.list old \ []\ list.collapse take_Suc_Cons)
+
+ with 1 True show ?thesis
+ using Stack_Proof.pop_list[of old]
+ by(auto simp: Stack_Proof.size_not_empty)
+ next
+ case False
+ with 1 have "remained - Suc 0 \ length aux + length new" by auto
+
+ with 1 False show ?thesis
+ using Stack_Proof.pop_list[of old]
+ apply(auto simp: Suc_diff_Suc take_tl Stack_Proof.size_not_empty tl_append_if)
+ by (simp add: Suc_diff_le rev_take tl_drop_2 tl_take)
+ qed
+ next
+ case (2 x xs added old remained)
+ then show ?case by auto
+ qed
+qed
+
+lemma push_list_current [simp]: "list_current (push x left) = x # list_current left"
+ by(induction x left rule: push.induct) auto
+
+lemma pop_list [simp]: "invar common \ 0 < size common \ pop common = (x, common') \
+ x # list common' = list common"
+proof(induction common arbitrary: x rule: pop.induct)
+ case 1
+ then show ?case
+ by(auto simp: size_not_empty split: prod.splits)
+next
+ case (2 current aux new moved)
+ then show ?case
+ proof(induction current rule: Current.pop.induct)
+ case (1 added old remained)
+ then show ?case
+ proof(cases "remained - Suc 0 \ length new")
+ case True
+
+ from 1 True have [simp]:
+ "aux \ []" "0 < remained"
+ "Stack.list old \ []" "remained - length new = 1"
+ by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
+
+ then have "take remained (Stack.list old) = hd aux # take (size old - Suc 0) new
+ \ Stack.first old = hd aux"
+ by (metis first_hd hd_take list.sel(1))
+
+ with 1 True take_hd[of aux] show ?thesis
+ by(auto simp: Suc_leI)
+ next
+ case False
+ then show ?thesis
+ proof(cases "remained - length new = length aux")
+ case True
+
+ then have length_minus_1: "remained - Suc (length new) = length aux - 1"
+ by simp
+
+ from 1 have not_empty: "0 < remained" "0 < size old" "aux \ []" "\ is_empty old"
+ by(auto simp: Stack_Proof.size_not_empty)
+
+ from 1 True not_empty have "take 1 (Stack.list old) = take 1 (rev aux)"
+ using take_1[of
+ remained
+ "size old"
+ "Stack.list old"
+ "(rev aux) @ take (size old + length new - remained) new"
+ ]
+ by(simp)
+
+ then have "[last aux] = [Stack.first old]"
+ using take_last first_take not_empty
+ by fastforce
+
+ then have "last aux = Stack.first old"
+ by auto
+
+ with 1 True False show ?thesis
+ using not_empty last_drop_rev[of aux]
+ by(auto simp: reverseN_drop length_minus_1 simp del: reverseN_def)
+ next
+ case False
+
+ with 1 have a: "take (remained - length new) aux \ []"
+ by auto
+
+ from 1 False have b: "\ is_empty old"
+ by(auto simp: Stack_Proof.size_not_empty)
+
+ from 1 have c: "remained - Suc (length new) < length aux"
+ by auto
+
+ from 1 have not_empty: "0 < remained" "0 < size old" "0 < remained - length new" "0 < length aux"
+ by auto
+
+ with False have "
+ take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new)
+ \ take (Suc 0) (Stack.list old) = take (Suc 0) (rev (take (remained - length new) aux))"
+ using take_1[of
+ remained
+ "size old"
+ "Stack.list old"
+ " (reverseN (remained - length new) aux new)"
+ ]
+ by(auto simp: not_empty Suc_le_eq)
+
+ with 1 False have "take 1 (Stack.list old) = take 1 (rev (take (remained - length new) aux))"
+ by auto
+
+ then have d: "[Stack.first old] = [last (take (remained - length new) aux)]"
+ using take_last first_take a b
+ by metis
+
+ have "last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux)
+ = rev (take (remained - length new) aux)"
+ using Suc_diff_Suc c not_empty
+ by (metis a drop_drop last_drop_rev plus_1_eq_Suc rev_take zero_less_diff)
+
+ with 1(1) 1(3) False not_empty d show ?thesis
+ by(cases "remained - length new = 1") (auto)
+ qed
+ qed
+ next
+ case 2
+ then show ?case by auto
+ qed
+qed
+
+lemma pop_list_current: "invar common \ 0 < size common \ pop common = (x, common')
+ \ x # list_current common' = list_current common"
+proof(induction common arbitrary: x rule: pop.induct)
+ case (1 current idle)
+ then show ?case
+ proof(induction idle rule: Idle.pop.induct)
+ case (1 stack stackSize)
+ then show ?case
+ proof(induction current rule: Current.pop.induct)
+ case (1 added old remained)
+ then have "Stack.first old = Stack.first stack"
+ using take_first[of old stack]
+ by auto
+
+ with 1 show ?case
+ by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty)
+ next
+ case (2 x xs added old remained)
+ then have "0 < size stack"
+ by auto
+
+ with Stack_Proof.size_not_empty Stack_Proof.list_not_empty
+ have not_empty: "\ is_empty stack" "Stack.list stack \ []"
+ by auto
+
+ with 2 have "hd (Stack.list stack) = x"
+ using take_hd'[of "Stack.list stack" x "xs @ Stack.list old"]
+ by auto
+
+ with 2 show ?case
+ using first_list[of stack] not_empty
+ by auto
+ qed
+ qed
+next
+ case (2 current)
+ then show ?case
+ proof(induction current rule: Current.pop.induct)
+ case (1 added old remained)
+ then have "\ is_empty old"
+ by(auto simp: Stack_Proof.size_not_empty)
+
+ with 1 show ?case
+ using first_pop
+ by(auto simp: Stack_Proof.list_not_empty)
+ next
+ case 2
+ then show ?case by auto
+ qed
+qed
+
+lemma list_current_size [simp]:
+ "\0 < size common; list_current common = []; invar common\ \ False"
+proof(induction common rule: invar_state.induct)
+ case 1
+ then show ?case
+ using list_size by auto
+next
+ case (2 current)
+ then have "invar current"
+ "Current.list current = []"
+ "0 < size current"
+ by(auto split: current.splits)
+
+ then show ?case using list_size by auto
+qed
+
+lemma list_size [simp]: "\0 < size common; list common = []; invar common\ \ False"
+proof(induction common rule: invar_state.induct)
+ case 1
+ then show ?case
+ using list_size Idle_Proof.size_empty
+ by auto
+next
+ case (2 current aux new moved)
+ then have "invar current"
+ "Current.list current = []"
+ "0 < size current"
+ by(auto split: current.splits)
+
+ then show ?case using list_size by auto
+qed
+
+lemma size_empty: "invar (common :: 'a state) \