Generic Authenticated Data Structures, Formally.

DOI10.4230/LIPIcs.ITP.2019.10OpenAlexW2977737234MaRDI QIDQ5875417

Dmitriy Traytel, Matthias Brun

Publication date: 3 February 2023

Full work available at URL: https://doi.org/10.4230/LIPIcs.ITP.2019.10

zbMATH Keywords

authenticated data structuresIsabelle/HOLverifiable computationnominal Isabelle

Mathematics Subject Classification ID

Uses Software

• Nominal Isabelle
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• A new approach to abstract syntax with variable binding
• The adequacy of Launchbury's natural semantics for lazy evaluation
• Formal SOS-Proofs for the Lambda-Calculus
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Authenticated data structures, generically
• A New Foundation for Nominal Isabelle
• General Bindings and Alpha-Equivalence in Nominal Isabelle

This page was built for publication: Generic Authenticated Data Structures, Formally.