POPL 2025 (series) / CoqPL 2025 (series) / The Eleventh International Workshop on Coq for Programming Languages /
CoqNFU: Towards Formalizing NFU in Coq
This program is tentative and subject to change.
Sat 25 Jan 2025 16:45 - 17:07 at Peek-A-Boo - Session 4 (16:00 - 17:30)
NFU is a set theory with decidable syntactic check that decides whether a formula is suitable or not to be used as a property defining a set. This feature makes NFU particularly interesting for formalization within assisted theorem provers. We discuss an implementation of a certified stratification algorithm as the first stepping stone in a larger project of implementing NFU in Coq.
| Extended Abstract (abstract.pdf) | 380KiB |
This program is tentative and subject to change.
Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change
Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change
16:00 - 17:30 | |||
16:00 22mTalk | Towards Automated Verification of LLM-Synthesized C Programs CoqPL File Attached | ||
16:22 22mTalk | Towards Mining Robust Coq Proof Patterns CoqPL Cezary Kaliszyk University of Melbourne, Xuan-Bach D. Le University of Melbourne, Christine Rizkallah University of Melbourne File Attached | ||
16:45 22mTalk | CoqNFU: Towards Formalizing NFU in Coq CoqPL File Attached | ||
17:07 22mTalk | Formal Verification of Quantum Stabilizer Code CoqPL File Attached | ||