Computer science/Data structures

Subject Classification

ACM: Theory of computation~Data structures design and analysis

AMS: Computer science / Theory of data / Data structures

2025

Power Operator for Lists

by Štěpán Holub, Martin Raška, Štěpán Starosta and Tobias Nipkow

Jan 29

2024

Formally Verified Suffix Array Construction

by Louis Cheung and Christine Rizkallah

Sep 25

Difference Bound Matrices

by Simon Wimmer and Peter Lammich

Aug 14

Region Quadtrees

by Tobias Nipkow

Jan 26

2023

Fixed-length vectors

by Lars Hupel

Aug 14

2022

Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML

by Achim D. Brucker

Jul 29

Real-Time Double-Ended Queue

by Balazs Toth and Tobias Nipkow

Jun 23

A Combinator Library for Prefix-Free Codes

by Emin Karayel

Apr 08

2021

van Emde Boas Trees

by Thomas Ammer and Peter Lammich

Nov 23

Fresh identifiers

by Andrei Popescu and Thomas Bauereiss

Aug 16

A Verified Imperative Implementation of B-Trees

by Niels Mündler

Feb 24

Hood-Melville Queue

by Alejandro Gómez-Londoño

Jan 18

2020

Finite Map Extras

by Javier Díaz

Oct 12

A Formal Model of the Safely Composable Document Object Model with Shadow Roots

by Achim D. Brucker and Michael Herzberg

Sep 28

A Formal Model of the Document Object Model with Shadow Roots

by Achim D. Brucker and Michael Herzberg

Sep 28

A Formalization of Safely Composable Web Components

by Achim D. Brucker and Michael Herzberg

Sep 28

A Formalization of Web Components

by Achim D. Brucker and Michael Herzberg

Sep 28

The Safely Composable DOM

by Achim D. Brucker and Michael Herzberg

Sep 28

Relational Disjoint-Set Forests

by Walter Guttmann

Aug 26

Authenticated Data Structures As Functors

by Andreas Lochbihler and Ognjen Marić

Apr 16

Skip Lists

by Max W. Haslbeck and Manuel Eberl

Jan 09

2019

Interval Arithmetic on 32-bit Words

by Rose Bohrer

Nov 27

Priority Search Trees

by Peter Lammich and Tobias Nipkow

Jun 25

Binary Heaps for IMP2

by Simon Griebel

Jun 13

Multidimensional Binary Search Trees

by Martin Rau

May 30

2018

A Formal Model of the Document Object Model

by Achim D. Brucker and Michael Herzberg

Dec 26

Verifying Imperative Programs using Auto2

by Bohua Zhan

Dec 21

Deriving generic class instances for datatypes

by Jonas Rädle and Lars Hupel

Nov 06

Randomised Binary Search Trees

by Manuel Eberl

Oct 19

Optimal Binary Search Trees

by Tobias Nipkow and Dániel Somogyi

May 27

OpSets: Sequential Specifications for Replicated Datatypes

by Martin Kleppmann, Victor B. F. Gomes, Dominic P. Mulligan and Alastair R. Beresford

May 10

Weight-Balanced Trees

by Tobias Nipkow and Stefan Dirix

Mar 13

Treaps

by Max W. Haslbeck, Manuel Eberl and Tobias Nipkow

Feb 06

Taylor Models

by Christoph Traut and Fabian Immler

Jan 08

2017

The IMAP CmRDT

by Tim Jungnickel, Lennart Oldenburg and Matthias Loibl

Nov 09

Root-Balanced Tree

by Tobias Nipkow

Aug 20

A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes

by Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan and Alastair R. Beresford

Jul 07

Expected Shape of Random Binary Search Trees

by Manuel Eberl

Apr 04

2016

The Imperative Refinement Framework

by Peter Lammich

Aug 08

Pairing Heap

by Hauke Brinkop and Tobias Nipkow

Jul 14

Finite Machine Word Library

by Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk and Thomas Sewell

Jun 09

Algorithms for Reduced Ordered Binary Decision Diagrams

by Julius Michaelis, Max W. Haslbeck, Peter Lammich and Lars Hupel

Apr 27

Tensor Product of Matrices

by T.V.H. Prathamesh

Jan 18

2015

Reasoning about Lists via List Interleaving

by Pasquale Noce

Jun 11

Parameterized Dynamic Tables

by Tobias Nipkow

Jun 07

Trie

by Andreas Lochbihler and Tobias Nipkow

Mar 30

Deriving class instances for datatypes

by Christian Sternagel and René Thiemann

Mar 11

2014

XML

by Christian Sternagel, René Thiemann and Akihisa Yamada

Oct 03

Priority Queues Based on Braun Trees

by Tobias Nipkow

Sep 04

Skew Heap

by Tobias Nipkow

Aug 13

Splay Tree

by Tobias Nipkow

Aug 12

Amortized Complexity Verified

by Tobias Nipkow

Jul 07

2013

Native Word

by Andreas Lochbihler

Sep 17

A Formal Model of IEEE Floating Point Arithmetic

by Lei Yu

Jul 27

Light-weight Containers

by Andreas Lochbihler

Apr 15

2012

Generating linear orders for datatypes

by René Thiemann

Aug 07

2011

Infinite Lists

by David Trachtenherz

Feb 23

2010

Finger Trees

by Benedikt Nordhoff, Stefan Körner and Peter Lammich

Oct 28

Functional Binomial Queues

by René Neumann

Oct 28

Binomial Heaps and Skew Binomial Heaps

by Rene Meis, Finn Nielsen and Peter Lammich

Oct 28

Executable Matrix Operations on Matrices of Arbitrary Dimensions

by Christian Sternagel and René Thiemann

Jun 17

List Index

by Tobias Nipkow

Feb 20

2009

Collections Framework

by Peter Lammich

Nov 25

Code Generation for Functions as Data

by Andreas Lochbihler

May 06

2008

The Textbook Proof of Huffman's Algorithm

by Jasmin Christian Blanchette

Oct 15

BDD Normalisation

by Veronika Ortner and Norbert Schirmer

Feb 29

2004

File Refinement

by Karen Zee and Viktor Kuncak

Dec 09

Lazy Lists II

by Stefan Friedrich

Apr 26

Binary Search Trees

by Viktor Kuncak

Apr 05

AVL Trees

by Tobias Nipkow and Cornelia Pusch

Mar 19