A Verified Foreign Function Interface Between Coq and C

This video presents a research talk from POPL 2025 conference that demonstrates a Verified Foreign Function Interface (VeriFFI) between Coq and C programming languages. Learn how researchers Joomy Korkut, Kathrin Stark, and Andrew W. Appel developed a system that guarantees type safety and correctness when combining dependently typed functional programs written in Coq with low-level C programs. Discover how VeriFFI works by translating Coq function types and constructor types along with functional models into VST function-specifications, allowing C functions to behave according to user-specified functional models even when the implementation differs significantly. The presentation explores a novel hybrid deep/shallow description of Coq dependent types that enables this translation. The 20-minute talk was delivered at the ACM SIGPLAN POPL 2025 conference held January 19-25, 2025.