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 | Session 2PEPM at PEPM Chair(s): Youyou Cong Tokyo Institute of Technology Live stream: https://www.youtube.com/watch?v=tuxm51MLkHM | ||
11:30 30mResearch paper | Coq to C Translation with Partial Evaluation PEPM Akira Tanaka National Institute of Advanced Industrial Science and Technology (AIST) Media Attached | ||
12:00 30mResearch paper | Counterexample Generation for Program Verification based on Ownership Refinement TypesBest Paper Award PEPM Hideto Ueno The Univeristy of Tokyo, John Toman Certora, inc., Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan Media Attached | ||