Formal Verification for Succinct Data Structures

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

The purpose of the page is to provide the Coq formalization discussed in: Akira Tanaka, Reynald Affeldt, Jacques Garrigue, Formal Verification of the rank Algorithm for Succinct Data Structures.

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.

Former publications:

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.