Related papers: While Loops in Coq
In this tutorial, we program big-step and small-step total interpreters for the While language extended with input and output primitives. While is a simple imperative language consisting of skip, assignment, sequence, conditional and loop.…
The goal of this lecture is to show how modern theorem provers---in this case, the Coq proof assistant---can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and…
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the…
In this paper, we facilitate the reasoning about impure programming languages, by annotating terms with `decorations' that describe what computational (side) effect evaluation of a term may involve. In a point-free categorical…
We present a method for verifying partial correctness properties of imperative programs that manipulate integers and arrays by using techniques based on the transformation of constraint logic programs (CLP). We use CLP as a metalanguage for…
For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among these methods, differentiable logics (DLs) are used to…
Common programming tools, like compilers, debuggers, and IDEs, crucially rely on the ability to analyse program code to reason about its behaviour and properties. There has been a great deal of work on verifying compilers and static…
Automated analysis of recursive derivations in logic programming is known to be a hard problem. Both termination and non-termination are undecidable problems in Turing-complete languages. However, some declarative languages offer a…
Proof assistants like Coq are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are especially difficult to reuse. In this paper, we present a…
Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to…
We exploit (co)inductive specifications and proofs to approach the evaluation of low-level programs for the Unlimited Register Machine (URM) within the Coq system, a proof assistant based on the Calculus of (Co)Inductive Constructions type…
Loop invariants play a central role in the verification of imperative programs. However, finding these invariants is often a difficult and time-consuming task for the programmer. We have previously shown how program transformation can be…
In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments: an invariant, for functional properties (ignoring termination); and a variant, for termination (ignoring…
In order to better understand reasoning involved in analyzing infinite games in extensive form, we performed experiments in the proof assistant Coq that are reported here.
We present a new approach to termination analysis of numerical computations in logic programs. Traditional approaches fail to analyse them due to non well-foundedness of the integers. We present a technique that allows overcoming these…
This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for…
We introduce a first-order quantum programming language, named FOQ, whose terminating programs are reversible. We restrict FOQ to a strict and tractable subset, named PFOQ, of terminating programs with bounded width, that provides a first…
Some total languages, like Agda and Coq, allow the use of guarded corecursion to construct infinite values and proofs. Guarded corecursion is a form of recursion in which arbitrary recursive calls are allowed, as long as they are guarded by…
We propose a new library to model and verify hardware circuits in the Coq proof assistant. This library allows one to easily build circuits by following the usual pen-and-paper diagrams. We define a deep-embedding: we use a (dependently…
In this paper, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.'s basic laws of classical programming to the quantum setting. These laws characterise the algebraic properties of…