Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 11:30 - 12:00 at PEPM - Session 2 Chair(s): Youyou Cong

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: Session 2PEPM at PEPM
Chair(s): Youyou CongTokyo Institute of Technology

Live stream: https://www.youtube.com/watch?v=tuxm51MLkHM

11:30 - 12:00
Research paper
Coq to C Translation with Partial Evaluation
Akira TanakaNational Institute of Advanced Industrial Science and Technology (AIST)
Media Attached
12:00 - 12:30
Research paper
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, Japan
Media Attached