2 papers
cs.PL2025
Pleasant Imperative Program Proofs with GallinaC
Frédéric Fort, David Nowak, Vlad Rusu
Even with the increase of popularity of functional programming, imperative programming remains a key programming paradigm, especially for programs operating at lower levels of abst…
cs.PL2023
While Loops in Coq
David Nowak, Vlad Rusu
While loops are present in virtually all imperative programming languages. They are important both for practical reasons (performing a number of iterations not known in advance) an…