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 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:30 - 12:30
|Coq to C Translation with Partial Evaluation|
Akira TanakaNational Institute of Advanced Industrial Science and Technology (AIST)Media Attached
|Counterexample Generation for Program Verification based on Ownership Refinement TypesBest Paper Award|
Hideto UenoThe Univeristy of Tokyo, John TomanCertora, inc., Naoki KobayashiUniversity of Tokyo, Japan, Takeshi TsukadaChiba University, JapanMedia Attached