Bidirectional certified programming

Daisuke Kinoshita, Keisuke Nakano

Research output: Contribution to journalConference articlepeer-review

2 Citations (Scopus)


Certified programming is one of the desirable approaches to developing dependable software, where expected properties of programs are formally proved by proof assistants such as Coq. One way for certified programming with Coq is to define a function, give proofs for its properties in Coq, and then extract a program in OCaml. Another way for certified programming with Coq is to import the definition from OCaml and give proofs for its properties in Coq. Since translations in both methods are unidirectional, we can modify only either of Coq and OCaml. That makes it hard to develop large certified programs. To solve this problem, we propose a new framework for certified programming through bidirectional transformation between Coq functions and OCaml programs. In our system, one can develop certified programs by modifying both Coq functions and OCaml programs alternatingly. All updates of the OCaml program are reflected to the Coq function, and vice versa, while reusing as many parts of the original one as possible.

Original languageEnglish
Pages (from-to)31-38
Number of pages8
JournalCEUR Workshop Proceedings
Publication statusPublished - 2017 Jan 1
Externally publishedYes
Event6th International Workshop on Bidirectional Transformations, BX 2017 - Uppsala, Sweden
Duration: 2017 Apr 29 → …

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'Bidirectional certified programming'. Together they form a unique fingerprint.

Cite this