diff --git a/metadata/topics.toml b/metadata/topics.toml
--- a/metadata/topics.toml
+++ b/metadata/topics.toml
@@ -1,603 +1,615 @@
 ["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".Algorithms."Randomized"]
 
 ["Computer science".Algorithms."Randomized".classification]
 acm.id = "10002950.10003648.10003671"
 acm.desc = "Mathematics of computing~Probabilistic algorithms"
 ams.id = "68W20"
 ams.hierarchy = [
   "Computer science",
   "Algorithms in computer science",
   "Randomized algorithms",
 ]
 
 ["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"
+acm.id = "10003752.10003790.10003806"
+acm.desc = "Theory of computation~Programming logic"
+ams.id = "68Q60"
+ams.hierarchy = [
+  "Computer science",
+  "Theory of computing",
+  "Specification and verification (program logics, model checking, etc.)"
+]
 
 ["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"
+ams.id = "94A60"
+ams.hierarchy = [
+  "Information and communication theory, circuits",
+  "Communication, information",
+  "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]
diff --git a/web/entries/CHERI-C_Memory_Model.html b/web/entries/CHERI-C_Memory_Model.html
--- a/web/entries/CHERI-C_Memory_Model.html
+++ b/web/entries/CHERI-C_Memory_Model.html
@@ -1,164 +1,164 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
   <meta charset="utf-8" />
   <meta http-equiv="X-UA-Compatible" content="IE=edge">
   <meta name="viewport" content="width=device-width, initial-scale=1"><title>A Formal CHERI-C Memory Model - Archive of Formal Proofs</title><meta name="description" content="In this work, we present a formal memory model that provides a memory semantics for CHERI-C programs with uncompressed capabilities in a &#39;purecap&#39;..."><meta property="og:title" content="A Formal CHERI-C Memory Model" />
 <meta property="og:description" content="" />
 <meta property="og:type" content="article" />
 <meta property="og:url" content="/entries/CHERI-C_Memory_Model.html" /><meta property="og:image" content="/images/afp.png"/><meta property="article:section" content="entries" />
 <meta property="article:published_time" content="2022-11-25T00:00:00+00:00" />
 <meta property="article:modified_time" content="2022-11-25T00:00:00+00:00" /><meta property="og:site_name" content="Archive of Formal Proofs" />
 
 <meta name="twitter:card" content="summary_large_image"/>
 <meta name="twitter:image" content="/images/afp.png"/>
 
 <meta name="twitter:title" content="A Formal CHERI-C Memory Model"/>
 <meta name="twitter:description" content=""/>
 
   
   <link rel="stylesheet" type="text/css" href="../css/front.min.css">
 
   <link rel="icon" href="../images/favicon.ico" type="image/icon">
     <script>
       MathJax = {
         tex: {
           inlineMath: [['$', '$'], ['\\(', '\\)']]
         },
         processEscapes: true,
         svg: {
           fontCache: 'global'
         }
       };
     </script>
     <script id="MathJax-script" async src="../js/mathjax/es5/tex-mml-chtml.js"></script>
   <script src="../js/entries.js"></script><script src="../js/obfuscate.js"></script>
   <script src="../js/flexsearch.bundle.js"></script>
   <script src="../js/scroll-spy.js"></script>
   <script src="../js/theory.js"></script>
   <script src="../js/util.js"></script><script src="../js/header-search.js"></script><script src="../js/search-autocomplete.js"></script>
 </head>
 
 
 <body class='mathjax_ignore '>
   <aside>
     <div id="menu-toggle">
   <input id="toggle" type="checkbox" />
   <label for="toggle">
     <span>menu</span>
     <img src="../images/menu.svg" alt="Menu" />
   </label>
 
   <a href="../" class='logo-link'>
     <img src="../images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
   </a>
 
   <a href="../search"><img src="../images/search.svg" alt="Search" /></a>
   <nav id="menu">
     <div>
       <a href="../" class='logo-link'>
         <img src="../images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
       </a>
       <ul>
         <a href="../"><li >Home</li></a>
         <a href="../topics/"><li >Topics</li></a>
         <a href="../download/"><li >Download</li></a>
         <a href="../help/"><li >Help</li></a>
         <a href="../submission/"><li >Submission</li></a>
         <a href="../statistics/"><li >Statistics</li></a>
         <a href="../about/"><li >About</li></a>
       </ul>
     </div>
   </nav>
 </div>
   </aside>
 
   <div
     class='content  entries'><header>
   <form autocomplete="off" action="../search">
     <div class='form-container'>
       <input id="search-input" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
       id="search-button" type="button"><img src="../images/search.svg" alt="Search" /></button>
       <datalist id="autocomplete">
       </datalist>
     </div>
   </form>
   <h1 >
     <span class='first'>A</span> <span class='first'>F</span>ormal <span class='first'>C</span><span class='first'>H</span><span class='first'>E</span><span class='first'>R</span><span class='first'>I</span>-<span class='first'>C</span> <span class='first'>M</span>emory <span class='first'>M</span>odel</h1>
   <div>
     
     <p><a href="../authors/park">Seung Hoon Park</a> <a href="https://www.cs.ox.ac.uk/people/simon.park/">🌐</a>
     </p>
     
     
     <p class="date">November 25, 2022</p>
     
   </div>
 </header><div><main><h3>Abstract</h3>
 
   <div class="abstract mathjax_process">In this work, we present a formal memory model that provides a memory semantics for CHERI-C programs with uncompressed capabilities in a 'purecap' environment. We present a CHERI-C memory model theory with properties suitable for verification and potentially other types of analyses. Our theory generates an OCaml executable instance of the memory model, which is then used to instantiate the parametric Gillian program analysis framework, enabling concrete execution of CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the correctness of our tool, and catch a good class of safety violations that the CHERI hardware might miss.</div>
 
   <h3>License</h3>
   <div><a href="https://isa-afp.org/LICENSE">BSD License</a></div><h3>Topics</h3>
   <ul><li><a href="../topics/computer-science/semantics-and-reasoning">Computer science/Semantics and reasoning</a></li></ul><h3>Related publications</h3>
   <ul><li>
-      Park, S. H., Pai, R., &amp; Melham, T. (2022). <i>A Formal CHERI-C Semantics for Verification</i> (Version 1). arXiv. https://doi.org/10.48550/ARXIV.2211.07511
+      Park, S. H., Pai, R., &amp; Melham, T. (2022). A Formal CHERI-C Semantics for Verification. <i>ArXiv</i>. https://doi.org/10.48550/ARXIV.2211.07511
     </li></ul>
   <h3>Session CHERI-C_Memory_Model</h3>
   <ul>
     <li><a href="../theories/cheri-c_memory_model/#Preliminary_Library">Preliminary_Library</a></li>
     <li><a href="../theories/cheri-c_memory_model/#CHERI_C_Concrete_Memory_Model">CHERI_C_Concrete_Memory_Model</a></li>
     <li><a href="../theories/cheri-c_memory_model/#CHERI_C_Global_Environment">CHERI_C_Global_Environment</a></li></ul><div class="flex-wrap">
   <div>
     <h3>Depends on</h3>
     <ul class="horizontal-list"><li><a href="../entries/Containers.html">Light-weight Containers</a></li><li><a href="../entries/Separation_Algebra.html">Separation Algebra</a></li><li><a href="../entries/Word_Lib.html">Finite Machine Word Library</a></li></ul>
   </div>
   
   </div>
 </main>
 
 <nav class='links'>
   <a class='popup-button' href="#cite-popup">Cite</a>
   <a class='popup-button' href="#download-popup">Download</a>
   <h4>PDFs</h4>
   <a href="https://www.isa-afp.org/browser_info/current/AFP/CHERI-C_Memory_Model/outline.pdf">Proof
     outline</a>
   <a href="https://www.isa-afp.org/browser_info/current/AFP/CHERI-C_Memory_Model/document.pdf">Proof
     document</a>
   <a href="https://www.isa-afp.org/browser_info/current/AFP/CHERI-C_Memory_Model/session_graph.pdf">Dependencies</a></nav>
 
 <div id="cite-popup" class="overlay">
   <a class="cancel" href="#"></a>
   <div class="popup">
     <h2>Cite</h2>
     <a class="close" href="#">&times;</a>
     <div>
       <p style="display:none;" id="bibtex-filename">CHERI-C_Memory_Model-AFP</p><pre id="copy-text">@article{CHERI-C_Memory_Model-AFP,
   author  = {Seung Hoon Park},
   title   = {A Formal CHERI-C Memory Model},
   journal = {Archive of Formal Proofs},
   month   = {November},
   year    = {2022},
   note    = {\url{https://isa-afp.org/entries/CHERI-C_Memory_Model.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }</pre>
       <button id="copy-bibtex">Copy</button> <a id="download-bibtex">Download</a>
     </div>
   </div>
 </div>
 
 <div id="download-popup" class="overlay">
   <a class="cancel" href="#"></a>
   <div class="popup">
     <h2>Download</h2>
     <a class="close" href="#">&times;</a>
     <a href="https://www.isa-afp.org/release//afp-CHERI-C_Memory_Model-current.tar.gz" download>Download latest</a>
     
   </div>
 </div>
     </div>
   </div>
 </body>
 
 </html>
\ No newline at end of file
diff --git a/web/entries/CommCSL.html b/web/entries/CommCSL.html
--- a/web/entries/CommCSL.html
+++ b/web/entries/CommCSL.html
@@ -1,171 +1,171 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
   <meta charset="utf-8" />
   <meta http-equiv="X-UA-Compatible" content="IE=edge">
   <meta name="viewport" content="width=device-width, initial-scale=1"><title>Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs - Archive of Formal Proofs</title><meta name="description" content="Information flow security ensures that the secret data manipulated by a program does not influence its observable output. Proving information flow security..."><meta property="og:title" content="Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs" />
 <meta property="og:description" content="" />
 <meta property="og:type" content="article" />
 <meta property="og:url" content="/entries/CommCSL.html" /><meta property="og:image" content="/images/afp.png"/><meta property="article:section" content="entries" />
 <meta property="article:published_time" content="2023-03-15T00:00:00+00:00" />
 <meta property="article:modified_time" content="2023-03-15T00:00:00+00:00" /><meta property="og:site_name" content="Archive of Formal Proofs" />
 
 <meta name="twitter:card" content="summary_large_image"/>
 <meta name="twitter:image" content="/images/afp.png"/>
 
 <meta name="twitter:title" content="Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs"/>
 <meta name="twitter:description" content=""/>
 
   
   <link rel="stylesheet" type="text/css" href="../css/front.min.css">
 
   <link rel="icon" href="../images/favicon.ico" type="image/icon">
     <script>
       MathJax = {
         tex: {
           inlineMath: [['$', '$'], ['\\(', '\\)']]
         },
         processEscapes: true,
         svg: {
           fontCache: 'global'
         }
       };
     </script>
     <script id="MathJax-script" async src="../js/mathjax/es5/tex-mml-chtml.js"></script>
   <script src="../js/entries.js"></script><script src="../js/obfuscate.js"></script>
   <script src="../js/flexsearch.bundle.js"></script>
   <script src="../js/scroll-spy.js"></script>
   <script src="../js/theory.js"></script>
   <script src="../js/util.js"></script><script src="../js/header-search.js"></script><script src="../js/search-autocomplete.js"></script>
 </head>
 
 
 <body class='mathjax_ignore '>
   <aside>
     <div id="menu-toggle">
   <input id="toggle" type="checkbox" />
   <label for="toggle">
     <span>menu</span>
     <img src="../images/menu.svg" alt="Menu" />
   </label>
 
   <a href="../" class='logo-link'>
     <img src="../images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
   </a>
 
   <a href="../search"><img src="../images/search.svg" alt="Search" /></a>
   <nav id="menu">
     <div>
       <a href="../" class='logo-link'>
         <img src="../images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
       </a>
       <ul>
         <a href="../"><li >Home</li></a>
         <a href="../topics/"><li >Topics</li></a>
         <a href="../download/"><li >Download</li></a>
         <a href="../help/"><li >Help</li></a>
         <a href="../submission/"><li >Submission</li></a>
         <a href="../statistics/"><li >Statistics</li></a>
         <a href="../about/"><li >About</li></a>
       </ul>
     </div>
   </nav>
 </div>
   </aside>
 
   <div
     class='content  entries'><header>
   <form autocomplete="off" action="../search">
     <div class='form-container'>
       <input id="search-input" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
       id="search-button" type="button"><img src="../images/search.svg" alt="Search" /></button>
       <datalist id="autocomplete">
       </datalist>
     </div>
   </form>
   <h1 >
     <span class='first'>F</span>ormalization of <span class='first'>C</span>omm<span class='first'>C</span><span class='first'>S</span><span class='first'>L</span>: <span class='first'>A</span> <span class='first'>R</span>elational <span class='first'>C</span>oncurrent <span class='first'>S</span>eparation <span class='first'>L</span>ogic for <span class='first'>P</span>roving <span class='first'>I</span>nformation <span class='first'>F</span>low <span class='first'>S</span>ecurity in <span class='first'>C</span>oncurrent <span class='first'>P</span>rograms</h1>
   <div>
     
     <p><a href="../authors/dardinier">Thibault Dardinier</a> <a class="obfuscated" data="eyJob3N0IjpbImluZiIsImV0aHoiLCJjaCJdLCJ1c2VyIjpbInRoaWJhdWx0IiwiZGFyZGluaWVyIl19">📧</a>
     </p>
     
     
     <p class="date">March 15, 2023</p>
     
   </div>
 </header><div><main><h3>Abstract</h3>
 
   <div class="abstract mathjax_process"><p>Information flow security ensures that the secret data manipulated by a program does not influence its observable output. Proving information flow security is especially challenging for concurrent programs, where operations on secret data may influence the execution time of a thread and, thereby, the interleaving between threads. Such internal timing channels may affect the observable outcome of a program even if an attacker does not observe execution times. Existing verification techniques for information flow security in concurrent programs attempt to prove that secret data does not influence the relative timing of threads. However, these techniques are often restrictive (for instance because they disallow branching on secret data) and make strong assumptions about the execution platform (ignoring caching, processor instructions with data-dependent execution time, and other common features that affect execution time).
 </p><p>
 In this entry, we formalize and prove the soundness of CommCSL, a novel relational concurrent separation logic for proving secure information flow in concurrent programs that lifts these restrictions and does not make any assumptions about timing behavior. The key idea is to prove that all mutating operations performed on shared data commute, such that different thread interleavings do not influence its final value. Crucially, commutativity is required only for an abstraction of the shared data that contains the information that will be leaked to a public output. Abstract commutativity is satisfied by many more operations than standard commutativity, which makes our technique widely applicable.</p></div>
 
   <h3>License</h3>
   <div><a href="https://isa-afp.org/LICENSE">BSD License</a></div><h3>Topics</h3>
   <ul><li><a href="../topics/computer-science/programming-languages/logics">Computer science/Programming languages/Logics</a></li><li><a href="../topics/computer-science/concurrency">Computer science/Concurrency</a></li><li><a href="../topics/computer-science/security">Computer science/Security</a></li></ul><h3>Related publications</h3>
   <ul><li>
-      Eilers, M., Dardinier, T., &amp; Müller, P. (2022). <i>CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity</i> (Version 1). arXiv. https://doi.org/10.48550/ARXIV.2211.08459
+      Eilers, M., Dardinier, T., &amp; Müller, P. (2022). <i>CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity</i> (Version 2). arXiv. https://doi.org/10.48550/ARXIV.2211.08459
     </li></ul>
   <h3>Session CommCSL</h3>
   <ul>
     <li><a href="../theories/commcsl/#PartialMap">PartialMap</a></li>
     <li><a href="../theories/commcsl/#PosRat">PosRat</a></li>
     <li><a href="../theories/commcsl/#FractionalHeap">FractionalHeap</a></li>
     <li><a href="../theories/commcsl/#StateModel">StateModel</a></li>
     <li><a href="../theories/commcsl/#Lang">Lang</a></li>
     <li><a href="../theories/commcsl/#CommCSL">CommCSL</a></li>
     <li><a href="../theories/commcsl/#AbstractCommutativity">AbstractCommutativity</a></li>
     <li><a href="../theories/commcsl/#Guards">Guards</a></li>
     <li><a href="../theories/commcsl/#Safety">Safety</a></li>
     <li><a href="../theories/commcsl/#Soundness">Soundness</a></li>
     <li><a href="../theories/commcsl/#NonInterference">NonInterference</a></li></ul><div class="flex-wrap">
   
   
   </div>
 </main>
 
 <nav class='links'>
   <a class='popup-button' href="#cite-popup">Cite</a>
   <a class='popup-button' href="#download-popup">Download</a>
   <h4>PDFs</h4>
   <a href="https://www.isa-afp.org/browser_info/current/AFP/CommCSL/outline.pdf">Proof
     outline</a>
   <a href="https://www.isa-afp.org/browser_info/current/AFP/CommCSL/document.pdf">Proof
     document</a>
   <a href="https://www.isa-afp.org/browser_info/current/AFP/CommCSL/session_graph.pdf">Dependencies</a></nav>
 
 <div id="cite-popup" class="overlay">
   <a class="cancel" href="#"></a>
   <div class="popup">
     <h2>Cite</h2>
     <a class="close" href="#">&times;</a>
     <div>
       <p style="display:none;" id="bibtex-filename">CommCSL-AFP</p><pre id="copy-text">@article{CommCSL-AFP,
   author  = {Thibault Dardinier},
   title   = {Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs},
   journal = {Archive of Formal Proofs},
   month   = {March},
   year    = {2023},
   note    = {\url{https://isa-afp.org/entries/CommCSL.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }</pre>
       <button id="copy-bibtex">Copy</button> <a id="download-bibtex">Download</a>
     </div>
   </div>
 </div>
 
 <div id="download-popup" class="overlay">
   <a class="cancel" href="#"></a>
   <div class="popup">
     <h2>Download</h2>
     <a class="close" href="#">&times;</a>
     <a href="https://www.isa-afp.org/release//afp-CommCSL-current.tar.gz" download>Download latest</a>
     
   </div>
 </div>
     </div>
   </div>
 </body>
 
 </html>
\ No newline at end of file
diff --git a/web/topics/computer-science/programming-languages/logics/index.html b/web/topics/computer-science/programming-languages/logics/index.html
--- a/web/topics/computer-science/programming-languages/logics/index.html
+++ b/web/topics/computer-science/programming-languages/logics/index.html
@@ -1,353 +1,353 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
   <meta charset="utf-8" />
   <meta http-equiv="X-UA-Compatible" content="IE=edge">
   <meta name="viewport" content="width=device-width, initial-scale=1"><title>Computer science/Programming languages/Logics - Archive of Formal Proofs</title><meta name="description" content="A collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle."><link rel="alternate" type="application/rss+xml" href="../../../../topics/computer-science/programming-languages/logics/index.xml" title="Archive of Formal Proofs" /><meta property="og:title" content="Computer science/Programming languages/Logics" />
 <meta property="og:description" content="A collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle." />
 <meta property="og:type" content="website" />
 <meta property="og:url" content="/topics/computer-science/programming-languages/logics/" /><meta property="og:image" content="/images/afp.png"/><meta property="og:site_name" content="Archive of Formal Proofs" />
 
 <meta name="twitter:card" content="summary_large_image"/>
 <meta name="twitter:image" content="/images/afp.png"/>
 
 <meta name="twitter:title" content="Computer science/Programming languages/Logics"/>
 <meta name="twitter:description" content="A collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle."/>
 
   
   <link rel="stylesheet" type="text/css" href="../../../../css/front.min.css">
 
   <link rel="icon" href="../../../../images/favicon.ico" type="image/icon"><script src="../../../../js/obfuscate.js"></script>
   <script src="../../../../js/flexsearch.bundle.js"></script>
   <script src="../../../../js/scroll-spy.js"></script>
   <script src="../../../../js/theory.js"></script>
   <script src="../../../../js/util.js"></script><script src="../../../../js/header-search.js"></script><script src="../../../../js/search-autocomplete.js"></script>
 </head>
 
 
 <body class='mathjax_ignore '>
   <aside>
     <div id="menu-toggle">
   <input id="toggle" type="checkbox" />
   <label for="toggle">
     <span>menu</span>
     <img src="../../../../images/menu.svg" alt="Menu" />
   </label>
 
   <a href="../../../../" class='logo-link'>
     <img src="../../../../images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
   </a>
 
   <a href="../../../../search"><img src="../../../../images/search.svg" alt="Search" /></a>
   <nav id="menu">
     <div>
       <a href="../../../../" class='logo-link'>
         <img src="../../../../images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
       </a>
       <ul>
         <a href="../../../../"><li >Home</li></a>
         <a href="../../../../topics/"><li >Topics</li></a>
         <a href="../../../../download/"><li >Download</li></a>
         <a href="../../../../help/"><li >Help</li></a>
         <a href="../../../../submission/"><li >Submission</li></a>
         <a href="../../../../statistics/"><li >Statistics</li></a>
         <a href="../../../../about/"><li >About</li></a>
       </ul>
     </div>
   </nav>
 </div>
   </aside>
 
   <div
     class='content '><header>
   <form autocomplete="off" action="../../../../search">
     <div class='form-container'>
       <input id="search-input" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
       id="search-button" type="button"><img src="../../../../images/search.svg" alt="Search" /></button>
       <datalist id="autocomplete">
       </datalist>
     </div>
   </form>
   <h1 >
     <span class='first'>C</span>omputer <span class='first'>S</span>cience/<span class='first'>P</span>rogramming <span class='first'>L</span>anguages/<span class='first'>L</span>ogics</h1>
   <div>
     
     
   </div>
-</header><div><h2>Subject Classification</h2><p>ACM: <a href="https://dl.acm.org/topic/ccs2012/10011007.10011006.10011008.10011009.10011015">Software and its engineering~Constraint and logic languages</a></p><h2 class="head">2023</h2><article class="entry">
+</header><div><h2>Subject Classification</h2><p>ACM: <a href="https://dl.acm.org/topic/ccs2012/10003752.10003790.10003806">Theory of computation~Programming logic</a></p><p>AMS: <a href="https://mathscinet.ams.org/mathscinet/msc/msc2020.html?t=68Q60">Computer science / Theory of computing / Specification and verification (program logics, model checking, etc.)</a></p><h2 class="head">2023</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/HyperHoareLogic.html">Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties</a></h5> <br>by <a href="../../../../authors/dardinier">Thibault Dardinier</a></div>
   <span class="date">
     Apr 03
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/CommCSL.html">Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs</a></h5> <br>by <a href="../../../../authors/dardinier">Thibault Dardinier</a></div>
   <span class="date">
     Mar 15
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Rensets.html">Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion</a></h5> <br>by <a href="../../../../authors/popescu">Andrei Popescu</a></div>
   <span class="date">
     Feb 28
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/HoareForDivergence.html">A Hoare Logic for Diverging Programs</a></h5> <br>by <a href="../../../../authors/pohjola">Johannes Åman Pohjola</a>, <a href="../../../../authors/myreen">Magnus O. Myreen</a> and <a href="../../../../authors/tanaka">Miki Tanaka</a></div>
   <span class="date">
     Jan 20
   </span>
 </article>
 
 
 <h2 class="head">2022</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Separation_Logic_Unbounded.html">Unbounded Separation Logic</a></h5> <br>by <a href="../../../../authors/dardinier">Thibault Dardinier</a></div>
   <span class="date">
     Sep 05
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Combinable_Wands.html">A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand</a></h5> <br>by <a href="../../../../authors/dardinier">Thibault Dardinier</a></div>
   <span class="date">
     May 30
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Package_logic.html">Formalization of a Framework for the Sound Automation of Magic Wands</a></h5> <br>by <a href="../../../../authors/dardinier">Thibault Dardinier</a></div>
   <span class="date">
     May 18
   </span>
 </article>
 
 
 <h2 class="head">2021</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Registers.html">Quantum and Classical Registers</a></h5> <br>by <a href="../../../../authors/unruh">Dominique Unruh</a></div>
   <span class="date">
     Oct 28
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Correctness_Algebras.html">Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations</a></h5> <br>by <a href="../../../../authors/guttmann">Walter Guttmann</a></div>
   <span class="date">
     Oct 12
   </span>
 </article>
 
 
 <h2 class="head">2020</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Relational-Incorrectness-Logic.html">An Under-Approximate Relational Logic</a></h5> <br>by <a href="../../../../authors/murray">Toby Murray</a></div>
   <span class="date">
     Mar 12
   </span>
 </article>
 
 
 <h2 class="head">2019</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Differential_Game_Logic.html">Differential Game Logic</a></h5> <br>by <a href="../../../../authors/platzer">André Platzer</a></div>
   <span class="date">
     Jun 03
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/QHLProver.html">Quantum Hoare Logic</a></h5> <br>by <a href="../../../../authors/liu">Junyi Liu</a>, <a href="../../../../authors/zhan">Bohua Zhan</a>, <a href="../../../../authors/wang">Shuling Wang</a>, <a href="../../../../authors/ying">Shenggang Ying</a>, <a href="../../../../authors/liut">Tao Liu</a>, <a href="../../../../authors/liy">Yangjia Li</a>, <a href="../../../../authors/yingm">Mingsheng Ying</a> and <a href="../../../../authors/zhann">Naijun Zhan</a></div>
   <span class="date">
     Mar 24
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/UTP.html">Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming</a></h5> <br>by <a href="../../../../authors/fosters">Simon Foster</a>, <a href="../../../../authors/zeyda">Frank Zeyda</a>, <a href="../../../../authors/nemouchi">Yakoub Nemouchi</a>, <a href="../../../../authors/ribeiro">Pedro Ribeiro</a> and <a href="../../../../authors/wolff">Burkhart Wolff</a></div>
   <span class="date">
     Feb 01
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/IMP2.html">IMP2 – Simple Program Verification in Isabelle/HOL</a></h5> <br>by <a href="../../../../authors/lammich">Peter Lammich</a> and <a href="../../../../authors/wimmer">Simon Wimmer</a></div>
   <span class="date">
     Jan 15
   </span>
 </article>
 
 
 <h2 class="head">2018</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Hoare_Time.html">Hoare Logics for Time Bounds</a></h5> <br>by <a href="../../../../authors/haslbeckm">Maximilian P. L. Haslbeck</a> and <a href="../../../../authors/nipkow">Tobias Nipkow</a></div>
   <span class="date">
     Feb 26
   </span>
 </article>
 
 
 <h2 class="head">2017</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Differential_Dynamic_Logic.html">Differential Dynamic Logic</a></h5> <br>by <a href="../../../../authors/bohrer">Rose Bohrer</a></div>
   <span class="date">
     Feb 13
   </span>
 </article>
 
 
 <h2 class="head">2016</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Complx.html">COMPLX: A Verification Framework for Concurrent Imperative Programs</a></h5> <br>by <a href="../../../../authors/amani">Sidney Amani</a>, <a href="../../../../authors/andronick">June Andronick</a>, <a href="../../../../authors/bortin">Maksym Bortin</a>, <a href="../../../../authors/lewis">Corey Lewis</a>, <a href="../../../../authors/rizkallah">Christine Rizkallah</a> and <a href="../../../../authors/tuongj">Joseph Tuong</a></div>
   <span class="date">
     Nov 29
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Separata.html">Separata: Isabelle tactics for Separation Algebra</a></h5> <br>by <a href="../../../../authors/hou">Zhe Hou</a>, <a href="../../../../authors/sanan">David Sanan</a>, <a href="../../../../authors/tiu">Alwen Tiu</a>, <a href="../../../../authors/gore">Rajeev Gore</a> and <a href="../../../../authors/clouston">Ranald Clouston</a></div>
   <span class="date">
     Nov 16
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/KAD.html">Kleene Algebras with Domain</a></h5> <br>by <a href="../../../../authors/gomes">Victor B. F. Gomes</a>, <a href="../../../../authors/guttmann">Walter Guttmann</a>, <a href="../../../../authors/hoefner">Peter Höfner</a>, <a href="../../../../authors/struth">Georg Struth</a> and <a href="../../../../authors/weber">Tjark Weber</a></div>
   <span class="date">
     Apr 12
   </span>
 </article>
 
 
 <h2 class="head">2015</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/ConcurrentIMP.html">Concurrent IMP</a></h5> <br>by <a href="../../../../authors/gammie">Peter Gammie</a></div>
   <span class="date">
     Apr 13
   </span>
 </article>
 
 
 <h2 class="head">2014</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/RefinementReactive.html">Formalization of Refinement Calculus for Reactive Systems</a></h5> <br>by <a href="../../../../authors/preoteasa">Viorel Preoteasa</a></div>
   <span class="date">
     Oct 08
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/KAT_and_DRA.html">Kleene Algebra with Tests and Demonic Refinement Algebras</a></h5> <br>by <a href="../../../../authors/armstrong">Alasdair Armstrong</a>, <a href="../../../../authors/gomes">Victor B. F. Gomes</a> and <a href="../../../../authors/struth">Georg Struth</a></div>
   <span class="date">
     Jan 23
   </span>
 </article>
 
 
 <h2 class="head">2013</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Automatic_Refinement.html">Automatic Data Refinement</a></h5> <br>by <a href="../../../../authors/lammich">Peter Lammich</a></div>
   <span class="date">
     Oct 02
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Ribbon_Proofs.html">Ribbon Proofs</a></h5> <br>by <a href="../../../../authors/wickerson">John Wickerson</a></div>
   <span class="date">
     Jan 19
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Kleene_Algebra.html">Kleene Algebra</a></h5> <br>by <a href="../../../../authors/armstrong">Alasdair Armstrong</a>, <a href="../../../../authors/struth">Georg Struth</a> and <a href="../../../../authors/weber">Tjark Weber</a></div>
   <span class="date">
     Jan 15
   </span>
 </article>
 
 
 <h2 class="head">2012</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Separation_Logic_Imperative_HOL.html">A Separation Logic Framework for Imperative HOL</a></h5> <br>by <a href="../../../../authors/lammich">Peter Lammich</a> and <a href="../../../../authors/meis">Rene Meis</a></div>
   <span class="date">
     Nov 14
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Separation_Algebra.html">Separation Algebra</a></h5> <br>by <a href="../../../../authors/klein">Gerwin Klein</a>, <a href="../../../../authors/kolanski">Rafal Kolanski</a> and <a href="../../../../authors/boyton">Andrew Boyton</a></div>
   <span class="date">
     May 11
   </span>
 </article>
 
 
 <h2 class="head">2011</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/TLA.html">A Definitional Encoding of TLA* in Isabelle/HOL</a></h5> <br>by <a href="../../../../authors/grov">Gudmund Grov</a> and <a href="../../../../authors/merz">Stephan Merz</a></div>
   <span class="date">
     Nov 19
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/MonoBoolTranAlgebra.html">Algebra of Monotonic Boolean Transformers</a></h5> <br>by <a href="../../../../authors/preoteasa">Viorel Preoteasa</a></div>
   <span class="date">
     Sep 22
   </span>
 </article>
 
 
 <h2 class="head">2010</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/DataRefinementIBP.html">Semantics and Data Refinement of Invariant Based Programs</a></h5> <br>by <a href="../../../../authors/preoteasa">Viorel Preoteasa</a> and <a href="../../../../authors/back">Ralph-Johan Back</a></div>
   <span class="date">
     May 28
   </span>
 </article>
 
 
 <h2 class="head">2008</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/BytecodeLogicJmlTypes.html">A Bytecode Logic for JML and Types</a></h5> <br>by <a href="../../../../authors/beringer">Lennart Beringer</a> and <a href="../../../../authors/hofmann">Martin Hofmann</a></div>
   <span class="date">
     Dec 12
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/SIFPL.html">Secure information flow and program logics</a></h5> <br>by <a href="../../../../authors/beringer">Lennart Beringer</a> and <a href="../../../../authors/hofmann">Martin Hofmann</a></div>
   <span class="date">
     Nov 10
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Simpl.html">A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment</a></h5> <br>by <a href="../../../../authors/schirmer">Norbert Schirmer</a></div>
   <span class="date">
     Feb 29
   </span>
 </article>
 
 
 <h2 class="head">2006</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Abstract-Hoare-Logics.html">Abstract Hoare Logics</a></h5> <br>by <a href="../../../../authors/nipkow">Tobias Nipkow</a></div>
   <span class="date">
     Aug 08
   </span>
 </article>
 
 
 
 
     </div>
   </div>
 </body>
 
 </html>
\ No newline at end of file
diff --git a/web/topics/computer-science/security/cryptography/index.html b/web/topics/computer-science/security/cryptography/index.html
--- a/web/topics/computer-science/security/cryptography/index.html
+++ b/web/topics/computer-science/security/cryptography/index.html
@@ -1,151 +1,151 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
   <meta charset="utf-8" />
   <meta http-equiv="X-UA-Compatible" content="IE=edge">
   <meta name="viewport" content="width=device-width, initial-scale=1"><title>Computer science/Security/Cryptography - Archive of Formal Proofs</title><meta name="description" content="A collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle."><link rel="alternate" type="application/rss+xml" href="../../../../topics/computer-science/security/cryptography/index.xml" title="Archive of Formal Proofs" /><meta property="og:title" content="Computer science/Security/Cryptography" />
 <meta property="og:description" content="A collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle." />
 <meta property="og:type" content="website" />
 <meta property="og:url" content="/topics/computer-science/security/cryptography/" /><meta property="og:image" content="/images/afp.png"/><meta property="og:site_name" content="Archive of Formal Proofs" />
 
 <meta name="twitter:card" content="summary_large_image"/>
 <meta name="twitter:image" content="/images/afp.png"/>
 
 <meta name="twitter:title" content="Computer science/Security/Cryptography"/>
 <meta name="twitter:description" content="A collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle."/>
 
   
   <link rel="stylesheet" type="text/css" href="../../../../css/front.min.css">
 
   <link rel="icon" href="../../../../images/favicon.ico" type="image/icon"><script src="../../../../js/obfuscate.js"></script>
   <script src="../../../../js/flexsearch.bundle.js"></script>
   <script src="../../../../js/scroll-spy.js"></script>
   <script src="../../../../js/theory.js"></script>
   <script src="../../../../js/util.js"></script><script src="../../../../js/header-search.js"></script><script src="../../../../js/search-autocomplete.js"></script>
 </head>
 
 
 <body class='mathjax_ignore '>
   <aside>
     <div id="menu-toggle">
   <input id="toggle" type="checkbox" />
   <label for="toggle">
     <span>menu</span>
     <img src="../../../../images/menu.svg" alt="Menu" />
   </label>
 
   <a href="../../../../" class='logo-link'>
     <img src="../../../../images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
   </a>
 
   <a href="../../../../search"><img src="../../../../images/search.svg" alt="Search" /></a>
   <nav id="menu">
     <div>
       <a href="../../../../" class='logo-link'>
         <img src="../../../../images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
       </a>
       <ul>
         <a href="../../../../"><li >Home</li></a>
         <a href="../../../../topics/"><li >Topics</li></a>
         <a href="../../../../download/"><li >Download</li></a>
         <a href="../../../../help/"><li >Help</li></a>
         <a href="../../../../submission/"><li >Submission</li></a>
         <a href="../../../../statistics/"><li >Statistics</li></a>
         <a href="../../../../about/"><li >About</li></a>
       </ul>
     </div>
   </nav>
 </div>
   </aside>
 
   <div
     class='content '><header>
   <form autocomplete="off" action="../../../../search">
     <div class='form-container'>
       <input id="search-input" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
       id="search-button" type="button"><img src="../../../../images/search.svg" alt="Search" /></button>
       <datalist id="autocomplete">
       </datalist>
     </div>
   </form>
   <h1 >
     <span class='first'>C</span>omputer <span class='first'>S</span>cience/<span class='first'>S</span>ecurity/<span class='first'>C</span>ryptography</h1>
   <div>
     
     
   </div>
-</header><div><h2>Subject Classification</h2><p>ACM: <a href="https://dl.acm.org/topic/ccs2012/10002978.10002979">Security and privacy~Cryptography</a></p><h2 class="head">2023</h2><article class="entry">
+</header><div><h2>Subject Classification</h2><p>ACM: <a href="https://dl.acm.org/topic/ccs2012/10002978.10002979">Security and privacy~Cryptography</a></p><p>AMS: <a href="https://mathscinet.ams.org/mathscinet/msc/msc2020.html?t=94A60">Information and communication theory, circuits / Communication, information / Cryptography</a></p><h2 class="head">2023</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/CVP_Hardness.html">Hardness of Lattice Problems</a></h5> <br>by <a href="../../../../authors/kreuzer">Katharina Kreuzer</a></div>
   <span class="date">
     Feb 02
   </span>
 </article>
 
 
 <h2 class="head">2021</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Constructive_Cryptography_CM.html">Constructive Cryptography in HOL: the Communication Modeling Aspect</a></h5> <br>by <a href="../../../../authors/lochbihler">Andreas Lochbihler</a> and <a href="../../../../authors/sefidgar">S. Reza Sefidgar</a></div>
   <span class="date">
     Mar 17
   </span>
 </article>
 
 
 <h2 class="head">2019</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Sigma_Commit_Crypto.html">Sigma Protocols and Commitment Schemes</a></h5> <br>by <a href="../../../../authors/butler">David Butler</a> and <a href="../../../../authors/lochbihler">Andreas Lochbihler</a></div>
   <span class="date">
     Oct 07
   </span>
 </article>
 
 
 <h2 class="head">2018</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Constructive_Cryptography.html">Constructive Cryptography in HOL</a></h5> <br>by <a href="../../../../authors/lochbihler">Andreas Lochbihler</a> and <a href="../../../../authors/sefidgar">S. Reza Sefidgar</a></div>
   <span class="date">
     Dec 17
   </span>
 </article>
 
 
 <h2 class="head">2017</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Game_Based_Crypto.html">Game-based cryptography in HOL</a></h5> <br>by <a href="../../../../authors/lochbihler">Andreas Lochbihler</a>, <a href="../../../../authors/sefidgar">S. Reza Sefidgar</a> and <a href="../../../../authors/bhatt">Bhargav Bhatt</a></div>
   <span class="date">
     May 05
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/CryptHOL.html">CryptHOL</a></h5> <br>by <a href="../../../../authors/lochbihler">Andreas Lochbihler</a></div>
   <span class="date">
     May 05
   </span>
 </article>
 <article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/Elliptic_Curves_Group_Law.html">The Group Law for Elliptic Curves</a></h5> <br>by <a href="../../../../authors/berghofer">Stefan Berghofer</a></div>
   <span class="date">
     Feb 28
   </span>
 </article>
 
 
 <h2 class="head">2005</h2><article class="entry">
   <div class="item-text">
     <h5><a class="title" href="../../../../entries/RSAPSS.html">SHA1, RSA, PSS and more</a></h5> <br>by <a href="../../../../authors/lindenberg">Christina Lindenberg</a> and <a href="../../../../authors/wirt">Kai Wirt</a></div>
   <span class="date">
     May 02
   </span>
 </article>
 
 
 
 
     </div>
   </div>
 </body>
 
 </html>
\ No newline at end of file