publications: - title: "While Loops in Coq" author: - name: "David Nowak" link: "https://davidnowak.github.io/" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2023" doi: "https://doi.org/10.4204/EPTCS.389.8" abstract: "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) and theoretical reasons (achieving Turing completeness). In this paper we propose an approach for incorporating while loops in an imperative language shallowly embedded in the Coq proof assistant. The main difficulty is that proving the termination of while loops is nontrivial, or impossible in the case of nontermination, whereas Coq only accepts programs endowed with termination proofs. Our solution is based on a new, general method for defining possibly non-terminating recursive functions in Coq. We illustrate the approach by proving termination and partial correctness of a program on linked lists." links: doi: "https://doi.org/10.4204/EPTCS.389.8" technicalreport: "https://researchr.org/publication/preprint--24" "url": "https://doi.org/10.4204/EPTCS.389.8" researchr: "https://researchr.org/publication/-24" cites: 0 citedby: 0 pages: "96-109" booktitle: "Proceedings 7th Symposium on Working Formal Methods, FROM 2023, Bucharest, Romania, 21-22 September 2023" kind: "inproceedings" key: "-24" - title: "(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic" author: - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" - name: "David Nowak" link: "https://davidnowak.github.io/" year: "2021" month: "January" doi: "https://doi.org/10.1016/j.jlamp.2020.100619" abstract: " Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and inherit the coinductive nature of the logic. The proof systems differ, however, in several aspects. First, they use induction and coinduction in different proportions. The second aspect regards compositionality, broadly meaning their ability to prove simpler formulas on smaller systems and to reuse those formulas as lemmas for proving more complex formulas on larger systems. The third aspect is the difficulty of their soundness proofs. We show that the more induction a proof system uses, and the more specialised is its use of coinduction (with respect to our problem domain), the more compositional the proof system is, but the more difficult is its soundness proof. We present formalisations of these results in the Coq proof assistant. In particular we have developed support for coinductive proofs that is comparable to that provided by Coq for inductive proofs. This may be of interest to a broader class of Coq users." links: doi: "https://doi.org/10.1016/j.jlamp.2020.100619" technicalreport: "https://researchr.org/publication/preprint-rn20" researchr: "https://researchr.org/publication/rn20" cites: 0 citedby: 0 journal: "jlap" volume: "118" kind: "article" key: "rn20" - title: "Formal definitions and proofs for partial (co)recursive functions" author: - name: "Horatiu Cheval" link: "https://researchr.org/alias/horatiu-cheval" - name: "David Nowak" link: "https://davidnowak.github.io/" - name: "Vlad Rusu" link: "https://researchr.org/alias/vlad-rusu" year: "2024" abstract: "Partial functions are a key concept in programming. Without partiality a programming language has limited expressiveness -- it is not Turing-complete, hence, it excludes some constructs such as {while}-loops. In functional programming languages, partiality mostly originates from the non-termination of recursive functions. Corecursive functions are another source of partiality: here, the issue is not termination, but the inability to produce arbitrary large, finite approximations of a theoretically infinite output. Partial functions have been formally studied in the branch of theoretical computer science called domain theory. In this paper we propose to step up the level of formality by using the Coq proof assistant. The main difficulty is that Coq requires all functions to be total, since partiality would break the soundness of its underlying logic. We propose practical solutions for this issue, and others, which appear when one attempts to define and reason about partial (co)recursive functions in a total functional language" links: published: "https://researchr.org/publication/ChevalNR24" researchr: "https://researchr.org/publication/preprint-ChevalNR24" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-ChevalNR24" - title: "Formal definitions and proofs for partial (co)recursive functions" author: - name: "Horatiu Cheval" link: "https://researchr.org/alias/horatiu-cheval" - name: "David Nowak" link: "https://davidnowak.github.io/" - name: "Vlad Rusu" link: "https://researchr.org/profile/vladrusu/publications" year: "2024" doi: "https://doi.org/10.1016/j.jlamp.2024.100999" abstract: "Partial functions are a key concept in programming. Without partiality a programming language has limited expressiveness -- it is not Turing-complete, hence, it excludes some constructs such as {while}-loops. In functional programming languages, partiality mostly originates from the non-termination of recursive functions. Corecursive functions are another source of partiality: here, the issue is not termination, but the inability to produce arbitrary large, finite approximations of a theoretically infinite output. Partial functions have been formally studied in the branch of theoretical computer science called domain theory. In this paper we propose to step up the level of formality by using the Coq proof assistant. The main difficulty is that Coq requires all functions to be total, since partiality would break the soundness of its underlying logic. We propose practical solutions for this issue, and others, which appear when one attempts to define and reason about partial (co)recursive functions in a total functional language" links: doi: "https://doi.org/10.1016/j.jlamp.2024.100999" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jlap/ChevalNR24" technicalreport: "https://researchr.org/publication/preprint-ChevalNR24" researchr: "https://researchr.org/publication/ChevalNR24" cites: 0 citedby: 0 journal: "jlap" volume: "141" pages: "100999" kind: "article" key: "ChevalNR24"