Generic Authenticated Data Structures, Formally.

DOI10.4230/LIPICS.ITP.2019.10MaRDI QIDQ5875417zbMATH OpenOpenAlexFDO

Authors Matthias Brun, Dmitriy Traytel

Publication date 3 February 2023

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

zbMATH Keywords

authenticated data structuresIsabelle/HOLnominal Isabelleverifiable computation

Mathematics Subject Classification ID

Cites work

• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• A new approach to abstract syntax with variable binding
• A new foundation for Nominal Isabelle
• Authentic third-party data publication
• Authenticated data structures, generically
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Formal SOS-Proofs for the Lambda-Calculus
• General bindings and alpha-equivalence in Nominal Isabelle
• scientific article; zbMATH DE number 6148924 (Why is no real title available?)
• The adequacy of Launchbury's natural semantics for lazy evaluation
• Types and programing languages

Cited in

(3)

• scientific article; zbMATH DE number 1962158 (Why is no real title available?)
• Animating MRBNFs: truly modular binding-aware datatypes in Isabelle/HOL
• Formalization of Generic Authenticated Data Structures

Describes a project that uses

Uses Software

• Nominal Isabelle
• GitHub

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875417)