Skip to content

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

License

Notifications You must be signed in to change notification settings

CertiCoq/VeriFFI

Repository files navigation

VeriFFI

VeriFFI is a verified Foreign Function Interface (FFI) for Coq (Gallina) programs that call, and are called by, C programs. The operational connection is by compiling Gallina programs through C using the CertiCoq compiler. The specification/verification connection is by using the Verified Software Toolchain (Verifiable C) to specify library functions written in C that are callable by CertiCoq-compiled programs, and vice versa. The goal is to have a fully foundational soundness proof for this connection. This is still a work in progress.

Participants:

Technical report:

About

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Languages