diff --git a/metadata/entries/Fixed_Length_Vector.toml b/metadata/entries/Fixed_Length_Vector.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Fixed_Length_Vector.toml
@@ -0,0 +1,33 @@
+title = "Fixed-length vectors"
+date = 2023-08-14
+topics = [
+ "Computer science/Data structures",
+]
+abstract = """
+This theory introduces a type constructor for lists with known length, also known as \"vectors\". Those vectors are indexed with a numeral type that represent their length.
+
+This can be employed to avoid carrying around length constraints on lists. Instead, those constraints are discharged by the type checker.
+
+As compared to the vectors defined in the distribution, this definition can easily work with unit vectors. We exploit the fact that the cardinality of an infinite type is defined to be 0: thus any infinite length index type represents a unit vector.
+
+Furthermore, we set up automation and BNF support."""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.hupel]
+email = "hupel_email"
+
+[contributors]
+
+[notify]
+hupel = "hupel_email"
+
+[history]
+
+[extra]
+
+[related]
+dois = []
+pubs = []
diff --git a/web/authors/hupel/index.html b/web/authors/hupel/index.html
--- a/web/authors/hupel/index.html
+++ b/web/authors/hupel/index.html
@@ -1,186 +1,198 @@
C omputer S cience/D ata S tructures
-
\ No newline at end of file
diff --git a/web/topics/computer-science/data-structures/index.xml b/web/topics/computer-science/data-structures/index.xml
--- a/web/topics/computer-science/data-structures/index.xml
+++ b/web/topics/computer-science/data-structures/index.xml
@@ -1,595 +1,604 @@
Computer science/Data structures on Archive of Formal Proofs
/topics/computer-science/data-structures/
Recent content in Computer science/Data structures on Archive of Formal Proofs
Hugo -- gohugo.io
en-gb
-
+
Fixed-length vectors
+ /entries/Fixed_Length_Vector.html
+ Mon, 14 Aug 2023 00:00:00 +0000
+
+ /entries/Fixed_Length_Vector.html
+
+
+
+ -
Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML
/entries/Nano_JSON.html
Fri, 29 Jul 2022 00:00:00 +0000
/entries/Nano_JSON.html
-
Real-Time Double-Ended Queue
/entries/Real_Time_Deque.html
Thu, 23 Jun 2022 00:00:00 +0000
/entries/Real_Time_Deque.html
-
A Combinator Library for Prefix-Free Codes
/entries/Prefix_Free_Code_Combinators.html
Fri, 08 Apr 2022 00:00:00 +0000
/entries/Prefix_Free_Code_Combinators.html
-
van Emde Boas Trees
/entries/Van_Emde_Boas_Trees.html
Tue, 23 Nov 2021 00:00:00 +0000
/entries/Van_Emde_Boas_Trees.html
-
Fresh identifiers
/entries/Fresh_Identifiers.html
Mon, 16 Aug 2021 00:00:00 +0000
/entries/Fresh_Identifiers.html
-
A Verified Imperative Implementation of B-Trees
/entries/BTree.html
Wed, 24 Feb 2021 00:00:00 +0000
/entries/BTree.html
-
Hood-Melville Queue
/entries/Hood_Melville_Queue.html
Mon, 18 Jan 2021 00:00:00 +0000
/entries/Hood_Melville_Queue.html
-
Finite Map Extras
/entries/Finite-Map-Extras.html
Mon, 12 Oct 2020 00:00:00 +0000
/entries/Finite-Map-Extras.html
-
A Formal Model of the Document Object Model with Shadow Roots
/entries/Shadow_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/Shadow_DOM.html
-
A Formal Model of the Safely Composable Document Object Model with Shadow Roots
/entries/Shadow_SC_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/Shadow_SC_DOM.html
-
A Formalization of Safely Composable Web Components
/entries/SC_DOM_Components.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/SC_DOM_Components.html
-
A Formalization of Web Components
/entries/DOM_Components.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/DOM_Components.html
-
The Safely Composable DOM
/entries/Core_SC_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/Core_SC_DOM.html
-
Relational Disjoint-Set Forests
/entries/Relational_Disjoint_Set_Forests.html
Wed, 26 Aug 2020 00:00:00 +0000
/entries/Relational_Disjoint_Set_Forests.html
-
Authenticated Data Structures As Functors
/entries/ADS_Functor.html
Thu, 16 Apr 2020 00:00:00 +0000
/entries/ADS_Functor.html
-
Skip Lists
/entries/Skip_Lists.html
Thu, 09 Jan 2020 00:00:00 +0000
/entries/Skip_Lists.html
-
Interval Arithmetic on 32-bit Words
/entries/Interval_Arithmetic_Word32.html
Wed, 27 Nov 2019 00:00:00 +0000
/entries/Interval_Arithmetic_Word32.html
-
Priority Search Trees
/entries/Priority_Search_Trees.html
Tue, 25 Jun 2019 00:00:00 +0000
/entries/Priority_Search_Trees.html
-
Binary Heaps for IMP2
/entries/IMP2_Binary_Heap.html
Thu, 13 Jun 2019 00:00:00 +0000
/entries/IMP2_Binary_Heap.html
-
Multidimensional Binary Search Trees
/entries/KD_Tree.html
Thu, 30 May 2019 00:00:00 +0000
/entries/KD_Tree.html
-
A Formal Model of the Document Object Model
/entries/Core_DOM.html
Wed, 26 Dec 2018 00:00:00 +0000
/entries/Core_DOM.html
-
Verifying Imperative Programs using Auto2
/entries/Auto2_Imperative_HOL.html
Fri, 21 Dec 2018 00:00:00 +0000
/entries/Auto2_Imperative_HOL.html
-
Deriving generic class instances for datatypes
/entries/Generic_Deriving.html
Tue, 06 Nov 2018 00:00:00 +0000
/entries/Generic_Deriving.html
-
Randomised Binary Search Trees
/entries/Randomised_BSTs.html
Fri, 19 Oct 2018 00:00:00 +0000
/entries/Randomised_BSTs.html
-
Optimal Binary Search Trees
/entries/Optimal_BST.html
Sun, 27 May 2018 00:00:00 +0000
/entries/Optimal_BST.html
-
OpSets: Sequential Specifications for Replicated Datatypes
/entries/OpSets.html
Thu, 10 May 2018 00:00:00 +0000
/entries/OpSets.html
-
Weight-Balanced Trees
/entries/Weight_Balanced_Trees.html
Tue, 13 Mar 2018 00:00:00 +0000
/entries/Weight_Balanced_Trees.html
-
Treaps
/entries/Treaps.html
Tue, 06 Feb 2018 00:00:00 +0000
/entries/Treaps.html
-
Taylor Models
/entries/Taylor_Models.html
Mon, 08 Jan 2018 00:00:00 +0000
/entries/Taylor_Models.html
-
The IMAP CmRDT
/entries/IMAP-CRDT.html
Thu, 09 Nov 2017 00:00:00 +0000
/entries/IMAP-CRDT.html
-
Root-Balanced Tree
/entries/Root_Balanced_Tree.html
Sun, 20 Aug 2017 00:00:00 +0000
/entries/Root_Balanced_Tree.html
-
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
/entries/CRDT.html
Fri, 07 Jul 2017 00:00:00 +0000
/entries/CRDT.html
-
Expected Shape of Random Binary Search Trees
/entries/Random_BSTs.html
Tue, 04 Apr 2017 00:00:00 +0000
/entries/Random_BSTs.html
-
The Imperative Refinement Framework
/entries/Refine_Imperative_HOL.html
Mon, 08 Aug 2016 00:00:00 +0000
/entries/Refine_Imperative_HOL.html
-
Pairing Heap
/entries/Pairing_Heap.html
Thu, 14 Jul 2016 00:00:00 +0000
/entries/Pairing_Heap.html
-
Finite Machine Word Library
/entries/Word_Lib.html
Thu, 09 Jun 2016 00:00:00 +0000
/entries/Word_Lib.html
-
Algorithms for Reduced Ordered Binary Decision Diagrams
/entries/ROBDD.html
Wed, 27 Apr 2016 00:00:00 +0000
/entries/ROBDD.html
-
Tensor Product of Matrices
/entries/Matrix_Tensor.html
Mon, 18 Jan 2016 00:00:00 +0000
/entries/Matrix_Tensor.html
-
Reasoning about Lists via List Interleaving
/entries/List_Interleaving.html
Thu, 11 Jun 2015 00:00:00 +0000
/entries/List_Interleaving.html
-
Parameterized Dynamic Tables
/entries/Dynamic_Tables.html
Sun, 07 Jun 2015 00:00:00 +0000
/entries/Dynamic_Tables.html
-
Trie
/entries/Trie.html
Mon, 30 Mar 2015 00:00:00 +0000
/entries/Trie.html
-
Deriving class instances for datatypes
/entries/Deriving.html
Wed, 11 Mar 2015 00:00:00 +0000
/entries/Deriving.html
-
XML
/entries/XML.html
Fri, 03 Oct 2014 00:00:00 +0000
/entries/XML.html
-
Priority Queues Based on Braun Trees
/entries/Priority_Queue_Braun.html
Thu, 04 Sep 2014 00:00:00 +0000
/entries/Priority_Queue_Braun.html
-
Skew Heap
/entries/Skew_Heap.html
Wed, 13 Aug 2014 00:00:00 +0000
/entries/Skew_Heap.html
-
Splay Tree
/entries/Splay_Tree.html
Tue, 12 Aug 2014 00:00:00 +0000
/entries/Splay_Tree.html
-
Amortized Complexity Verified
/entries/Amortized_Complexity.html
Mon, 07 Jul 2014 00:00:00 +0000
/entries/Amortized_Complexity.html
-
Native Word
/entries/Native_Word.html
Tue, 17 Sep 2013 00:00:00 +0000
/entries/Native_Word.html
-
A Formal Model of IEEE Floating Point Arithmetic
/entries/IEEE_Floating_Point.html
Sat, 27 Jul 2013 00:00:00 +0000
/entries/IEEE_Floating_Point.html
-
Light-weight Containers
/entries/Containers.html
Mon, 15 Apr 2013 00:00:00 +0000
/entries/Containers.html
-
Generating linear orders for datatypes
/entries/Datatype_Order_Generator.html
Tue, 07 Aug 2012 00:00:00 +0000
/entries/Datatype_Order_Generator.html
-
Infinite Lists
/entries/List-Infinite.html
Wed, 23 Feb 2011 00:00:00 +0000
/entries/List-Infinite.html
-
Binomial Heaps and Skew Binomial Heaps
/entries/Binomial-Heaps.html
Thu, 28 Oct 2010 00:00:00 +0000
/entries/Binomial-Heaps.html
-
Finger Trees
/entries/Finger-Trees.html
Thu, 28 Oct 2010 00:00:00 +0000
/entries/Finger-Trees.html
-
Functional Binomial Queues
/entries/Binomial-Queues.html
Thu, 28 Oct 2010 00:00:00 +0000
/entries/Binomial-Queues.html
-
Executable Matrix Operations on Matrices of Arbitrary Dimensions
/entries/Matrix.html
Thu, 17 Jun 2010 00:00:00 +0000
/entries/Matrix.html
-
List Index
/entries/List-Index.html
Sat, 20 Feb 2010 00:00:00 +0000
/entries/List-Index.html
-
Collections Framework
/entries/Collections.html
Wed, 25 Nov 2009 00:00:00 +0000
/entries/Collections.html
-
Code Generation for Functions as Data
/entries/FinFun.html
Wed, 06 May 2009 00:00:00 +0000
/entries/FinFun.html
-
The Textbook Proof of Huffman's Algorithm
/entries/Huffman.html
Wed, 15 Oct 2008 00:00:00 +0000
/entries/Huffman.html
-
BDD Normalisation
/entries/BDD.html
Fri, 29 Feb 2008 00:00:00 +0000
/entries/BDD.html
-
File Refinement
/entries/FileRefinement.html
Thu, 09 Dec 2004 00:00:00 +0000
/entries/FileRefinement.html
-
Lazy Lists II
/entries/Lazy-Lists-II.html
Mon, 26 Apr 2004 00:00:00 +0000
/entries/Lazy-Lists-II.html
-
Binary Search Trees
/entries/BinarySearchTree.html
Mon, 05 Apr 2004 00:00:00 +0000
/entries/BinarySearchTree.html
-
AVL Trees
/entries/AVL-Trees.html
Fri, 19 Mar 2004 00:00:00 +0000
/entries/AVL-Trees.html
diff --git a/web/topics/computer-science/index.html b/web/topics/computer-science/index.html
--- a/web/topics/computer-science/index.html
+++ b/web/topics/computer-science/index.html
@@ -1,3462 +1,3469 @@
Computer science - Archive of Formal Proofs
Subject Classification AMS: Computer science
2023
+
+ Aug 14
+
+
+
+
Jul 25
Jul 16
Jul 11
Jun 19
Jun 16
Jun 06
Jun 01
May 09
Apr 29
Apr 27
Apr 03
Apr 03
Apr 03
Apr 03
Mar 15
Mar 15
Mar 15
Mar 03
Feb 28
Feb 02
Jan 27
Jan 20
Jan 08
Jan 03
Jan 03
2022
Dec 15
Dec 05
Nov 30
Nov 25
Nov 11
Oct 04
Sep 29
Sep 28
Sep 08
Sep 05
Aug 18
Aug 17
Aug 09
Aug 09
Jul 29
Jul 18
Jul 18
Jul 10
Jun 23
Jun 08
Jun 08
May 30
May 18
Apr 08
Apr 08
Apr 08
Apr 08
Feb 28
Feb 28
Feb 28
Feb 20
Feb 15
Feb 13
Feb 04
Feb 03
Feb 02
Jan 25
2021
Dec 29
Dec 16
Dec 15
Nov 23
Oct 28
Oct 28
Oct 28
Oct 13
Oct 13
Oct 12
Oct 02
Sep 05
Aug 26
Aug 16
Aug 16
Aug 16
Aug 16
Aug 16
Jun 18
Jun 04
May 24
May 24
May 24
Apr 30
Apr 24
Apr 13
Apr 01
Mar 17
Mar 12
Mar 03
Feb 24
Feb 24
Jan 18
Jan 11
2020
Dec 08
Dec 07
Dec 05
Nov 22
Nov 19
Nov 19
Oct 29
Oct 29
Oct 20
Oct 12
Sep 28
Sep 28
Sep 28
Sep 28
Sep 28
Sep 07
Sep 07
Aug 31
Aug 31
Aug 26
Aug 25
Jul 21
Jun 01
May 23
May 08
Apr 27
Apr 16
Apr 10
Apr 09
Apr 09
Apr 08
Apr 08
Mar 25
Mar 12
Mar 12
Mar 07
Feb 10
Jan 16
Jan 13
Jan 09
Jan 09
2019
Dec 04
Dec 04
Nov 27
Oct 22
Oct 22
Oct 16
Oct 07
Oct 04
Oct 04
Sep 16
Sep 16
Aug 16
Aug 16
Aug 06
Aug 01
Jul 30
Jul 30
Jul 30
Jul 08
Jul 04
Jul 04
Jun 25
Jun 25
Jun 13
Jun 13
Jun 03
May 30
May 14
May 14
May 09
Apr 26
Apr 26
Apr 16
Apr 06
Apr 06
Mar 24
Mar 24
Mar 09
Feb 14
Feb 11
Feb 08
Feb 01
Feb 01
Jan 15
Jan 15
Jan 15
Jan 07
2018
Dec 26
Dec 25
Dec 21
Dec 21
Dec 17
Dec 11
Nov 06
Oct 19
Oct 19
Oct 12
Sep 20
Aug 24
Jun 05
May 27
May 27
May 25
May 24
May 22
May 22
May 10
May 10
May 07
Apr 29
Apr 27
Apr 24
Mar 13
Mar 12
Mar 01
Feb 26
Feb 06
Feb 06
Feb 02
Jan 08
Jan 08
2017
Dec 21
Dec 18
Nov 22
Nov 09
Nov 09
Oct 19
Oct 19
Oct 14
Aug 20
Aug 16
Jul 28
Jul 21
Jul 15
Jul 09
Jul 07
Jul 07
Jun 01
May 25
May 24
May 08
May 05
May 05
May 05
May 05
May 05
May 05
May 05
Apr 28
Apr 04
Apr 04
Mar 15
Mar 15
Mar 15
Feb 28
Feb 13
Jan 31
Jan 17
Jan 08
Jan 08
Jan 03
2016
Dec 30
Nov 29
Nov 29
Nov 23
Nov 16
Nov 10
Oct 25
Oct 21
Oct 19
Oct 19
Sep 30
Sep 09
Aug 31
Aug 24
Aug 18
Aug 12
Aug 08
Aug 08
Jul 14
Jul 05
Jun 28
Jun 28
Jun 25
Jun 25
Jun 13
Jun 13
Jun 09
May 24
May 18
May 02
Apr 27
Apr 27
Apr 27
Apr 27
Apr 26
Apr 26
Apr 12
Apr 12
Mar 08
Mar 01
Feb 17
Feb 17
Feb 05
Jan 18
2015
Dec 22
Nov 18
Sep 16
Sep 04
Aug 18
Aug 10
Jul 21
Jul 07
Jun 11
Jun 11
Jun 11
Jun 11
Jun 07
May 28
May 27
Apr 13
Apr 13
Mar 30
Mar 18
Mar 11
Feb 20
Feb 12
Feb 12
Feb 05
Jan 28
2014
Nov 28
Oct 23
Oct 13
Oct 10
Oct 09
Oct 08
Oct 03
Oct 03
Oct 03
Sep 25
Sep 04
Sep 03
Aug 13
Aug 12
Jul 29
Jul 18
Jul 13
Jul 07
Jul 04
Jul 03
Jun 12
Jun 08
May 28
May 28
May 28
May 28
May 28
May 23
May 23
May 21
Apr 28
Apr 23
Apr 23
Apr 23
Apr 23
Apr 23
Apr 23
Apr 22
Apr 16
Apr 03
Mar 11
Mar 08
Feb 18
Feb 11
Jan 30
Jan 23
Jan 23
Jan 16
Jan 11
2013
Dec 01
Nov 15
Nov 14
Oct 02
Sep 17
Jul 27
Apr 15
Jan 31
Jan 31
Jan 19
Jan 15
Jan 15
2012
Nov 14
Sep 10
Sep 10
Aug 07
Jul 27
Jul 01
Jun 26
May 29
May 29
May 29
May 27
May 27
May 11
May 07
May 02
Mar 01
Feb 29
Jan 30
Jan 30
Jan 03
2011
Nov 19
Nov 09
Sep 22
Aug 26
Aug 19
May 17
Mar 14
Feb 23
Feb 23
Feb 07
Jan 10
2010
Nov 16
Oct 28
Oct 28
Oct 28
Aug 29
Aug 10
Aug 08
Jun 17
May 28
May 28
May 12
Apr 30
Mar 23
Mar 23
Feb 20
Feb 12
2009
Dec 03
Nov 25
Nov 25
Nov 13
Oct 30
May 06
Apr 29
2008
Dec 12
Nov 10
Nov 10
Oct 15
Sep 16
Sep 02
Sep 02
Jul 23
Feb 29
Feb 29
Feb 29
Feb 18
2007
Dec 14
Dec 03
Nov 06
Aug 02
2006
Sep 09
Aug 08
May 15
Mar 31
Mar 15
2005
Oct 12
Jun 24
Jun 22
Jun 20
Jun 01
May 02
2004
Dec 09
Jul 09
Jun 24
Apr 26
Apr 05
Mar 30
Mar 19
Mar 19
\ No newline at end of file
diff --git a/web/topics/computer-science/index.xml b/web/topics/computer-science/index.xml
--- a/web/topics/computer-science/index.xml
+++ b/web/topics/computer-science/index.xml
@@ -1,4304 +1,4313 @@
Computer science on Archive of Formal Proofs
/topics/computer-science/
Recent content in Computer science on Archive of Formal Proofs
Hugo -- gohugo.io
en-gb
- Tue, 25 Jul 2023 00:00:00 +0000
+ Mon, 14 Aug 2023 00:00:00 +0000
+ -
+
Fixed-length vectors
+ /entries/Fixed_Length_Vector.html
+ Mon, 14 Aug 2023 00:00:00 +0000
+
+ /entries/Fixed_Length_Vector.html
+
+
+
-
Modal quantales, involutive quantales, Dedekind Quantales
/entries/Quantales_Converse.html
Tue, 25 Jul 2023 00:00:00 +0000
/entries/Quantales_Converse.html
-
Earley Parser
/entries/Earley_Parser.html
Sun, 16 Jul 2023 00:00:00 +0000
/entries/Earley_Parser.html
-
Gray Codes for Arbitrary Numeral Systems
/entries/Gray_Codes.html
Tue, 11 Jul 2023 00:00:00 +0000
/entries/Gray_Codes.html
-
Executable Randomized Algorithms
/entries/Executable_Randomized_Algorithms.html
Mon, 19 Jun 2023 00:00:00 +0000
/entries/Executable_Randomized_Algorithms.html
-
DCR Syntax and Execution Equivalent Markings
/entries/DCR-ExecutionEquivalence.html
Fri, 16 Jun 2023 00:00:00 +0000
/entries/DCR-ExecutionEquivalence.html
-
Cryptographic Standards
/entries/Crypto_Standards.html
Tue, 06 Jun 2023 00:00:00 +0000
/entries/Crypto_Standards.html
-
A Verified Efficient Implementation of the Weighted Path Order
/entries/Efficient_Weighted_Path_Order.html
Thu, 01 Jun 2023 00:00:00 +0000
/entries/Efficient_Weighted_Path_Order.html
-
Tree Enumeration
/entries/Tree_Enumeration.html
Tue, 09 May 2023 00:00:00 +0000
/entries/Tree_Enumeration.html
-
The Halting Problem is Soluble in Malament-Hogarth Spacetimes
/entries/MHComputation.html
Sat, 29 Apr 2023 00:00:00 +0000
/entries/MHComputation.html
-
The Schwartz-Zippel Lemma
/entries/Schwartz_Zippel.html
Thu, 27 Apr 2023 00:00:00 +0000
/entries/Schwartz_Zippel.html
-
Distributed Distinct Elements
/entries/Distributed_Distinct_Elements.html
Mon, 03 Apr 2023 00:00:00 +0000
/entries/Distributed_Distinct_Elements.html
-
Distributed Distinct Elements
/entries/Distributed_Distinct_Elements.html
Mon, 03 Apr 2023 00:00:00 +0000
/entries/Distributed_Distinct_Elements.html
-
Distributed Distinct Elements
/entries/Distributed_Distinct_Elements.html
Mon, 03 Apr 2023 00:00:00 +0000
/entries/Distributed_Distinct_Elements.html
-
Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties
/entries/HyperHoareLogic.html
Mon, 03 Apr 2023 00:00:00 +0000
/entries/HyperHoareLogic.html
-
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs
/entries/CommCSL.html
Wed, 15 Mar 2023 00:00:00 +0000
/entries/CommCSL.html
-
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs
/entries/CommCSL.html
Wed, 15 Mar 2023 00:00:00 +0000
/entries/CommCSL.html
-
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs
/entries/CommCSL.html
Wed, 15 Mar 2023 00:00:00 +0000
/entries/CommCSL.html
-
Expander Graphs
/entries/Expander_Graphs.html
Fri, 03 Mar 2023 00:00:00 +0000
/entries/Expander_Graphs.html
-
Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion
/entries/Rensets.html
Tue, 28 Feb 2023 00:00:00 +0000
/entries/Rensets.html
-
Hardness of Lattice Problems
/entries/CVP_Hardness.html
Thu, 02 Feb 2023 00:00:00 +0000
/entries/CVP_Hardness.html
-
ABY3 Multiplication and Array Shuffling
/entries/ABY3_Protocols.html
Fri, 27 Jan 2023 00:00:00 +0000
/entries/ABY3_Protocols.html
-
A Hoare Logic for Diverging Programs
/entries/HoareForDivergence.html
Fri, 20 Jan 2023 00:00:00 +0000
/entries/HoareForDivergence.html
-
The Cook-Levin theorem
/entries/Cook_Levin.html
Sun, 08 Jan 2023 00:00:00 +0000
/entries/Cook_Levin.html
-
Binary codes that do not preserve primitivity
/entries/Binary_Code_Imprimitive.html
Tue, 03 Jan 2023 00:00:00 +0000
/entries/Binary_Code_Imprimitive.html
-
Intersection of two monoids generated by two element codes
/entries/Two_Generated_Word_Monoids_Intersection.html
Tue, 03 Jan 2023 00:00:00 +0000
/entries/Two_Generated_Word_Monoids_Intersection.html
-
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
/entries/Quantifier_Elimination_Hybrid.html
Thu, 15 Dec 2022 00:00:00 +0000
/entries/Quantifier_Elimination_Hybrid.html
-
Automation of Boolos' Curious Inference in Isabelle/HOL
/entries/Boolos_Curious_Inference_Automated.html
Mon, 05 Dec 2022 00:00:00 +0000
/entries/Boolos_Curious_Inference_Automated.html
-
A Verified Translation of Multitape Turing Machines into Singletape Turing Machines
/entries/Multitape_To_Singletape_TM.html
Wed, 30 Nov 2022 00:00:00 +0000
/entries/Multitape_To_Singletape_TM.html
-
A Formal CHERI-C Memory Model
/entries/CHERI-C_Memory_Model.html
Fri, 25 Nov 2022 00:00:00 +0000
/entries/CHERI-C_Memory_Model.html
-
Combinatorial Enumeration Algorithms
/entries/Combinatorial_Enumeration_Algorithms.html
Fri, 11 Nov 2022 00:00:00 +0000
/entries/Combinatorial_Enumeration_Algorithms.html
-
Verification of Query Optimization Algorithms
/entries/Query_Optimization.html
Tue, 04 Oct 2022 00:00:00 +0000
/entries/Query_Optimization.html
-
Maximum Segment Sum
/entries/Maximum_Segment_Sum.html
Thu, 29 Sep 2022 00:00:00 +0000
/entries/Maximum_Segment_Sum.html
-
Making Arbitrary Relational Calculus Queries Safe-Range
/entries/Safe_Range_RC.html
Wed, 28 Sep 2022 00:00:00 +0000
/entries/Safe_Range_RC.html
-
CRYSTALS-Kyber
/entries/CRYSTALS-Kyber.html
Thu, 08 Sep 2022 00:00:00 +0000
/entries/CRYSTALS-Kyber.html
-
Unbounded Separation Logic
/entries/Separation_Logic_Unbounded.html
Mon, 05 Sep 2022 00:00:00 +0000
/entries/Separation_Logic_Unbounded.html
-
Number Theoretic Transform
/entries/Number_Theoretic_Transform.html
Thu, 18 Aug 2022 00:00:00 +0000
/entries/Number_Theoretic_Transform.html
-
Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph
/entries/SCC_Bloemen_Sequential.html
Wed, 17 Aug 2022 00:00:00 +0000
/entries/SCC_Bloemen_Sequential.html
-
Verified Complete Test Strategies for Finite State Machines
/entries/FSM_Tests.html
Tue, 09 Aug 2022 00:00:00 +0000
/entries/FSM_Tests.html
-
Verified Complete Test Strategies for Finite State Machines
/entries/FSM_Tests.html
Tue, 09 Aug 2022 00:00:00 +0000
/entries/FSM_Tests.html
-
Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML
/entries/Nano_JSON.html
Fri, 29 Jul 2022 00:00:00 +0000
/entries/Nano_JSON.html
-
Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL
/entries/Solidity.html
Mon, 18 Jul 2022 00:00:00 +0000
/entries/Solidity.html
-
Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL
/entries/Solidity.html
Mon, 18 Jul 2022 00:00:00 +0000
/entries/Solidity.html
-
A Reuse-Based Multi-Stage Compiler Verification for Language IMP
/entries/IMP_Compiler_Reuse.html
Sun, 10 Jul 2022 00:00:00 +0000
/entries/IMP_Compiler_Reuse.html
-
Real-Time Double-Ended Queue
/entries/Real_Time_Deque.html
Thu, 23 Jun 2022 00:00:00 +0000
/entries/Real_Time_Deque.html
-
IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols
/entries/IsaNet.html
Wed, 08 Jun 2022 00:00:00 +0000
/entries/IsaNet.html
-
IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols
/entries/IsaNet.html
Wed, 08 Jun 2022 00:00:00 +0000
/entries/IsaNet.html
-
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
/entries/Combinable_Wands.html
Mon, 30 May 2022 00:00:00 +0000
/entries/Combinable_Wands.html
-
Formalization of a Framework for the Sound Automation of Magic Wands
/entries/Package_logic.html
Wed, 18 May 2022 00:00:00 +0000
/entries/Package_logic.html
-
A Combinator Library for Prefix-Free Codes
/entries/Prefix_Free_Code_Combinators.html
Fri, 08 Apr 2022 00:00:00 +0000
/entries/Prefix_Free_Code_Combinators.html
-
A Combinator Library for Prefix-Free Codes
/entries/Prefix_Free_Code_Combinators.html
Fri, 08 Apr 2022 00:00:00 +0000
/entries/Prefix_Free_Code_Combinators.html
-
Formalization of Randomized Approximation Algorithms for Frequency Moments
/entries/Frequency_Moments.html
Fri, 08 Apr 2022 00:00:00 +0000
/entries/Frequency_Moments.html
-
Formalization of Randomized Approximation Algorithms for Frequency Moments
/entries/Frequency_Moments.html
Fri, 08 Apr 2022 00:00:00 +0000
/entries/Frequency_Moments.html
-
Residuated Transition Systems
/entries/ResiduatedTransitionSystem.html
Mon, 28 Feb 2022 00:00:00 +0000
/entries/ResiduatedTransitionSystem.html
-
Residuated Transition Systems
/entries/ResiduatedTransitionSystem.html
Mon, 28 Feb 2022 00:00:00 +0000
/entries/ResiduatedTransitionSystem.html
-
Residuated Transition Systems
/entries/ResiduatedTransitionSystem.html
Mon, 28 Feb 2022 00:00:00 +0000
/entries/ResiduatedTransitionSystem.html
-
Universal Hash Families
/entries/Universal_Hash_Families.html
Sun, 20 Feb 2022 00:00:00 +0000
/entries/Universal_Hash_Families.html
-
First-Order Query Evaluation
/entries/Eval_FO.html
Tue, 15 Feb 2022 00:00:00 +0000
/entries/Eval_FO.html
-
Multi-Head Monitoring of Metric Dynamic Logic
/entries/VYDRA_MDL.html
Sun, 13 Feb 2022 00:00:00 +0000
/entries/VYDRA_MDL.html
-
Enumeration of Equivalence Relations
/entries/Equivalence_Relation_Enumeration.html
Fri, 04 Feb 2022 00:00:00 +0000
/entries/Equivalence_Relation_Enumeration.html
-
Quasi-Borel Spaces
/entries/Quasi_Borel_Spaces.html
Thu, 03 Feb 2022 00:00:00 +0000
/entries/Quasi_Borel_Spaces.html
-
First-Order Theory of Rewriting
/entries/FO_Theory_Rewriting.html
Wed, 02 Feb 2022 00:00:00 +0000
/entries/FO_Theory_Rewriting.html
-
Median Method
/entries/Median_Method.html
Tue, 25 Jan 2022 00:00:00 +0000
/entries/Median_Method.html
-
Gale-Shapley Algorithm
/entries/Gale_Shapley.html
Wed, 29 Dec 2021 00:00:00 +0000
/entries/Gale_Shapley.html
-
Verified Algorithms for Solving Markov Decision Processes
/entries/MDP-Algorithms.html
Thu, 16 Dec 2021 00:00:00 +0000
/entries/MDP-Algorithms.html
-
Regular Tree Relations
/entries/Regular_Tree_Relations.html
Wed, 15 Dec 2021 00:00:00 +0000
/entries/Regular_Tree_Relations.html
-
van Emde Boas Trees
/entries/Van_Emde_Boas_Trees.html
Tue, 23 Nov 2021 00:00:00 +0000
/entries/Van_Emde_Boas_Trees.html
-
Quantum and Classical Registers
/entries/Registers.html
Thu, 28 Oct 2021 00:00:00 +0000
/entries/Registers.html
-
Quantum and Classical Registers
/entries/Registers.html
Thu, 28 Oct 2021 00:00:00 +0000
/entries/Registers.html
-
Quantum and Classical Registers
/entries/Registers.html
Thu, 28 Oct 2021 00:00:00 +0000
/entries/Registers.html
-
X86 instruction semantics and basic block symbolic execution
/entries/X86_Semantics.html
Wed, 13 Oct 2021 00:00:00 +0000
/entries/X86_Semantics.html
-
X86 instruction semantics and basic block symbolic execution
/entries/X86_Semantics.html
Wed, 13 Oct 2021 00:00:00 +0000
/entries/X86_Semantics.html
-
Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations
/entries/Correctness_Algebras.html
Tue, 12 Oct 2021 00:00:00 +0000
/entries/Correctness_Algebras.html
-
Verified Quadratic Virtual Substitution for Real Arithmetic
/entries/Virtual_Substitution.html
Sat, 02 Oct 2021 00:00:00 +0000
/entries/Virtual_Substitution.html
-
A data flow analysis algorithm for computing dominators
/entries/Dominance_CHK.html
Sun, 05 Sep 2021 00:00:00 +0000
/entries/Dominance_CHK.html
-
Logging-independent Message Anonymity in the Relational Method
/entries/Logging_Independent_Anonymity.html
Thu, 26 Aug 2021 00:00:00 +0000
/entries/Logging_Independent_Anonymity.html
-
CoCon: A Confidentiality-Verified Conference Management System
/entries/CoCon.html
Mon, 16 Aug 2021 00:00:00 +0000
/entries/CoCon.html
-
Compositional BD Security
/entries/BD_Security_Compositional.html
Mon, 16 Aug 2021 00:00:00 +0000
/entries/BD_Security_Compositional.html
-
CoSMed: A confidentiality-verified social media platform
/entries/CoSMed.html
Mon, 16 Aug 2021 00:00:00 +0000
/entries/CoSMed.html
-
CoSMeDis: A confidentiality-verified distributed social media platform
/entries/CoSMeDis.html
Mon, 16 Aug 2021 00:00:00 +0000
/entries/CoSMeDis.html
-
Fresh identifiers
/entries/Fresh_Identifiers.html
Mon, 16 Aug 2021 00:00:00 +0000
/entries/Fresh_Identifiers.html
-
MiniSail - A kernel language for the ISA specification language SAIL
/entries/MiniSail.html
Fri, 18 Jun 2021 00:00:00 +0000
/entries/MiniSail.html
-
A Shorter Compiler Correctness Proof for Language IMP
/entries/IMP_Compiler.html
Fri, 04 Jun 2021 00:00:00 +0000
/entries/IMP_Compiler.html
-
Combinatorics on Words Basics
/entries/Combinatorics_Words.html
Mon, 24 May 2021 00:00:00 +0000
/entries/Combinatorics_Words.html
-
Graph Lemma
/entries/Combinatorics_Words_Graph_Lemma.html
Mon, 24 May 2021 00:00:00 +0000
/entries/Combinatorics_Words_Graph_Lemma.html
-
Lyndon words
/entries/Combinatorics_Words_Lyndon.html
Mon, 24 May 2021 00:00:00 +0000
/entries/Combinatorics_Words_Lyndon.html
-
Regression Test Selection
/entries/Regression_Test_Selection.html
Fri, 30 Apr 2021 00:00:00 +0000
/entries/Regression_Test_Selection.html
-
The BKR Decision Procedure for Univariate Real Arithmetic
/entries/BenOr_Kozen_Reif.html
Sat, 24 Apr 2021 00:00:00 +0000
/entries/BenOr_Kozen_Reif.html
-
Formalization of Timely Dataflow's Progress Tracking Protocol
/entries/Progress_Tracking.html
Tue, 13 Apr 2021 00:00:00 +0000
/entries/Progress_Tracking.html
-
Information Flow Control via Dependency Tracking
/entries/IFC_Tracking.html
Thu, 01 Apr 2021 00:00:00 +0000
/entries/IFC_Tracking.html
-
Constructive Cryptography in HOL: the Communication Modeling Aspect
/entries/Constructive_Cryptography_CM.html
Wed, 17 Mar 2021 00:00:00 +0000
/entries/Constructive_Cryptography_CM.html
-
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html
Fri, 12 Mar 2021 00:00:00 +0000
/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html
-
Quantum projective measurements and the CHSH inequality
/entries/Projective_Measurements.html
Wed, 03 Mar 2021 00:00:00 +0000
/entries/Projective_Measurements.html
-
A Verified Imperative Implementation of B-Trees
/entries/BTree.html
Wed, 24 Feb 2021 00:00:00 +0000
/entries/BTree.html
-
A Verified Imperative Implementation of B-Trees
/entries/BTree.html
Wed, 24 Feb 2021 00:00:00 +0000
/entries/BTree.html
-
Hood-Melville Queue
/entries/Hood_Melville_Queue.html
Mon, 18 Jan 2021 00:00:00 +0000
/entries/Hood_Melville_Queue.html
-
JinjaDCI: a Java semantics with dynamic class initialization
/entries/JinjaDCI.html
Mon, 11 Jan 2021 00:00:00 +0000
/entries/JinjaDCI.html
-
Relational Minimum Spanning Tree Algorithms
/entries/Relational_Minimum_Spanning_Trees.html
Tue, 08 Dec 2020 00:00:00 +0000
/entries/Relational_Minimum_Spanning_Trees.html
-
Inline Caching and Unboxing Optimization for Interpreters
/entries/Interpreter_Optimizations.html
Mon, 07 Dec 2020 00:00:00 +0000
/entries/Interpreter_Optimizations.html
-
The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
/entries/Relational_Method.html
Sat, 05 Dec 2020 00:00:00 +0000
/entries/Relational_Method.html
-
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information
/entries/Isabelle_Marries_Dirac.html
Sun, 22 Nov 2020 00:00:00 +0000
/entries/Isabelle_Marries_Dirac.html
-
The HOL-CSP Refinement Toolkit
/entries/CSP_RefTK.html
Thu, 19 Nov 2020 00:00:00 +0000
/entries/CSP_RefTK.html
-
The HOL-CSP Refinement Toolkit
/entries/CSP_RefTK.html
Thu, 19 Nov 2020 00:00:00 +0000
/entries/CSP_RefTK.html
-
AI Planning Languages Semantics
/entries/AI_Planning_Languages_Semantics.html
Thu, 29 Oct 2020 00:00:00 +0000
/entries/AI_Planning_Languages_Semantics.html
-
Verified SAT-Based AI Planning
/entries/Verified_SAT_Based_AI_Planning.html
Thu, 29 Oct 2020 00:00:00 +0000
/entries/Verified_SAT_Based_AI_Planning.html
-
A Sound Type System for Physical Quantities, Units, and Measurements
/entries/Physical_Quantities.html
Tue, 20 Oct 2020 00:00:00 +0000
/entries/Physical_Quantities.html
-
Finite Map Extras
/entries/Finite-Map-Extras.html
Mon, 12 Oct 2020 00:00:00 +0000
/entries/Finite-Map-Extras.html
-
A Formal Model of the Document Object Model with Shadow Roots
/entries/Shadow_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/Shadow_DOM.html
-
A Formal Model of the Safely Composable Document Object Model with Shadow Roots
/entries/Shadow_SC_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/Shadow_SC_DOM.html
-
A Formalization of Safely Composable Web Components
/entries/SC_DOM_Components.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/SC_DOM_Components.html
-
A Formalization of Web Components
/entries/DOM_Components.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/DOM_Components.html
-
The Safely Composable DOM
/entries/Core_SC_DOM.html
Mon, 28 Sep 2020 00:00:00 +0000
/entries/Core_SC_DOM.html
-
A Formal Model of Extended Finite State Machines
/entries/Extended_Finite_State_Machines.html
Mon, 07 Sep 2020 00:00:00 +0000
/entries/Extended_Finite_State_Machines.html
-
Inference of Extended Finite State Machines
/entries/Extended_Finite_State_Machine_Inference.html
Mon, 07 Sep 2020 00:00:00 +0000
/entries/Extended_Finite_State_Machine_Inference.html
-
Practical Algebraic Calculus Checker
/entries/PAC_Checker.html
Mon, 31 Aug 2020 00:00:00 +0000
/entries/PAC_Checker.html
-
Some classical results in inductive inference of recursive functions
/entries/Inductive_Inference.html
Mon, 31 Aug 2020 00:00:00 +0000
/entries/Inductive_Inference.html
-
Relational Disjoint-Set Forests
/entries/Relational_Disjoint_Set_Forests.html
Wed, 26 Aug 2020 00:00:00 +0000
/entries/Relational_Disjoint_Set_Forests.html
-
Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching
/entries/BirdKMP.html
Tue, 25 Aug 2020 00:00:00 +0000
/entries/BirdKMP.html
-
A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm
/entries/Chandy_Lamport.html
Tue, 21 Jul 2020 00:00:00 +0000
/entries/Chandy_Lamport.html
-
A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles
/entries/Safe_Distance.html
Mon, 01 Jun 2020 00:00:00 +0000
/entries/Safe_Distance.html
-
A verified algorithm for computing the Smith normal form of a matrix
/entries/Smith_Normal_Form.html
Sat, 23 May 2020 00:00:00 +0000
/entries/Smith_Normal_Form.html
-
An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation
/entries/LTL_Normal_Form.html
Fri, 08 May 2020 00:00:00 +0000
/entries/LTL_Normal_Form.html
-
Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems
/entries/Attack_Trees.html
Mon, 27 Apr 2020 00:00:00 +0000
/entries/Attack_Trees.html
-
Authenticated Data Structures As Functors
/entries/ADS_Functor.html
Thu, 16 Apr 2020 00:00:00 +0000
/entries/ADS_Functor.html
-
Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows
/entries/Sliding_Window_Algorithm.html
Fri, 10 Apr 2020 00:00:00 +0000
/entries/Sliding_Window_Algorithm.html
-
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
/entries/MFODL_Monitor_Optimized.html
Thu, 09 Apr 2020 00:00:00 +0000
/entries/MFODL_Monitor_Optimized.html
-
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
/entries/MFODL_Monitor_Optimized.html
Thu, 09 Apr 2020 00:00:00 +0000
/entries/MFODL_Monitor_Optimized.html
-
Automated Stateful Protocol Verification
/entries/Automated_Stateful_Protocol_Verification.html
Wed, 08 Apr 2020 00:00:00 +0000
/entries/Automated_Stateful_Protocol_Verification.html
-
Stateful Protocol Composition and Typing
/entries/Stateful_Protocol_Composition_and_Typing.html
Wed, 08 Apr 2020 00:00:00 +0000
/entries/Stateful_Protocol_Composition_and_Typing.html
-
Strong Eventual Consistency of the Collaborative Editing Framework WOOT
/entries/WOOT_Strong_Eventual_Consistency.html
Wed, 25 Mar 2020 00:00:00 +0000
/entries/WOOT_Strong_Eventual_Consistency.html
-
An Under-Approximate Relational Logic
/entries/Relational-Incorrectness-Logic.html
Thu, 12 Mar 2020 00:00:00 +0000
/entries/Relational-Incorrectness-Logic.html
-
An Under-Approximate Relational Logic
/entries/Relational-Incorrectness-Logic.html
Thu, 12 Mar 2020 00:00:00 +0000
/entries/Relational-Incorrectness-Logic.html
-
Hello World
/entries/Hello_World.html
Sat, 07 Mar 2020 00:00:00 +0000
/entries/Hello_World.html
-
A Generic Framework for Verified Compilers
/entries/VeriComp.html
Mon, 10 Feb 2020 00:00:00 +0000
/entries/VeriComp.html
-
Verified Approximation Algorithms
/entries/Approximation_Algorithms.html
Thu, 16 Jan 2020 00:00:00 +0000
/entries/Approximation_Algorithms.html
-
Closest Pair of Points Algorithms
/entries/Closest_Pair_Points.html
Mon, 13 Jan 2020 00:00:00 +0000
/entries/Closest_Pair_Points.html
-
Skip Lists
/entries/Skip_Lists.html
Thu, 09 Jan 2020 00:00:00 +0000
/entries/Skip_Lists.html
-
Skip Lists
/entries/Skip_Lists.html
Thu, 09 Jan 2020 00:00:00 +0000
/entries/Skip_Lists.html
-
An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
/entries/Generalized_Counting_Sort.html
Wed, 04 Dec 2019 00:00:00 +0000
/entries/Generalized_Counting_Sort.html
-
An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
/entries/Generalized_Counting_Sort.html
Wed, 04 Dec 2019 00:00:00 +0000
/entries/Generalized_Counting_Sort.html
-
Interval Arithmetic on 32-bit Words
/entries/Interval_Arithmetic_Word32.html
Wed, 27 Nov 2019 00:00:00 +0000
/entries/Interval_Arithmetic_Word32.html
-
Isabelle/C
/entries/Isabelle_C.html
Tue, 22 Oct 2019 00:00:00 +0000
/entries/Isabelle_C.html
-
Isabelle/C
/entries/Isabelle_C.html
Tue, 22 Oct 2019 00:00:00 +0000
/entries/Isabelle_C.html
-
VerifyThis 2019 -- Polished Isabelle Solutions
/entries/VerifyThis2019.html
Wed, 16 Oct 2019 00:00:00 +0000
/entries/VerifyThis2019.html
-
Sigma Protocols and Commitment Schemes
/entries/Sigma_Commit_Crypto.html
Mon, 07 Oct 2019 00:00:00 +0000
/entries/Sigma_Commit_Crypto.html
-
Clean - An Abstract Imperative Programming Language and its Theory
/entries/Clean.html
Fri, 04 Oct 2019 00:00:00 +0000
/entries/Clean.html
-
Clean - An Abstract Imperative Programming Language and its Theory
/entries/Clean.html
Fri, 04 Oct 2019 00:00:00 +0000
/entries/Clean.html
-
Formalization of Multiway-Join Algorithms
/entries/Generic_Join.html
Mon, 16 Sep 2019 00:00:00 +0000
/entries/Generic_Join.html
-
Formalization of Multiway-Join Algorithms
/entries/Generic_Join.html
Mon, 16 Sep 2019 00:00:00 +0000
/entries/Generic_Join.html
-
Formalisation of an Adaptive State Counting Algorithm
/entries/Adaptive_State_Counting.html
Fri, 16 Aug 2019 00:00:00 +0000
/entries/Adaptive_State_Counting.html
-
Formalisation of an Adaptive State Counting Algorithm
/entries/Adaptive_State_Counting.html
Fri, 16 Aug 2019 00:00:00 +0000
/entries/Adaptive_State_Counting.html
-
Communicating Concurrent Kleene Algebra for Distributed Systems Specification
/entries/C2KA_DistributedSystems.html
Tue, 06 Aug 2019 00:00:00 +0000
/entries/C2KA_DistributedSystems.html
-
Stellar Quorum Systems
/entries/Stellar_Quorums.html
Thu, 01 Aug 2019 00:00:00 +0000
/entries/Stellar_Quorums.html
-
A Formal Development of a Polychronous Polytimed Coordination Language
/entries/TESL_Language.html
Tue, 30 Jul 2019 00:00:00 +0000
/entries/TESL_Language.html
-
A Formal Development of a Polychronous Polytimed Coordination Language
/entries/TESL_Language.html
Tue, 30 Jul 2019 00:00:00 +0000
/entries/TESL_Language.html
-
A Formal Development of a Polychronous Polytimed Coordination Language
/entries/TESL_Language.html
Tue, 30 Jul 2019 00:00:00 +0000
/entries/TESL_Language.html
-
A Verified Code Generator from Isabelle/HOL to CakeML
/entries/CakeML_Codegen.html
Mon, 08 Jul 2019 00:00:00 +0000
/entries/CakeML_Codegen.html
-
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
/entries/MFOTL_Monitor.html
Thu, 04 Jul 2019 00:00:00 +0000
/entries/MFOTL_Monitor.html
-
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
/entries/MFOTL_Monitor.html
Thu, 04 Jul 2019 00:00:00 +0000
/entries/MFOTL_Monitor.html
-
Priority Search Trees
/entries/Priority_Search_Trees.html
Tue, 25 Jun 2019 00:00:00 +0000
/entries/Priority_Search_Trees.html
-
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
/entries/Prim_Dijkstra_Simple.html
Tue, 25 Jun 2019 00:00:00 +0000
/entries/Prim_Dijkstra_Simple.html
-
Binary Heaps for IMP2
/entries/IMP2_Binary_Heap.html
Thu, 13 Jun 2019 00:00:00 +0000
/entries/IMP2_Binary_Heap.html
-
Binary Heaps for IMP2
/entries/IMP2_Binary_Heap.html
Thu, 13 Jun 2019 00:00:00 +0000
/entries/IMP2_Binary_Heap.html
-
Differential Game Logic
/entries/Differential_Game_Logic.html
Mon, 03 Jun 2019 00:00:00 +0000
/entries/Differential_Game_Logic.html
-
Multidimensional Binary Search Trees
/entries/KD_Tree.html
Thu, 30 May 2019 00:00:00 +0000
/entries/KD_Tree.html
-
Formalization of Generic Authenticated Data Structures
/entries/LambdaAuth.html
Tue, 14 May 2019 00:00:00 +0000
/entries/LambdaAuth.html
-
Formalization of Generic Authenticated Data Structures
/entries/LambdaAuth.html
Tue, 14 May 2019 00:00:00 +0000
/entries/LambdaAuth.html
-
Multi-Party Computation
/entries/Multi_Party_Computation.html
Thu, 09 May 2019 00:00:00 +0000
/entries/Multi_Party_Computation.html
-
HOL-CSP Version 2.0
/entries/HOL-CSP.html
Fri, 26 Apr 2019 00:00:00 +0000
/entries/HOL-CSP.html
-
HOL-CSP Version 2.0
/entries/HOL-CSP.html
Fri, 26 Apr 2019 00:00:00 +0000
/entries/HOL-CSP.html
-
A Compositional and Unified Translation of LTL into Ο-Automata
/entries/LTL_Master_Theorem.html
Tue, 16 Apr 2019 00:00:00 +0000
/entries/LTL_Master_Theorem.html
-
A General Theory of Syntax with Bindings
/entries/Binding_Syntax_Theory.html
Sat, 06 Apr 2019 00:00:00 +0000
/entries/Binding_Syntax_Theory.html
-
A General Theory of Syntax with Bindings
/entries/Binding_Syntax_Theory.html
Sat, 06 Apr 2019 00:00:00 +0000
/entries/Binding_Syntax_Theory.html
-
Quantum Hoare Logic
/entries/QHLProver.html
Sun, 24 Mar 2019 00:00:00 +0000
/entries/QHLProver.html
-
Quantum Hoare Logic
/entries/QHLProver.html
Sun, 24 Mar 2019 00:00:00 +0000
/entries/QHLProver.html
-
Safe OCL
/entries/Safe_OCL.html
Sat, 09 Mar 2019 00:00:00 +0000
/entries/Safe_OCL.html
-
Kruskal's Algorithm for Minimum Spanning Forest
/entries/Kruskal.html
Thu, 14 Feb 2019 00:00:00 +0000
/entries/Kruskal.html
-
Probabilistic Primality Testing
/entries/Probabilistic_Prime_Tests.html
Mon, 11 Feb 2019 00:00:00 +0000
/entries/Probabilistic_Prime_Tests.html
-
Universal Turing Machine
/entries/Universal_Turing_Machine.html
Fri, 08 Feb 2019 00:00:00 +0000
/entries/Universal_Turing_Machine.html
-
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
/entries/UTP.html
Fri, 01 Feb 2019 00:00:00 +0000
/entries/UTP.html
-
The Inversions of a List
/entries/List_Inversions.html
Fri, 01 Feb 2019 00:00:00 +0000
/entries/List_Inversions.html
-
An Algebra for Higher-Order Terms
/entries/Higher_Order_Terms.html
Tue, 15 Jan 2019 00:00:00 +0000
/entries/Higher_Order_Terms.html
-
IMP2 β Simple Program Verification in Isabelle/HOL
/entries/IMP2.html
Tue, 15 Jan 2019 00:00:00 +0000
/entries/IMP2.html
-
IMP2 β Simple Program Verification in Isabelle/HOL
/entries/IMP2.html
Tue, 15 Jan 2019 00:00:00 +0000
/entries/IMP2.html
-
A Reduction Theorem for Store Buffers
/entries/Store_Buffer_Reduction.html
Mon, 07 Jan 2019 00:00:00 +0000
/entries/Store_Buffer_Reduction.html
-
A Formal Model of the Document Object Model
/entries/Core_DOM.html
Wed, 26 Dec 2018 00:00:00 +0000
/entries/Core_DOM.html
-
Formalization of Concurrent Revisions
/entries/Concurrent_Revisions.html
Tue, 25 Dec 2018 00:00:00 +0000
/entries/Concurrent_Revisions.html
-
Verifying Imperative Programs using Auto2
/entries/Auto2_Imperative_HOL.html
Fri, 21 Dec 2018 00:00:00 +0000
/entries/Auto2_Imperative_HOL.html
-
Verifying Imperative Programs using Auto2
/entries/Auto2_Imperative_HOL.html
Fri, 21 Dec 2018 00:00:00 +0000
/entries/Auto2_Imperative_HOL.html
-
Constructive Cryptography in HOL
/entries/Constructive_Cryptography.html
Mon, 17 Dec 2018 00:00:00 +0000
/entries/Constructive_Cryptography.html
-
Transformer Semantics
/entries/Transformer_Semantics.html
Tue, 11 Dec 2018 00:00:00 +0000
/entries/Transformer_Semantics.html
-
Deriving generic class instances for datatypes
/entries/Generic_Deriving.html
Tue, 06 Nov 2018 00:00:00 +0000
/entries/Generic_Deriving.html
-
Randomised Binary Search Trees
/entries/Randomised_BSTs.html
Fri, 19 Oct 2018 00:00:00 +0000
/entries/Randomised_BSTs.html
-
Randomised Binary Search Trees
/entries/Randomised_BSTs.html
Fri, 19 Oct 2018 00:00:00 +0000
/entries/Randomised_BSTs.html
-
Upper Bounding Diameters of State Spaces of Factored Transition Systems
/entries/Factored_Transition_System_Bounding.html
Fri, 12 Oct 2018 00:00:00 +0000
/entries/Factored_Transition_System_Bounding.html
-
Signature-Based GrΓΆbner Basis Algorithms
/entries/Signature_Groebner.html
Thu, 20 Sep 2018 00:00:00 +0000
/entries/Signature_Groebner.html
-
An Incremental Simplex Algorithm with Unsatisfiable Core Generation
/entries/Simplex.html
Fri, 24 Aug 2018 00:00:00 +0000
/entries/Simplex.html
-
Partial Order Reduction
/entries/Partial_Order_Reduction.html
Tue, 05 Jun 2018 00:00:00 +0000
/entries/Partial_Order_Reduction.html
-
Optimal Binary Search Trees
/entries/Optimal_BST.html
Sun, 27 May 2018 00:00:00 +0000
/entries/Optimal_BST.html
-
Optimal Binary Search Trees
/entries/Optimal_BST.html
Sun, 27 May 2018 00:00:00 +0000
/entries/Optimal_BST.html
-
Hidden Markov Models
/entries/Hidden_Markov_Models.html
Fri, 25 May 2018 00:00:00 +0000
/entries/Hidden_Markov_Models.html
-
Probabilistic Timed Automata
/entries/Probabilistic_Timed_Automata.html
Thu, 24 May 2018 00:00:00 +0000
/entries/Probabilistic_Timed_Automata.html
-
Monadification, Memoization and Dynamic Programming
/entries/Monad_Memo_DP.html
Tue, 22 May 2018 00:00:00 +0000
/entries/Monad_Memo_DP.html
-
Monadification, Memoization and Dynamic Programming
/entries/Monad_Memo_DP.html
Tue, 22 May 2018 00:00:00 +0000
/entries/Monad_Memo_DP.html
-
OpSets: Sequential Specifications for Replicated Datatypes
/entries/OpSets.html
Thu, 10 May 2018 00:00:00 +0000
/entries/OpSets.html
-
OpSets: Sequential Specifications for Replicated Datatypes
/entries/OpSets.html
Thu, 10 May 2018 00:00:00 +0000
/entries/OpSets.html
-
An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
/entries/Modular_Assembly_Kit_Security.html
Mon, 07 May 2018 00:00:00 +0000
/entries/Modular_Assembly_Kit_Security.html
-
WebAssembly
/entries/WebAssembly.html
Sun, 29 Apr 2018 00:00:00 +0000
/entries/WebAssembly.html
-
VerifyThis 2018 - Polished Isabelle Solutions
/entries/VerifyThis2018.html
Fri, 27 Apr 2018 00:00:00 +0000
/entries/VerifyThis2018.html
-
Bounded Natural Functors with Covariance and Contravariance
/entries/BNF_CC.html
Tue, 24 Apr 2018 00:00:00 +0000
/entries/BNF_CC.html
-
Weight-Balanced Trees
/entries/Weight_Balanced_Trees.html
Tue, 13 Mar 2018 00:00:00 +0000
/entries/Weight_Balanced_Trees.html
-
CakeML
/entries/CakeML.html
Mon, 12 Mar 2018 00:00:00 +0000
/entries/CakeML.html
-
A Theory of Architectural Design Patterns
/entries/Architectural_Design_Patterns.html
Thu, 01 Mar 2018 00:00:00 +0000
/entries/Architectural_Design_Patterns.html
-
Hoare Logics for Time Bounds
/entries/Hoare_Time.html
Mon, 26 Feb 2018 00:00:00 +0000
/entries/Hoare_Time.html
-
First-Order Terms
/entries/First_Order_Terms.html
Tue, 06 Feb 2018 00:00:00 +0000
/entries/First_Order_Terms.html
-
Treaps
/entries/Treaps.html
Tue, 06 Feb 2018 00:00:00 +0000
/entries/Treaps.html
-
A verified LLL algorithm
/entries/LLL_Basis_Reduction.html
Fri, 02 Feb 2018 00:00:00 +0000
/entries/LLL_Basis_Reduction.html
-
Taylor Models
/entries/Taylor_Models.html
Mon, 08 Jan 2018 00:00:00 +0000
/entries/Taylor_Models.html
-
Taylor Models
/entries/Taylor_Models.html
Mon, 08 Jan 2018 00:00:00 +0000
/entries/Taylor_Models.html
-
The Median-of-Medians Selection Algorithm
/entries/Median_Of_Medians_Selection.html
Thu, 21 Dec 2017 00:00:00 +0000
/entries/Median_Of_Medians_Selection.html
-
The string search algorithm by Knuth, Morris and Pratt
/entries/Knuth_Morris_Pratt.html
Mon, 18 Dec 2017 00:00:00 +0000
/entries/Knuth_Morris_Pratt.html
-
Stochastic Matrices and the Perron-Frobenius Theorem
/entries/Stochastic_Matrices.html
Wed, 22 Nov 2017 00:00:00 +0000
/entries/Stochastic_Matrices.html
-
The IMAP CmRDT
/entries/IMAP-CRDT.html
Thu, 09 Nov 2017 00:00:00 +0000
/entries/IMAP-CRDT.html
-
The IMAP CmRDT
/entries/IMAP-CRDT.html
Thu, 09 Nov 2017 00:00:00 +0000
/entries/IMAP-CRDT.html
-
BΓΌchi Complementation
/entries/Buchi_Complementation.html
Thu, 19 Oct 2017 00:00:00 +0000
/entries/Buchi_Complementation.html
-
Transition Systems and Automata
/entries/Transition_Systems_and_Automata.html
Thu, 19 Oct 2017 00:00:00 +0000
/entries/Transition_Systems_and_Automata.html
-
Homogeneous Linear Diophantine Equations
/entries/Diophantine_Eqns_Lin_Hom.html
Sat, 14 Oct 2017 00:00:00 +0000
/entries/Diophantine_Eqns_Lin_Hom.html
-
Root-Balanced Tree
/entries/Root_Balanced_Tree.html
Sun, 20 Aug 2017 00:00:00 +0000
/entries/Root_Balanced_Tree.html
-
The LambdaMu-calculus
/entries/LambdaMu.html
Wed, 16 Aug 2017 00:00:00 +0000
/entries/LambdaMu.html
-
Dynamic Architectures
/entries/DynamicArchitectures.html
Fri, 28 Jul 2017 00:00:00 +0000
/entries/DynamicArchitectures.html
-
Declarative Semantics for Functional Languages
/entries/Decl_Sem_Fun_PL.html
Fri, 21 Jul 2017 00:00:00 +0000
/entries/Decl_Sem_Fun_PL.html
-
HOLCF-Prelude
/entries/HOLCF-Prelude.html
Sat, 15 Jul 2017 00:00:00 +0000
/entries/HOLCF-Prelude.html
-
Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
/entries/Name_Carrying_Type_Inference.html
Sun, 09 Jul 2017 00:00:00 +0000
/entries/Name_Carrying_Type_Inference.html
-
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
/entries/CRDT.html
Fri, 07 Jul 2017 00:00:00 +0000
/entries/CRDT.html
-
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
/entries/CRDT.html
Fri, 07 Jul 2017 00:00:00 +0000
/entries/CRDT.html
-
Formalizing Push-Relabel Algorithms
/entries/Prpu_Maxflow.html
Thu, 01 Jun 2017 00:00:00 +0000
/entries/Prpu_Maxflow.html
-
Optics
/entries/Optics.html
Thu, 25 May 2017 00:00:00 +0000
/entries/Optics.html
-
Developing Security Protocols by Refinement
/entries/Security_Protocol_Refinement.html
Wed, 24 May 2017 00:00:00 +0000
/entries/Security_Protocol_Refinement.html
-
The Floyd-Warshall Algorithm for Shortest Paths
/entries/Floyd_Warshall.html
Mon, 08 May 2017 00:00:00 +0000
/entries/Floyd_Warshall.html
-
CryptHOL
/entries/CryptHOL.html
Fri, 05 May 2017 00:00:00 +0000
/entries/CryptHOL.html
-
CryptHOL
/entries/CryptHOL.html
Fri, 05 May 2017 00:00:00 +0000
/entries/CryptHOL.html
-
Effect polymorphism in higher-order logic
/entries/Monomorphic_Monad.html
Fri, 05 May 2017 00:00:00 +0000
/entries/Monomorphic_Monad.html
-
Game-based cryptography in HOL
/entries/Game_Based_Crypto.html
Fri, 05 May 2017 00:00:00 +0000
/entries/Game_Based_Crypto.html
-
Monad normalisation
/entries/Monad_Normalisation.html
Fri, 05 May 2017 00:00:00 +0000
/entries/Monad_Normalisation.html
-
Probabilistic while loop
/entries/Probabilistic_While.html
Fri, 05 May 2017 00:00:00 +0000
/entries/Probabilistic_While.html
-
Probabilistic while loop
/entries/Probabilistic_While.html
Fri, 05 May 2017 00:00:00 +0000
/entries/Probabilistic_While.html
-
Local Lexing
/entries/LocalLexing.html
Fri, 28 Apr 2017 00:00:00 +0000
/entries/LocalLexing.html
-
Expected Shape of Random Binary Search Trees
/entries/Random_BSTs.html
Tue, 04 Apr 2017 00:00:00 +0000
/entries/Random_BSTs.html
-
Expected Shape of Random Binary Search Trees
/entries/Random_BSTs.html
Tue, 04 Apr 2017 00:00:00 +0000
/entries/Random_BSTs.html
-
Lower bound on comparison-based sorting algorithms
/entries/Comparison_Sort_Lower_Bound.html
Wed, 15 Mar 2017 00:00:00 +0000
/entries/Comparison_Sort_Lower_Bound.html
-
The number of comparisons in QuickSort
/entries/Quick_Sort_Cost.html
Wed, 15 Mar 2017 00:00:00 +0000
/entries/Quick_Sort_Cost.html
-
The number of comparisons in QuickSort
/entries/Quick_Sort_Cost.html
Wed, 15 Mar 2017 00:00:00 +0000
/entries/Quick_Sort_Cost.html
-
The Group Law for Elliptic Curves
/entries/Elliptic_Curves_Group_Law.html
Tue, 28 Feb 2017 00:00:00 +0000
/entries/Elliptic_Curves_Group_Law.html
-
Differential Dynamic Logic
/entries/Differential_Dynamic_Logic.html
Mon, 13 Feb 2017 00:00:00 +0000
/entries/Differential_Dynamic_Logic.html
-
Refining Authenticated Key Agreement with Strong Adversaries
/entries/Key_Agreement_Strong_Adversaries.html
Tue, 31 Jan 2017 00:00:00 +0000
/entries/Key_Agreement_Strong_Adversaries.html
-
Minimal Static Single Assignment Form
/entries/Minimal_SSA.html
Tue, 17 Jan 2017 00:00:00 +0000
/entries/Minimal_SSA.html
-
Formal Network Models and Their Application to Firewall Policies
/entries/UPF_Firewall.html
Sun, 08 Jan 2017 00:00:00 +0000
/entries/UPF_Firewall.html
-
Formal Network Models and Their Application to Firewall Policies
/entries/UPF_Firewall.html
Sun, 08 Jan 2017 00:00:00 +0000
/entries/UPF_Firewall.html
-
Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
/entries/Password_Authentication_Protocol.html
Tue, 03 Jan 2017 00:00:00 +0000
/entries/Password_Authentication_Protocol.html
-
Concurrent Refinement Algebra and Rely Quotients
/entries/Concurrent_Ref_Alg.html
Fri, 30 Dec 2016 00:00:00 +0000
/entries/Concurrent_Ref_Alg.html
-
COMPLX: A Verification Framework for Concurrent Imperative Programs
/entries/Complx.html
Tue, 29 Nov 2016 00:00:00 +0000
/entries/Complx.html
-
COMPLX: A Verification Framework for Concurrent Imperative Programs
/entries/Complx.html
Tue, 29 Nov 2016 00:00:00 +0000
/entries/Complx.html
-
Abstract Interpretation of Annotated Commands
/entries/Abs_Int_ITP2012.html
Wed, 23 Nov 2016 00:00:00 +0000
/entries/Abs_Int_ITP2012.html
-
Separata: Isabelle tactics for Separation Algebra
/entries/Separata.html
Wed, 16 Nov 2016 00:00:00 +0000
/entries/Separata.html
-
Expressiveness of Deep Learning
/entries/Deep_Learning.html
Thu, 10 Nov 2016 00:00:00 +0000
/entries/Deep_Learning.html
-
Modal Logics for Nominal Transition Systems
/entries/Modal_Logics_for_NTS.html
Tue, 25 Oct 2016 00:00:00 +0000
/entries/Modal_Logics_for_NTS.html
-
LOFT β Verified Migration of Linux Firewalls to SDN
/entries/LOFT.html
Fri, 21 Oct 2016 00:00:00 +0000
/entries/LOFT.html
-
A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
/entries/SPARCv8.html
Wed, 19 Oct 2016 00:00:00 +0000
/entries/SPARCv8.html
-
A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
/entries/SPARCv8.html
Wed, 19 Oct 2016 00:00:00 +0000
/entries/SPARCv8.html
-
FisherβYates shuffle
/entries/Fisher_Yates.html
Fri, 30 Sep 2016 00:00:00 +0000
/entries/Fisher_Yates.html
-
Iptables Semantics
/entries/Iptables_Semantics.html
Fri, 09 Sep 2016 00:00:00 +0000
/entries/Iptables_Semantics.html
-
Routing
/entries/Routing.html
Wed, 31 Aug 2016 00:00:00 +0000
/entries/Routing.html
-
Simple Firewall
/entries/Simple_Firewall.html
Wed, 24 Aug 2016 00:00:00 +0000
/entries/Simple_Firewall.html
-
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
/entries/InfPathElimination.html
Thu, 18 Aug 2016 00:00:00 +0000
/entries/InfPathElimination.html
-
Formalizing the Edmonds-Karp Algorithm
/entries/EdmondsKarp_Maxflow.html
Fri, 12 Aug 2016 00:00:00 +0000
/entries/EdmondsKarp_Maxflow.html
-
The Imperative Refinement Framework
/entries/Refine_Imperative_HOL.html
Mon, 08 Aug 2016 00:00:00 +0000
/entries/Refine_Imperative_HOL.html
-
The Imperative Refinement Framework
/entries/Refine_Imperative_HOL.html
Mon, 08 Aug 2016 00:00:00 +0000
/entries/Refine_Imperative_HOL.html
-
Pairing Heap
/entries/Pairing_Heap.html
Thu, 14 Jul 2016 00:00:00 +0000
/entries/Pairing_Heap.html
-
A Framework for Verifying Depth-First Search Algorithms
/entries/DFS_Framework.html
Tue, 05 Jul 2016 00:00:00 +0000
/entries/DFS_Framework.html
-
Compositional Security-Preserving Refinement for Concurrent Imperative Programs
/entries/Dependent_SIFUM_Refinement.html
Tue, 28 Jun 2016 00:00:00 +0000
/entries/Dependent_SIFUM_Refinement.html
-
IP Addresses
/entries/IP_Addresses.html
Tue, 28 Jun 2016 00:00:00 +0000
/entries/IP_Addresses.html
-
A Dependent Security Type System for Concurrent Imperative Programs
/entries/Dependent_SIFUM_Type_Systems.html
Sat, 25 Jun 2016 00:00:00 +0000
/entries/Dependent_SIFUM_Type_Systems.html
-
A Dependent Security Type System for Concurrent Imperative Programs
/entries/Dependent_SIFUM_Type_Systems.html
Sat, 25 Jun 2016 00:00:00 +0000
/entries/Dependent_SIFUM_Type_Systems.html
-
Conservation of CSP Noninterference Security under Concurrent Composition
/entries/Noninterference_Concurrent_Composition.html
Mon, 13 Jun 2016 00:00:00 +0000
/entries/Noninterference_Concurrent_Composition.html
-
Conservation of CSP Noninterference Security under Concurrent Composition
/entries/Noninterference_Concurrent_Composition.html
Mon, 13 Jun 2016 00:00:00 +0000
/entries/Noninterference_Concurrent_Composition.html
-
Finite Machine Word Library
/entries/Word_Lib.html
Thu, 09 Jun 2016 00:00:00 +0000
/entries/Word_Lib.html
-
POSIX Lexing with Derivatives of Regular Expressions
/entries/Posix-Lexing.html
Tue, 24 May 2016 00:00:00 +0000
/entries/Posix-Lexing.html
-
A Constructive Proof for FLP
/entries/FLP.html
Wed, 18 May 2016 00:00:00 +0000
/entries/FLP.html
-
GrΓΆbner Bases Theory
/entries/Groebner_Bases.html
Mon, 02 May 2016 00:00:00 +0000
/entries/Groebner_Bases.html
-
A formalisation of the Cocke-Younger-Kasami algorithm
/entries/CYK.html
Wed, 27 Apr 2016 00:00:00 +0000
/entries/CYK.html
-
A formalisation of the Cocke-Younger-Kasami algorithm
/entries/CYK.html
Wed, 27 Apr 2016 00:00:00 +0000
/entries/CYK.html
-
Algorithms for Reduced Ordered Binary Decision Diagrams
/entries/ROBDD.html
Wed, 27 Apr 2016 00:00:00 +0000
/entries/ROBDD.html
-
Algorithms for Reduced Ordered Binary Decision Diagrams
/entries/ROBDD.html
Wed, 27 Apr 2016 00:00:00 +0000
/entries/ROBDD.html
-
Conservation of CSP Noninterference Security under Sequential Composition
/entries/Noninterference_Sequential_Composition.html
Tue, 26 Apr 2016 00:00:00 +0000
/entries/Noninterference_Sequential_Composition.html
-
Conservation of CSP Noninterference Security under Sequential Composition
/entries/Noninterference_Sequential_Composition.html
Tue, 26 Apr 2016 00:00:00 +0000
/entries/Noninterference_Sequential_Composition.html
-
Kleene Algebras with Domain
/entries/KAD.html
Tue, 12 Apr 2016 00:00:00 +0000
/entries/KAD.html
-
Kleene Algebras with Domain
/entries/KAD.html
Tue, 12 Apr 2016 00:00:00 +0000
/entries/KAD.html
-
Timed Automata
/entries/Timed_Automata.html
Tue, 08 Mar 2016 00:00:00 +0000
/entries/Timed_Automata.html
-
Linear Temporal Logic
/entries/LTL.html
Tue, 01 Mar 2016 00:00:00 +0000
/entries/LTL.html
-
Analysis of List Update Algorithms
/entries/List_Update.html
Wed, 17 Feb 2016 00:00:00 +0000
/entries/List_Update.html
-
Analysis of List Update Algorithms
/entries/List_Update.html
Wed, 17 Feb 2016 00:00:00 +0000
/entries/List_Update.html
-
Verified Construction of Static Single Assignment Form
/entries/Formal_SSA.html
Fri, 05 Feb 2016 00:00:00 +0000
/entries/Formal_SSA.html
-
Tensor Product of Matrices
/entries/Matrix_Tensor.html
Mon, 18 Jan 2016 00:00:00 +0000
/entries/Matrix_Tensor.html
-
Applicative Lifting
/entries/Applicative_Lifting.html
Tue, 22 Dec 2015 00:00:00 +0000
/entries/Applicative_Lifting.html
-
The Tortoise and Hare Algorithm
/entries/TortoiseHare.html
Wed, 18 Nov 2015 00:00:00 +0000
/entries/TortoiseHare.html
-
A Meta-Model for the Isabelle API
/entries/Isabelle_Meta_Model.html
Wed, 16 Sep 2015 00:00:00 +0000
/entries/Isabelle_Meta_Model.html
-
Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata
/entries/LTL_to_DRA.html
Fri, 04 Sep 2015 00:00:00 +0000
/entries/LTL_to_DRA.html
-
The Inductive Unwinding Theorem for CSP Noninterference Security
/entries/Noninterference_Inductive_Unwinding.html
Tue, 18 Aug 2015 00:00:00 +0000
/entries/Noninterference_Inductive_Unwinding.html
-
Analysing and Comparing Encodability Criteria for Process Calculi
/entries/Encodability_Process_Calculi.html
Mon, 10 Aug 2015 00:00:00 +0000
/entries/Encodability_Process_Calculi.html
-
Generating Cases from Labeled Subgoals
/entries/Case_Labeling.html
Tue, 21 Jul 2015 00:00:00 +0000
/entries/Case_Labeling.html
-
Hermite Normal Form
/entries/Hermite.html
Tue, 07 Jul 2015 00:00:00 +0000
/entries/Hermite.html
-
Reasoning about Lists via List Interleaving
/entries/List_Interleaving.html
Thu, 11 Jun 2015 00:00:00 +0000
/entries/List_Interleaving.html
-
The Generic Unwinding Theorem for CSP Noninterference Security
/entries/Noninterference_Generic_Unwinding.html
Thu, 11 Jun 2015 00:00:00 +0000
/entries/Noninterference_Generic_Unwinding.html
-
The Generic Unwinding Theorem for CSP Noninterference Security
/entries/Noninterference_Generic_Unwinding.html
Thu, 11 Jun 2015 00:00:00 +0000
/entries/Noninterference_Generic_Unwinding.html
-
The Ipurge Unwinding Theorem for CSP Noninterference Security
/entries/Noninterference_Ipurge_Unwinding.html
Thu, 11 Jun 2015 00:00:00 +0000
/entries/Noninterference_Ipurge_Unwinding.html
-
Parameterized Dynamic Tables
/entries/Dynamic_Tables.html
Sun, 07 Jun 2015 00:00:00 +0000
/entries/Dynamic_Tables.html
-
Derivatives of Logical Formulas
/entries/Formula_Derivatives.html
Thu, 28 May 2015 00:00:00 +0000
/entries/Formula_Derivatives.html
-
A Zoo of Probabilistic Systems
/entries/Probabilistic_System_Zoo.html
Wed, 27 May 2015 00:00:00 +0000
/entries/Probabilistic_System_Zoo.html
-
Concurrent IMP
/entries/ConcurrentIMP.html
Mon, 13 Apr 2015 00:00:00 +0000
/entries/ConcurrentIMP.html
-
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
/entries/ConcurrentGC.html
Mon, 13 Apr 2015 00:00:00 +0000
/entries/ConcurrentGC.html
-
Trie
/entries/Trie.html
Mon, 30 Mar 2015 00:00:00 +0000
/entries/Trie.html
-
Consensus Refined
/entries/Consensus_Refined.html
Wed, 18 Mar 2015 00:00:00 +0000
/entries/Consensus_Refined.html
-
Deriving class instances for datatypes
/entries/Deriving.html
Wed, 11 Mar 2015 00:00:00 +0000
/entries/Deriving.html
-
The Safety of Call Arity
/entries/Call_Arity.html
Fri, 20 Feb 2015 00:00:00 +0000
/entries/Call_Arity.html
-
Echelon Form
/entries/Echelon_Form.html
Thu, 12 Feb 2015 00:00:00 +0000
/entries/Echelon_Form.html
-
QR Decomposition
/entries/QR_Decomposition.html
Thu, 12 Feb 2015 00:00:00 +0000
/entries/QR_Decomposition.html
-
Finite Automata in Hereditarily Finite Set Theory
/entries/Finite_Automata_HF.html
Thu, 05 Feb 2015 00:00:00 +0000
/entries/Finite_Automata_HF.html
-
Verification of the UpDown Scheme
/entries/UpDown_Scheme.html
Wed, 28 Jan 2015 00:00:00 +0000
/entries/UpDown_Scheme.html
-
The Unified Policy Framework (UPF)
/entries/UPF.html
Fri, 28 Nov 2014 00:00:00 +0000
/entries/UPF.html
-
Loop freedom of the (untimed) AODV routing protocol
/entries/AODV.html
Thu, 23 Oct 2014 00:00:00 +0000
/entries/AODV.html
-
Lifting Definition Option
/entries/Lifting_Definition_Option.html
Mon, 13 Oct 2014 00:00:00 +0000
/entries/Lifting_Definition_Option.html
-
Stream Fusion in HOL with Code Generation
/entries/Stream_Fusion_Code.html
Fri, 10 Oct 2014 00:00:00 +0000
/entries/Stream_Fusion_Code.html
-
A Verified Compiler for Probability Density Functions
/entries/Density_Compiler.html
Thu, 09 Oct 2014 00:00:00 +0000
/entries/Density_Compiler.html
-
Formalization of Refinement Calculus for Reactive Systems
/entries/RefinementReactive.html
Wed, 08 Oct 2014 00:00:00 +0000
/entries/RefinementReactive.html
-
Certification Monads
/entries/Certification_Monads.html
Fri, 03 Oct 2014 00:00:00 +0000
/entries/Certification_Monads.html
-
XML
/entries/XML.html
Fri, 03 Oct 2014 00:00:00 +0000
/entries/XML.html
-
XML
/entries/XML.html
Fri, 03 Oct 2014 00:00:00 +0000
/entries/XML.html
-
Imperative Insertion Sort
/entries/Imperative_Insertion_Sort.html
Thu, 25 Sep 2014 00:00:00 +0000
/entries/Imperative_Insertion_Sort.html
-
Priority Queues Based on Braun Trees
/entries/Priority_Queue_Braun.html
Thu, 04 Sep 2014 00:00:00 +0000
/entries/Priority_Queue_Braun.html
-
Gauss-Jordan Algorithm and Its Applications
/entries/Gauss_Jordan.html
Wed, 03 Sep 2014 00:00:00 +0000
/entries/Gauss_Jordan.html
-
Skew Heap
/entries/Skew_Heap.html
Wed, 13 Aug 2014 00:00:00 +0000
/entries/Skew_Heap.html
-
Splay Tree
/entries/Splay_Tree.html
Tue, 12 Aug 2014 00:00:00 +0000
/entries/Splay_Tree.html
-
Haskell's Show Class in Isabelle/HOL
/entries/Show.html
Tue, 29 Jul 2014 00:00:00 +0000
/entries/Show.html
-
Formal Specification of a Generic Separation Kernel
/entries/CISC-Kernel.html
Fri, 18 Jul 2014 00:00:00 +0000
/entries/CISC-Kernel.html
-
pGCL for Isabelle
/entries/pGCL.html
Sun, 13 Jul 2014 00:00:00 +0000
/entries/pGCL.html
-
Amortized Complexity Verified
/entries/Amortized_Complexity.html
Mon, 07 Jul 2014 00:00:00 +0000
/entries/Amortized_Complexity.html
-
Network Security Policy Verification
/entries/Network_Security_Policy_Verification.html
Fri, 04 Jul 2014 00:00:00 +0000
/entries/Network_Security_Policy_Verification.html
-
Pop-Refinement
/entries/Pop_Refinement.html
Thu, 03 Jul 2014 00:00:00 +0000
/entries/Pop_Refinement.html
-
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
/entries/MSO_Regex_Equivalence.html
Thu, 12 Jun 2014 00:00:00 +0000
/entries/MSO_Regex_Equivalence.html
-
Boolean Expression Checkers
/entries/Boolean_Expression_Checkers.html
Sun, 08 Jun 2014 00:00:00 +0000
/entries/Boolean_Expression_Checkers.html
-
A Fully Verified Executable LTL Model Checker
/entries/CAVA_LTL_Modelchecker.html
Wed, 28 May 2014 00:00:00 +0000
/entries/CAVA_LTL_Modelchecker.html
-
Converting Linear-Time Temporal Logic to Generalized BΓΌchi Automata
/entries/LTL_to_GBA.html
Wed, 28 May 2014 00:00:00 +0000
/entries/LTL_to_GBA.html
-
Promela Formalization
/entries/Promela.html
Wed, 28 May 2014 00:00:00 +0000
/entries/Promela.html
-
The CAVA Automata Library
/entries/CAVA_Automata.html
Wed, 28 May 2014 00:00:00 +0000
/entries/CAVA_Automata.html
-
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
/entries/Gabow_SCC.html
Wed, 28 May 2014 00:00:00 +0000
/entries/Gabow_SCC.html
-
Noninterference Security in Communicating Sequential Processes
/entries/Noninterference_CSP.html
Fri, 23 May 2014 00:00:00 +0000
/entries/Noninterference_CSP.html
-
Transitive closure according to Roy-Floyd-Warshall
/entries/Roy_Floyd_Warshall.html
Fri, 23 May 2014 00:00:00 +0000
/entries/Roy_Floyd_Warshall.html
-
Regular Algebras
/entries/Regular_Algebras.html
Wed, 21 May 2014 00:00:00 +0000
/entries/Regular_Algebras.html
-
Formalisation and Analysis of Component Dependencies
/entries/ComponentDependencies.html
Mon, 28 Apr 2014 00:00:00 +0000
/entries/ComponentDependencies.html
-
A Formalization of Assumptions and Guarantees for Compositional Noninterference
/entries/SIFUM_Type_Systems.html
Wed, 23 Apr 2014 00:00:00 +0000
/entries/SIFUM_Type_Systems.html
-
A Formalization of Assumptions and Guarantees for Compositional Noninterference
/entries/SIFUM_Type_Systems.html
Wed, 23 Apr 2014 00:00:00 +0000
/entries/SIFUM_Type_Systems.html
-
A Formalization of Declassification with WHAT-and-WHERE-Security
/entries/WHATandWHERE_Security.html
Wed, 23 Apr 2014 00:00:00 +0000
/entries/WHATandWHERE_Security.html
-
A Formalization of Declassification with WHAT-and-WHERE-Security
/entries/WHATandWHERE_Security.html
Wed, 23 Apr 2014 00:00:00 +0000
/entries/WHATandWHERE_Security.html
-
A Formalization of Strong Security
/entries/Strong_Security.html
Wed, 23 Apr 2014 00:00:00 +0000
/entries/Strong_Security.html
-
A Formalization of Strong Security
/entries/Strong_Security.html
Wed, 23 Apr 2014 00:00:00 +0000
/entries/Strong_Security.html
-
Bounded-Deducibility Security
/entries/Bounded_Deducibility_Security.html
Tue, 22 Apr 2014 00:00:00 +0000
/entries/Bounded_Deducibility_Security.html
-
A shallow embedding of HyperCTL*
/entries/HyperCTL.html
Wed, 16 Apr 2014 00:00:00 +0000
/entries/HyperCTL.html
-
Syntax and semantics of a GPU kernel programming language
/entries/GPU_Kernel_PL.html
Thu, 03 Apr 2014 00:00:00 +0000
/entries/GPU_Kernel_PL.html
-
Probabilistic Noninterference
/entries/Probabilistic_Noninterference.html
Tue, 11 Mar 2014 00:00:00 +0000
/entries/Probabilistic_Noninterference.html
-
Mechanization of the Algebra for Wireless Networks (AWN)
/entries/AWN.html
Sat, 08 Mar 2014 00:00:00 +0000
/entries/AWN.html
-
Mutually Recursive Partial Functions
/entries/Partial_Function_MR.html
Tue, 18 Feb 2014 00:00:00 +0000
/entries/Partial_Function_MR.html
-
Verification of Selection and Heap Sort Using Locales
/entries/Selection_Heap_Sort.html
Tue, 11 Feb 2014 00:00:00 +0000
/entries/Selection_Heap_Sort.html
-
Unified Decision Procedures for Regular Expression Equivalence
/entries/Regex_Equivalence.html
Thu, 30 Jan 2014 00:00:00 +0000
/entries/Regex_Equivalence.html
-
Kleene Algebra with Tests and Demonic Refinement Algebras
/entries/KAT_and_DRA.html
Thu, 23 Jan 2014 00:00:00 +0000
/entries/KAT_and_DRA.html
-
Kleene Algebra with Tests and Demonic Refinement Algebras
/entries/KAT_and_DRA.html
Thu, 23 Jan 2014 00:00:00 +0000
/entries/KAT_and_DRA.html
-
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
/entries/Featherweight_OCL.html
Thu, 16 Jan 2014 00:00:00 +0000
/entries/Featherweight_OCL.html
-
Compositional Properties of Crypto-Based Components
/entries/CryptoBasedCompositionalProperties.html
Sat, 11 Jan 2014 00:00:00 +0000
/entries/CryptoBasedCompositionalProperties.html
-
A General Method for the Proof of Theorems on Tail-recursive Functions
/entries/Tail_Recursive_Functions.html
Sun, 01 Dec 2013 00:00:00 +0000
/entries/Tail_Recursive_Functions.html
-
A Codatatype of Formal Languages
/entries/Coinductive_Languages.html
Fri, 15 Nov 2013 00:00:00 +0000
/entries/Coinductive_Languages.html
-
Stream Processing Components: Isabelle/HOL Formalisation and Case Studies
/entries/FocusStreamsCaseStudies.html
Thu, 14 Nov 2013 00:00:00 +0000
/entries/FocusStreamsCaseStudies.html
-
Automatic Data Refinement
/entries/Automatic_Refinement.html
Wed, 02 Oct 2013 00:00:00 +0000
/entries/Automatic_Refinement.html
-
Native Word
/entries/Native_Word.html
Tue, 17 Sep 2013 00:00:00 +0000
/entries/Native_Word.html
-
A Formal Model of IEEE Floating Point Arithmetic
/entries/IEEE_Floating_Point.html
Sat, 27 Jul 2013 00:00:00 +0000
/entries/IEEE_Floating_Point.html
-
Light-weight Containers
/entries/Containers.html
Mon, 15 Apr 2013 00:00:00 +0000
/entries/Containers.html
-
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
/entries/Launchbury.html
Thu, 31 Jan 2013 00:00:00 +0000
/entries/Launchbury.html
-
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
/entries/Launchbury.html
Thu, 31 Jan 2013 00:00:00 +0000
/entries/Launchbury.html
-
Ribbon Proofs
/entries/Ribbon_Proofs.html
Sat, 19 Jan 2013 00:00:00 +0000
/entries/Ribbon_Proofs.html
-
Kleene Algebra
/entries/Kleene_Algebra.html
Tue, 15 Jan 2013 00:00:00 +0000
/entries/Kleene_Algebra.html
-
Kleene Algebra
/entries/Kleene_Algebra.html
Tue, 15 Jan 2013 00:00:00 +0000
/entries/Kleene_Algebra.html
-
A Separation Logic Framework for Imperative HOL
/entries/Separation_Logic_Imperative_HOL.html
Wed, 14 Nov 2012 00:00:00 +0000
/entries/Separation_Logic_Imperative_HOL.html
-
Possibilistic Noninterference
/entries/Possibilistic_Noninterference.html
Mon, 10 Sep 2012 00:00:00 +0000
/entries/Possibilistic_Noninterference.html
-
Possibilistic Noninterference
/entries/Possibilistic_Noninterference.html
Mon, 10 Sep 2012 00:00:00 +0000
/entries/Possibilistic_Noninterference.html
-
Generating linear orders for datatypes
/entries/Datatype_Order_Generator.html
Tue, 07 Aug 2012 00:00:00 +0000
/entries/Datatype_Order_Generator.html
-
Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
/entries/Heard_Of.html
Fri, 27 Jul 2012 00:00:00 +0000
/entries/Heard_Of.html
-
Logical Relations for PCF
/entries/PCF.html
Sun, 01 Jul 2012 00:00:00 +0000
/entries/PCF.html
-
Type Constructor Classes and Monad Transformers
/entries/Tycon.html
Tue, 26 Jun 2012 00:00:00 +0000
/entries/Tycon.html
-
CCS in nominal logic
/entries/CCS.html
Tue, 29 May 2012 00:00:00 +0000
/entries/CCS.html
-
Psi-calculi in Isabelle
/entries/Psi_Calculi.html
Tue, 29 May 2012 00:00:00 +0000
/entries/Psi_Calculi.html
-
The pi-calculus in nominal logic
/entries/Pi_Calculus.html
Tue, 29 May 2012 00:00:00 +0000
/entries/Pi_Calculus.html
-
Isabelle/Circus
/entries/Circus.html
Sun, 27 May 2012 00:00:00 +0000
/entries/Circus.html
-
Isabelle/Circus
/entries/Circus.html
Sun, 27 May 2012 00:00:00 +0000
/entries/Circus.html
-
Separation Algebra
/entries/Separation_Algebra.html
Fri, 11 May 2012 00:00:00 +0000
/entries/Separation_Algebra.html
-
Stuttering Equivalence
/entries/Stuttering_Equivalence.html
Mon, 07 May 2012 00:00:00 +0000
/entries/Stuttering_Equivalence.html
-
Inductive Study of Confidentiality
/entries/Inductive_Confidentiality.html
Wed, 02 May 2012 00:00:00 +0000
/entries/Inductive_Confidentiality.html
-
Abortable Linearizable Modules
/entries/Abortable_Linearizable_Modules.html
Thu, 01 Mar 2012 00:00:00 +0000
/entries/Abortable_Linearizable_Modules.html
-
Executable Transitive Closures
/entries/Transitive-Closure-II.html
Wed, 29 Feb 2012 00:00:00 +0000
/entries/Transitive-Closure-II.html
-
Dijkstra's Shortest Path Algorithm
/entries/Dijkstra_Shortest_Path.html
Mon, 30 Jan 2012 00:00:00 +0000
/entries/Dijkstra_Shortest_Path.html
-
Refinement for Monadic Programs
/entries/Refine_Monadic.html
Mon, 30 Jan 2012 00:00:00 +0000
/entries/Refine_Monadic.html
-
Markov Models
/entries/Markov_Models.html
Tue, 03 Jan 2012 00:00:00 +0000
/entries/Markov_Models.html
-
A Definitional Encoding of TLA* in Isabelle/HOL
/entries/TLA.html
Sat, 19 Nov 2011 00:00:00 +0000
/entries/TLA.html
-
Efficient Mergesort
/entries/Efficient-Mergesort.html
Wed, 09 Nov 2011 00:00:00 +0000
/entries/Efficient-Mergesort.html
-
Algebra of Monotonic Boolean Transformers
/entries/MonoBoolTranAlgebra.html
Thu, 22 Sep 2011 00:00:00 +0000
/entries/MonoBoolTranAlgebra.html
-
The Myhill-Nerode Theorem Based on Regular Expressions
/entries/Myhill-Nerode.html
Fri, 26 Aug 2011 00:00:00 +0000
/entries/Myhill-Nerode.html
-
Gauss-Jordan Elimination for Matrices Represented as Functions
/entries/Gauss-Jordan-Elim-Fun.html
Fri, 19 Aug 2011 00:00:00 +0000
/entries/Gauss-Jordan-Elim-Fun.html
-
Knowledge-based programs
/entries/KBPs.html
Tue, 17 May 2011 00:00:00 +0000
/entries/KBPs.html
-
Executable Transitive Closures of Finite Relations
/entries/Transitive-Closure.html
Mon, 14 Mar 2011 00:00:00 +0000
/entries/Transitive-Closure.html
-
AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
/entries/AutoFocus-Stream.html
Wed, 23 Feb 2011 00:00:00 +0000
/entries/AutoFocus-Stream.html
-
Infinite Lists
/entries/List-Infinite.html
Wed, 23 Feb 2011 00:00:00 +0000
/entries/List-Infinite.html
-
Lightweight Java
/entries/LightweightJava.html
Mon, 07 Feb 2011 00:00:00 +0000
/entries/LightweightJava.html
-
RIPEMD-160
/entries/RIPEMD-160-SPARK.html
Mon, 10 Jan 2011 00:00:00 +0000
/entries/RIPEMD-160-SPARK.html
-
Shivers' Control Flow Analysis
/entries/Shivers-CFA.html
Tue, 16 Nov 2010 00:00:00 +0000
/entries/Shivers-CFA.html
-
Binomial Heaps and Skew Binomial Heaps
/entries/Binomial-Heaps.html
Thu, 28 Oct 2010 00:00:00 +0000
/entries/Binomial-Heaps.html
-
Finger Trees
/entries/Finger-Trees.html
Thu, 28 Oct 2010 00:00:00 +0000
/entries/Finger-Trees.html
-
Functional Binomial Queues
/entries/Binomial-Queues.html
Thu, 28 Oct 2010 00:00:00 +0000
/entries/Binomial-Queues.html
-
Strong Normalization of Moggis's Computational Metalanguage
/entries/Lam-ml-Normalization.html
Sun, 29 Aug 2010 00:00:00 +0000
/entries/Lam-ml-Normalization.html
-
Executable Multivariate Polynomials
/entries/Polynomials.html
Tue, 10 Aug 2010 00:00:00 +0000
/entries/Polynomials.html
-
Formalizing Statecharts using Hierarchical Automata
/entries/Statecharts.html
Sun, 08 Aug 2010 00:00:00 +0000
/entries/Statecharts.html
-
Executable Matrix Operations on Matrices of Arbitrary Dimensions
/entries/Matrix.html
Thu, 17 Jun 2010 00:00:00 +0000
/entries/Matrix.html
-
Semantics and Data Refinement of Invariant Based Programs
/entries/DataRefinementIBP.html
Fri, 28 May 2010 00:00:00 +0000
/entries/DataRefinementIBP.html
-
Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
/entries/GraphMarkingIBP.html
Fri, 28 May 2010 00:00:00 +0000
/entries/GraphMarkingIBP.html
-
Regular Sets and Expressions
/entries/Regular-Sets.html
Wed, 12 May 2010 00:00:00 +0000
/entries/Regular-Sets.html
-
Locally Nameless Sigma Calculus
/entries/Locally-Nameless-Sigma.html
Fri, 30 Apr 2010 00:00:00 +0000
/entries/Locally-Nameless-Sigma.html
-
Information Flow Noninterference via Slicing
/entries/InformationFlowSlicing.html
Tue, 23 Mar 2010 00:00:00 +0000
/entries/InformationFlowSlicing.html
-
Inter-Procedural Information Flow Noninterference via Slicing
/entries/InformationFlowSlicing_Inter.html
Tue, 23 Mar 2010 00:00:00 +0000
/entries/InformationFlowSlicing_Inter.html
-
List Index
/entries/List-Index.html
Sat, 20 Feb 2010 00:00:00 +0000
/entries/List-Index.html
-
Coinductive
/entries/Coinductive.html
Fri, 12 Feb 2010 00:00:00 +0000
/entries/Coinductive.html
-
Formalizing the Logic-Automaton Connection
/entries/Presburger-Automata.html
Thu, 03 Dec 2009 00:00:00 +0000
/entries/Presburger-Automata.html
-
Collections Framework
/entries/Collections.html
Wed, 25 Nov 2009 00:00:00 +0000
/entries/Collections.html
-
Tree Automata
/entries/Tree-Automata.html
Wed, 25 Nov 2009 00:00:00 +0000
/entries/Tree-Automata.html
-
Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer
/entries/HRB-Slicing.html
Fri, 13 Nov 2009 00:00:00 +0000
/entries/HRB-Slicing.html
-
The Worker/Wrapper Transformation
/entries/WorkerWrapper.html
Fri, 30 Oct 2009 00:00:00 +0000
/entries/WorkerWrapper.html
-
Code Generation for Functions as Data
/entries/FinFun.html
Wed, 06 May 2009 00:00:00 +0000
/entries/FinFun.html
-
Stream Fusion
/entries/Stream-Fusion.html
Wed, 29 Apr 2009 00:00:00 +0000
/entries/Stream-Fusion.html
-
A Bytecode Logic for JML and Types
/entries/BytecodeLogicJmlTypes.html
Fri, 12 Dec 2008 00:00:00 +0000
/entries/BytecodeLogicJmlTypes.html
-
Secure information flow and program logics
/entries/SIFPL.html
Mon, 10 Nov 2008 00:00:00 +0000
/entries/SIFPL.html
-
Secure information flow and program logics
/entries/SIFPL.html
Mon, 10 Nov 2008 00:00:00 +0000
/entries/SIFPL.html
-
The Textbook Proof of Huffman's Algorithm
/entries/Huffman.html
Wed, 15 Oct 2008 00:00:00 +0000
/entries/Huffman.html
-
Towards Certified Slicing
/entries/Slicing.html
Tue, 16 Sep 2008 00:00:00 +0000
/entries/Slicing.html
-
A Correctness Proof for the Volpano/Smith Security Typing System
/entries/VolpanoSmith.html
Tue, 02 Sep 2008 00:00:00 +0000
/entries/VolpanoSmith.html
-
A Correctness Proof for the Volpano/Smith Security Typing System
/entries/VolpanoSmith.html
Tue, 02 Sep 2008 00:00:00 +0000
/entries/VolpanoSmith.html
-
Formal Verification of Modern SAT Solvers
/entries/SATSolverVerification.html
Wed, 23 Jul 2008 00:00:00 +0000
/entries/SATSolverVerification.html
-
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
/entries/Simpl.html
Fri, 29 Feb 2008 00:00:00 +0000
/entries/Simpl.html
-
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
/entries/Simpl.html
Fri, 29 Feb 2008 00:00:00 +0000
/entries/Simpl.html
-
BDD Normalisation
/entries/BDD.html
Fri, 29 Feb 2008 00:00:00 +0000
/entries/BDD.html
-
Normalization by Evaluation
/entries/NormByEval.html
Mon, 18 Feb 2008 00:00:00 +0000
/entries/NormByEval.html
-
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors
/entries/Program-Conflict-Analysis.html
Fri, 14 Dec 2007 00:00:00 +0000
/entries/Program-Conflict-Analysis.html
-
Jinja with Threads
/entries/JinjaThreads.html
Mon, 03 Dec 2007 00:00:00 +0000
/entries/JinjaThreads.html
-
Much Ado About Two
/entries/MuchAdoAboutTwo.html
Tue, 06 Nov 2007 00:00:00 +0000
/entries/MuchAdoAboutTwo.html
-
POPLmark Challenge Via de Bruijn Indices
/entries/POPLmark-deBruijn.html
Thu, 02 Aug 2007 00:00:00 +0000
/entries/POPLmark-deBruijn.html
-
Hotel Key Card System
/entries/HotelKeyCards.html
Sat, 09 Sep 2006 00:00:00 +0000
/entries/HotelKeyCards.html
-
Abstract Hoare Logics
/entries/Abstract-Hoare-Logics.html
Tue, 08 Aug 2006 00:00:00 +0000
/entries/Abstract-Hoare-Logics.html
-
CoreC++
/entries/CoreC++.html
Mon, 15 May 2006 00:00:00 +0000
/entries/CoreC++.html
-
A Theory of Featherweight Java in Isabelle/HOL
/entries/FeatherweightJava.html
Fri, 31 Mar 2006 00:00:00 +0000
/entries/FeatherweightJava.html
-
Instances of Schneider's generalized protocol of clock synchronization
/entries/ClockSynchInst.html
Wed, 15 Mar 2006 00:00:00 +0000
/entries/ClockSynchInst.html
-
Fast Fourier Transform
/entries/FFT.html
Wed, 12 Oct 2005 00:00:00 +0000
/entries/FFT.html
-
Formalization of a Generalized Protocol for Clock Synchronization
/entries/GenClock.html
Fri, 24 Jun 2005 00:00:00 +0000
/entries/GenClock.html
-
Proving the Correctness of Disk Paxos
/entries/DiskPaxos.html
Wed, 22 Jun 2005 00:00:00 +0000
/entries/DiskPaxos.html
-
Jive Data and Store Model
/entries/JiveDataStoreModel.html
Mon, 20 Jun 2005 00:00:00 +0000
/entries/JiveDataStoreModel.html
-
Jinja is not Java
/entries/Jinja.html
Wed, 01 Jun 2005 00:00:00 +0000
/entries/Jinja.html
-
SHA1, RSA, PSS and more
/entries/RSAPSS.html
Mon, 02 May 2005 00:00:00 +0000
/entries/RSAPSS.html
-
File Refinement
/entries/FileRefinement.html
Thu, 09 Dec 2004 00:00:00 +0000
/entries/FileRefinement.html
-
Compiling Exceptions Correctly
/entries/Compiling-Exceptions-Correctly.html
Fri, 09 Jul 2004 00:00:00 +0000
/entries/Compiling-Exceptions-Correctly.html
-
Depth First Search
/entries/Depth-First-Search.html
Thu, 24 Jun 2004 00:00:00 +0000
/entries/Depth-First-Search.html
-
Lazy Lists II
/entries/Lazy-Lists-II.html
Mon, 26 Apr 2004 00:00:00 +0000
/entries/Lazy-Lists-II.html
-
Binary Search Trees
/entries/BinarySearchTree.html
Mon, 05 Apr 2004 00:00:00 +0000
/entries/BinarySearchTree.html
-
Functional Automata
/entries/Functional-Automata.html
Tue, 30 Mar 2004 00:00:00 +0000
/entries/Functional-Automata.html
-
AVL Trees
/entries/AVL-Trees.html
Fri, 19 Mar 2004 00:00:00 +0000
/entries/AVL-Trees.html
-
Mini ML
/entries/MiniML.html
Fri, 19 Mar 2004 00:00:00 +0000
/entries/MiniML.html
diff --git a/web/topics/index.html b/web/topics/index.html
--- a/web/topics/index.html
+++ b/web/topics/index.html
@@ -1,121 +1,121 @@
Archive of Formal Proofs
\ No newline at end of file