Formal Verification for Succinct Data Structures

The purpose of the page is to provide the Coq formalization for Succinct Data Structures.

Publications:

Akira Tanaka. Coq to C Translation with Partial Evaluation. Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '21). 2021-01-18, Virtual.

Akira Tanaka. Gallina Subset for C Extraction of Non-structural Recursion. The Coq Workshop 2019, 2019-09-08.

Akira Tanaka. Ruby Extension Library Verified using Coq Proof-assistant. RubyKaigi 2017, 2017-09-20.

Akira Tanaka, Reynald Affeldt, Jacques Garrigue. Safe Low-level Code Generation in Coq using Monomorphization and Monadification. IPSJ-SIGPRO, 2017-06-09.

Akira Tanaka, Reynald Affeldt, Jacques Garrigue. Formal Verification of the rank Algorithm for Succinct Data Structures. 18th International Conference on Formal Engineering Methods (ICFEM 2016), 2016-11-17.

Akira Tanaka, Reynald Affeldt, Jacques Garrigue. Formal Verification of the rank Function for Succinct Data Structures. 第18回プログラミングおよびプログラミング言語ワークショップ PPL 2016, 2016-03-08. 日本ソフトウェア科学会 プログラミング論研究会. Best paper award.