Formal Verification for Succinct Data Structures

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

Publications:

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.