Efficient extensional binary tries

DOI10.1007/s10817-022-09655-xarXiv2110.05063MaRDI QIDQ6156636

Andrew W. Appel, Xavier Leroy

Publication date: 14 June 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2110.05063

zbMATH Keywords

Coqprogram proofVSTCompCertverified data structures

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• VST-Floyd: a separation logic tool to verify correctness of C programs
• Edinburgh LCF. A mechanized logic of computation
• Abstraction and subsumption in modular verification of C programs
• Verified software units
• Verified Software Toolchain
• A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Programming Languages and Systems
• Program Logics for Certified Compilers

This page was built for publication: Efficient extensional binary tries