φ-System is an experimental certified programming language and also a generic verification platform. It aims for reducing the labor effort for obtaining foundationally certified concrete programs (like C).
A neat version for the readme is still in progress and will be updated soon. We refer readers to Example Gallery for a quick preview of our examples. There are also some materials working in progress for interesting readers.
We are always looking for collaborations!
Qiyuan Xu, David Sanán, Zhé Hóu, Xiaokun Luan, Conrad Watt, and Yang Liu. 2025. Generically Automating Separation Logic by Functors, Homomorphisms and Modules. Proc. ACM Program. Lang. 9, POPL, Article 67 (January 2025), 40 pages. https://doi.org/10.1145/3704903