diff --git a/metadata/entries/BTree.toml b/metadata/entries/BTree.toml
--- a/metadata/entries/BTree.toml
+++ b/metadata/entries/BTree.toml
@@ -1,46 +1,47 @@
title = "A Verified Imperative Implementation of B-Trees"
date = 2021-02-24
topics = [
+ "Computer science/Data management systems",
"Computer science/Data structures",
]
abstract = """
In this work, we use the interactive theorem prover Isabelle/HOL to
verify an imperative implementation of the classical B-tree data
structure invented by Bayer and McCreight [ACM 1970]. The
implementation supports set membership, insertion and deletion queries with
efficient binary search for intra-node navigation. This is
accomplished by first specifying the structure abstractly in the
functional modeling language HOL and proving functional correctness.
Using manual refinement, we derive an imperative implementation in
Imperative/HOL. We show the validity of this refinement using the
separation logic utilities from the
Isabelle Refinement Framework . The code can be exported to
the programming languages SML, OCaml and Scala. We examine the runtime of all
operations indirectly by reproducing results of the logarithmic
relationship between height and the number of nodes. The results are
discussed in greater detail in the corresponding Bachelor's
Thesis."""
license = "bsd"
note = ""
[authors]
[authors.muendler]
email = "muendler_email"
[contributors]
[notify]
muendler = "muendler_email"
[history]
2021-05-02 = """
Add implementation and proof of correctness of imperative deletion operations.
Further add the option to export code to OCaml.
"""
[extra]
[related]
diff --git a/metadata/entries/Eval_FO.toml b/metadata/entries/Eval_FO.toml
--- a/metadata/entries/Eval_FO.toml
+++ b/metadata/entries/Eval_FO.toml
@@ -1,61 +1,62 @@
title = "First-Order Query Evaluation"
date = 2022-02-15
topics = [
+ "Computer science/Data management systems",
"Logic/General logic/Classical first-order logic",
]
abstract = """
We formalize first-order query evaluation over an infinite domain with
equality. We first define the syntax and semantics of first-order
logic with equality. Next we define a locale
eval_fo abstracting a representation of
a potentially infinite set of tuples satisfying a first-order query
over finite relations. Inside the locale, we define a function
eval checking if the set of tuples satisfying a
first-order query over a database (an interpretation of the
query's predicates) is finite (i.e., deciding relative
safety) and computing the set of satisfying tuples if it is
finite. Altogether the function eval solves
capturability (Avron and Hirshfeld, 1991) of
first-order logic with equality. We also use the function
eval to prove a code equation for the semantics of
first-order logic, i.e., the function checking if a first-order query
over a database is satisfied by a variable assignment.
We provide an
interpretation of the locale eval_fo
based on the approach by Ailamazyan et al. A core notion in the
interpretation is the active domain of a query and a database that
contains all domain elements that occur in the database or interpret
the query's constants. We prove the main theorem of Ailamazyan et
al. relating the satisfaction of a first-order query over an infinite
domain to the satisfaction of this query over a finite domain
consisting of the active domain and a few additional domain elements
(outside the active domain) whose number only depends on the query. In
our interpretation of the locale
eval_fo, we use a potentially higher
number of the additional domain elements, but their number still only
depends on the query and thus has no effect on the data complexity
(Vardi, 1982) of query evaluation. Our interpretation yields an
executable function eval. The
time complexity of eval on a query is linear in the
total number of tuples in the intermediate relations for the
subqueries. Specifically, we build a database index to evaluate a
conjunction. We also optimize the case of a negated subquery in a
conjunction. Finally, we export code for the infinite domain of
natural numbers."""
license = "bsd"
note = ""
[authors]
[authors.raszyk]
email = "raszyk_email"
[contributors]
[notify]
raszyk = "raszyk_email1"
[history]
[extra]
[related]
diff --git a/metadata/entries/Generic_Join.toml b/metadata/entries/Generic_Join.toml
--- a/metadata/entries/Generic_Join.toml
+++ b/metadata/entries/Generic_Join.toml
@@ -1,33 +1,34 @@
title = "Formalization of Multiway-Join Algorithms"
date = 2019-09-16
topics = [
+ "Computer science/Data management systems",
"Computer science/Algorithms",
]
abstract = """
Worst-case optimal multiway-join algorithms are recent seminal
achievement of the database community. These algorithms compute the
natural join of multiple relational databases and improve in the worst
case over traditional query plan optimizations of nested binary joins.
In 2014, Ngo, RĂ©,
and Rudra gave a unified presentation of different multi-way
join algorithms. We formalized and proved correct their \"Generic
Join\" algorithm and extended it to support negative joins."""
license = "bsd"
note = ""
[authors]
[authors.dardinier]
[contributors]
[notify]
dardinier = "dardinier_email"
traytel = "traytel_email1"
[history]
[extra]
[related]
diff --git a/metadata/entries/Safe_Range_RC.toml b/metadata/entries/Safe_Range_RC.toml
--- a/metadata/entries/Safe_Range_RC.toml
+++ b/metadata/entries/Safe_Range_RC.toml
@@ -1,61 +1,62 @@
title = "Making Arbitrary Relational Calculus Queries Safe-Range"
date = 2022-09-28
topics = [
+ "Computer science/Data management systems",
"Logic/General logic/Classical first-order logic",
]
abstract = """
The relational calculus (RC), i.e., first-order logic with equality
but without function symbols, is a concise, declarative database query
language. In contrast to relational algebra or SQL, which are the
traditional query languages of choice in the database community, RC
queries can evaluate to an infinite relation. Moreover, even in cases
where the evaluation result of an RC query would be finite it is not
clear how to efficiently compute it. Safe-range RC is an interesting
syntactic subclass of RC, because all safe-range queries evaluate to a
finite result and it is well-known
how to evaluate such queries by translating them to relational
algebra. We formalize and prove correct our
recent translation of an arbitrary RC query into a pair of
safe-range queries. Assuming an infinite domain, the two queries have
the following meaning: The first is closed and characterizes the
original query's relative safety, i.e., whether given a fixed
database (interpretation of atomic predicates with finite relations),
the original query evaluates to a finite relation. The second
safe-range query is equivalent to the original query, if the latter is
relatively safe. The formalization uses the Refinement Framework to
go from the non-deterministic algorithm described in the paper to a
deterministic, executable query translation. Our executable query
translation is a first step towards a verified tool that efficiently
evaluates arbitrary RC queries. This very problem is also solved by
the AFP entry Eval_FO
with a theoretically incomparable but practically worse time
complexity. (The latter is demonstrated by our
empirical evaluation.)"""
license = "bsd"
note = ""
[authors]
[authors.raszyk]
email = "raszyk_email"
[authors.traytel]
homepage = "traytel_homepage"
[contributors]
[notify]
raszyk = "raszyk_email1"
traytel = "traytel_email2"
[history]
[extra]
[related]
diff --git a/metadata/topics.toml b/metadata/topics.toml
--- a/metadata/topics.toml
+++ b/metadata/topics.toml
@@ -1,579 +1,591 @@
["Computer science"]
["Computer science".classification]
ams.id = "68"
ams.hierarchy = [
"Computer science",
]
["Computer science"."Artificial intelligence"]
["Computer science"."Artificial intelligence".classification]
acm.id = "10010147.10010178"
acm.desc = "Computing methodologies~Artificial intelligence"
ams.id = "68T"
ams.hierarchy = [
"Computer science",
"Artificial intelligence",
]
["Computer science"."Automata and formal languages"]
["Computer science"."Automata and formal languages".classification]
acm.id = "10003752.10003766"
acm.desc = "Theory of computation~Formal languages and automata theory"
ams.id = "68Q45"
ams.hierarchy = [
"Computer scienece",
"Theory of computing",
"Formal languages and automata",
]
["Computer science".Algorithms]
["Computer science".Algorithms.classification]
acm.id = "10003752.10003809"
acm.desc = "Theory of computation~Design and analysis of algorithms"
ams.id = "68W"
ams.hierarchy = [
"Computer science",
"Algorithms in computer science",
]
["Computer science".Algorithms.Graph]
["Computer science".Algorithms.Graph.classification]
acm.id = "10003752.10003809.10003635"
acm.desc = "Theory of computation~Graph algorithms analysis"
ams.id = "05C85"
ams.hierarchy = [
"Combinatorics",
"Graph theory",
"Graph algorithms",
]
["Computer science".Algorithms.Distributed]
["Computer science".Algorithms.Distributed.classification]
acm.id = "10003752.10003809.10010172"
acm.desc = "Theory of computation~Distributed algorithms"
ams.id = "68W15"
ams.hierarchy = [
"Computer science",
"Algorithms in computer science",
"Distributed algorithms",
]
["Computer science".Algorithms.Concurrent]
["Computer science".Algorithms.Concurrent.classification]
acm.id = "10003752.10003809.10011778"
acm.desc = "Theory of computation~Concurrent algorithms"
ams.id = "68W10"
ams.hierarchy = [
"Computer science",
"Algorithms in computer science",
"Parallel algorithms in computer science",
]
["Computer science".Algorithms.Online]
["Computer science".Algorithms.Online.classification]
acm.id = "10003752.10003809.10010047"
acm.desc = "Theory of computation~Online algorithms"
ams.id = "68W27"
ams.hierarchy = [
"Computer science",
"Algorithms in computer science",
"Online algorithms; streaming algorithms",
]
["Computer science".Algorithms.Geometry]
["Computer science".Algorithms.Geometry.classification]
["Computer science".Algorithms.Approximation]
["Computer science".Algorithms.Approximation.classification]
acm.id = "10003752.10003809.10003636"
acm.desc = "Theory of computation~Approximation algorithms analysis"
ams.id = "68W25"
ams.hierarchy = [
"Computer science",
"Algorithms in computer science",
"Approximation algorithms",
]
["Computer science".Algorithms.Mathematical]
["Computer science".Algorithms.Mathematical.classification]
["Computer science".Algorithms.Optimization]
["Computer science".Algorithms.Optimization.classification]
acm.id = "10003752.10003809.10003716"
acm.desc = "Theory of computation~Mathematical optimization"
["Computer science".Algorithms."Quantum computing"]
["Computer science".Algorithms."Quantum computing".classification]
ams.id = "68Q12"
ams.hierarchy = [
"Computer science",
"Theory of computing",
"Quantum algorithms and complexity in the theory of computing",
]
["Computer science".Concurrency]
["Computer science".Concurrency.classification]
acm.id = "10003752.10003753.10003761"
acm.desc = "Theory of computation~Concurrency"
ams.id = "68Q85"
ams.hierarchy = [
"Computer science",
"Theory of computing",
"Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)",
]
["Computer science".Concurrency."Process calculi"]
["Computer science".Concurrency."Process calculi".classification]
acm.id = "10003752.10003753.10003761.10003764"
acm.desc = "Theory of computation~Process calculi"
ams.id = "68Q85"
ams.hierarchy = [
"Computer science",
"Theory of computing",
"Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)",
]
+["Computer science"."Data management systems"]
+
+["Computer science"."Data management systems".classification]
+acm.id = "10002951.10002952"
+acm.desc = "Information systems~Data management systems"
+ams.id = "68P15"
+ams.hierarchy = [
+ "Computer science",
+ "Theory of data",
+ "Database theory",
+]
+
["Computer science"."Data structures"]
["Computer science"."Data structures".classification]
acm.id = "10003752.10003809.10010031"
acm.desc = "Theory of computation~Data structures design and analysis"
ams.id = "68P05"
ams.hierarchy = [
"Computer science",
"Theory of data",
"Data structures",
]
["Computer science"."Functional programming"]
["Computer science"."Functional programming".classification]
acm.id = "10011007.10011006.10011008.10011009.10011012"
acm.desc = "Software and its engineering~Functional languages"
ams.id = "68N18"
ams.hierarchy = [
"Computer science",
"Theory of software",
"Functional programming and lambda calculus",
]
["Computer science".Hardware]
["Computer science".Hardware.classification]
acm.id = "10010583"
acm.desc = "Hardware"
["Computer science"."Machine learning"]
["Computer science"."Machine learning".classification]
acm.id = "10010147.10010257"
acm.desc = "Computing methodologies~Machine learning"
["Computer science".Networks]
["Computer science".Networks.classification]
acm.id = "10003033"
acm.desc = "Networks"
["Computer science"."Programming languages"]
["Computer science"."Programming languages".classification]
acm.id = "10011007.10011006.10011008"
acm.desc = "Software and its engineering~General programming languages"
ams.id = "68N15"
ams.hierarchy = [
"Computer science",
"Theory of software",
"Theory of programming languages",
]
["Computer science"."Programming languages"."Language definitions"]
["Computer science"."Programming languages"."Language definitions".classification]
acm.id = "10011007.10011006.10011039"
acm.desc = "Software and its engineering~Formal language definitions"
["Computer science"."Programming languages"."Lambda calculi"]
["Computer science"."Programming languages"."Lambda calculi".classification]
acm.id = "10002950.10003714.10003732.10003733"
acm.desc = "Mathematics of computing~Lambda calculus"
ams.id = "68N18"
ams.hierarchy = [
"Computer science",
"Theory of software",
"Functional programming and lambda calculus",
]
["Computer science"."Programming languages"."Type systems"]
["Computer science"."Programming languages"."Type systems".classification]
acm.id = "10011007.10011006.10011008.10011024.10011028"
acm.desc = "Software and its engineering~Data types and structures"
["Computer science"."Programming languages".Logics]
["Computer science"."Programming languages".Logics.classification]
acm.id = "10011007.10011006.10011008.10011009.10011015"
acm.desc = "Software and its engineering~Constraint and logic languages"
["Computer science"."Programming languages".Compiling]
["Computer science"."Programming languages".Compiling.classification]
acm.id = "10011007.10011006.10011041"
acm.desc = "Software and its engineering~Compilers"
ams.id = "68N20"
ams.hierarchy = [
"Computer science",
"Theory of software",
"Theory of compilers and interpreters",
]
["Computer science"."Programming languages"."Static analysis"]
["Computer science"."Programming languages"."Static analysis".classification]
acm.id = "10011007.10010940.10010992.10010998.10011000"
acm.desc = "Software and its engineering~Automated static analysis"
["Computer science"."Programming languages".Misc]
["Computer science"."Programming languages".Misc.classification]
["Computer science".Security]
["Computer science".Security.classification]
acm.id = "10002978"
acm.desc = "Security and privacy"
ams.id = "68M25"
ams.hierarchy = [
"Computer science",
"Computer system organization",
"Computer security",
]
["Computer science".Security.Cryptography]
["Computer science".Security.Cryptography.classification]
acm.id = "10002978.10002979"
acm.desc = "Security and privacy~Cryptography"
["Computer science"."Semantics and reasoning"]
["Computer science"."Semantics and reasoning".classification]
acm.id = "10003752.10010124"
acm.desc = "Theory of computation~Semantics and reasoning"
ams.id = "68Q55"
ams.hierarchy = [
"Computer science",
"Theory of computing",
"Semantics in the theory of computing",
]
["Computer science"."System description languages"]
["Computer science"."System description languages".classification]
acm.id = "10011007.10011006.10011060"
acm.desc = "Software and its engineering~System description languages"
[Logic]
[Logic.classification]
acm.id = "10003752.10003790"
acm.desc = "Theory of computation~Logic"
ams.id = "03"
ams.hierarchy = [
"Mathematical logic and foundations",
]
[Logic."Philosophical aspects"]
[Logic."Philosophical aspects".classification]
ams.id = "03A"
ams.hierarchy = [
"Mathematical logic and foundations",
"Philosophical aspects of logic and foundations",
]
[Logic."General logic"]
[Logic."General logic".classification]
ams.id = "03B"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
]
[Logic."General logic"."Classical propositional logic"]
[Logic."General logic"."Classical propositional logic".classification]
ams.id = "03B05"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
"Classical propositional logic",
]
[Logic."General logic"."Classical first-order logic"]
[Logic."General logic"."Classical first-order logic".classification]
ams.id = "03B10"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
"Classical first-order logic",
]
[Logic."General logic"."Decidability of theories"]
[Logic."General logic"."Decidability of theories".classification]
ams.id = "03B25"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
"Decidability of theories and sets of sentences",
]
[Logic."General logic"."Mechanization of proofs"]
[Logic."General logic"."Mechanization of proofs".classification]
ams.id = "03B35"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
"Mechanization of proofs and logical operations",
]
[Logic."General logic"."Logics of knowledge and belief"]
[Logic."General logic"."Logics of knowledge and belief".classification]
acm.id = "10010147.10010178.10010187.10010198"
acm.desc = "Computing methodologies~Reasoning about belief and knowledge"
ams.id = "03B42"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
"Logics of knowledge and belief (including belief change)",
]
[Logic."General logic"."Temporal logic"]
[Logic."General logic"."Temporal logic".classification]
acm.id = "10003752.10003790.10003793"
acm.desc = "Theory of computation~Modal and temporal logics"
ams.id = "03B44"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
"Temporal logic",
]
[Logic."General logic"."Modal logic"]
[Logic."General logic"."Modal logic".classification]
acm.id = "10003752.10003790.10003793"
acm.desc = "Theory of computation~Modal and temporal logics"
ams.id = "03B45"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
"Modal logic (including the logic of norms)",
]
[Logic."General logic"."Paraconsistent logics"]
[Logic."General logic"."Paraconsistent logics".classification]
ams.id = "03B53"
ams.hierarchy = [
"Mathematical logic and foundations",
"General logic",
"Paraconsistent logics",
]
[Logic.Computability]
[Logic.Computability.classification]
acm.id = "10003752.10003753.10003754"
acm.desc = "Theory of computation~Computability"
ams.id = "03D"
ams.hierarchy = [
"Mathematical logic and foundations",
"Computability and recursion theory",
]
[Logic."Set theory"]
[Logic."Set theory".classification]
ams.id = "03E"
ams.hierarchy = [
"Mathematical logic and foundations",
"Set theory",
]
[Logic."Proof theory"]
[Logic."Proof theory".classification]
acm.id = "10003752.10003790.10003792"
acm.desc = "Theory of computation~Proof theory"
ams.id = "03F"
ams.hierarchy = [
"Mathematical logic and foundations",
"Proof theory and constructive mathematics",
]
[Logic.Rewriting]
[Logic.Rewriting.classification]
acm.id = "10003752.10003790.10003798"
acm.desc = "Theory of computation~Equational logic and rewriting"
[Mathematics]
[Mathematics.classification]
[Mathematics.Order]
[Mathematics.Order.classification]
ams.id = "06"
ams.hierarchy = [
"Order, lattices, ordered algebraic structures",
]
[Mathematics.Algebra]
[Mathematics.Algebra.classification]
ams.id = "08"
ams.hierarchy = [
"General algebraic systems",
]
[Mathematics.Analysis]
[Mathematics.Analysis.classification]
acm.id = "10002950.10003714"
acm.desc = "Mathematics of computing~Mathematical analysis"
[Mathematics."Measure and integration"]
[Mathematics."Measure and integration".classification]
ams.id = "28"
ams.hierarchy = [
"Measure and integration",
]
[Mathematics."Probability theory"]
[Mathematics."Probability theory".classification]
acm.id = "10002950.10003648"
acm.desc = "Mathematics of computing~Probability and statistics"
ams.id = "60"
ams.hierarchy = [
"Probability theory and stochastic processes",
]
[Mathematics."Number theory"]
[Mathematics."Number theory".classification]
ams.id = "11"
ams.hierarchy = [
"Number theory",
]
[Mathematics."Games and economics"]
[Mathematics."Games and economics".classification]
ams.id = "91"
ams.hierarchy = [
"Game theory, economics, finance, and other social and behavioral sciences",
]
[Mathematics.Geometry]
[Mathematics.Geometry.classification]
ams.id = "51"
ams.hierarchy = [
"Geometry",
]
[Mathematics.Topology]
[Mathematics.Topology.classification]
acm.id = "10002950.10003741.10003742"
acm.desc = "Mathematics of computing~Topology"
ams.id = "54"
ams.hierarchy = [
"General topology",
]
[Mathematics."Graph theory"]
[Mathematics."Graph theory".classification]
acm.id = "10002950.10003624.10003633"
acm.desc = "Mathematics of computing~Graph theory"
ams.id = "05C"
ams.hierarchy = [
"Combinatorics",
"Graph theory",
]
[Mathematics.Combinatorics]
[Mathematics.Combinatorics.classification]
acm.id = "10002950.10003624.10003625"
acm.desc = "Mathematics of computing~Combinatorics"
ams.id = "05"
ams.hierarchy = [
"Combinatorics",
]
[Mathematics."Category theory"]
[Mathematics."Category theory".classification]
ams.id = "18"
ams.hierarchy = [
"Category theory; homological algebra",
]
[Mathematics.Physics]
[Mathematics.Physics.classification]
ams.id = "00A79"
ams.hierarchy = [
"General and overarching topics; collections",
"General applied mathematics",
"Physics",
]
[Mathematics.Physics."Quantum information"]
[Mathematics.Physics."Quantum information".classification]
acm.id = "10003752.10003753.10003758.10010626"
acm.desc = "Theory of computation~Quantum information theory"
ams.id = "81P45"
ams.hierarchy = [
"Quantum theory",
"Foundations, quantum information and its processing, quantum axioms, and philosophy",
"Quantum information, communication, networks (quantum-theoretic aspects)",
]
[Mathematics.Misc]
[Mathematics.Misc.classification]
[Tools]
[Tools.classification]