Coq proof assistant can be used to prove various properties of programs written in the Gallina language. It is also possible to translate Gallina programs to OCaml programs. However, OCaml is not suitable for low-level programs. Therefore, we are developing a Coq plugin for Gallina to C translation. This plugin transforms functions written in Gallina into a form as close to C as possible within Gallina. This transformation includes partial evaluation, which improves execution efficiency and eliminates polymorphism and dependent types. We can easily verify in Coq that this transformation does not change the execution result, and thus it is highly reliable. And Gallina functions after this transformation can be easily translated to C.
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:30 - 12:30
|Coq to C Translation with Partial Evaluation|
Akira Tanaka National Institute of Advanced Industrial Science and Technology (AIST)Media Attached
|Counterexample Generation for Program Verification based on Ownership Refinement TypesBest Paper Award|
Hideto Ueno The Univeristy of Tokyo, John Toman Certora, inc., Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada Chiba University, JapanMedia Attached