Program in Coq

Abstract : In this thesis, we develop new techniques to conveniently write formally verified programs. To proceed, we study the use of Coq as a programming language in different settings. Coq being a purely functional language, we mainly focus on the representation and on the specification of impure effects, like exceptions, mutable references, inputs-outputs, and concurrency.First, we work on two preliminary projects helping us to understand the challenges of programming in Coq. The first project, Cybele, is a Coq plugin to write efficient proofs by reflection with effects. We compile and execute the impure effects in OCaml to generate a prophecy, a kind of certificate, and then interpret the effects in Coq using the prophecy. The second project, the compiler CoqOfOCaml, imports OCaml programs with effects into Coq, using an effect inference system.Next, we describe different generic and composable representations of impure effects in Coq. The breakable computations combine the standard exceptions and mutable references effects, with a pause mechanism to make explicit the evaluation steps in order to represent the concurrent evaluation of two terms. By implementing the Pluto web server in Coq, we realize that the most important effects to program are the asynchronous inputs-outputs. Indeed, these effects are ubiquitous and cannot be encoded in a purely functional manner. Thus, we design the asynchronous computations as a first way to represent and compile programs with events and handlers in Coq.Then, we study techniques to prove properties about programs with effects. We start with the verification of the blog system ChickBlog written in the language of the interactive computations. This blog runs one worker with synchronous inputs-outputs per client. We verify our blog using the method of specification by use cases. We adapt this technique to type theory by expressing a use case as a well-typed co-program over the program we verify. Thanks to this formalism, we can present a use case as a symbolic test program and symbolically debug it, step by step, using the interactive proof mode of Coq. To our knowledge, this is the first such adaptation of the use case specifications in type theory. We believe that the formal specification by use cases is one of the keys to verify effectful programs, as the method of use cases proved to be convenient to express (informal) specifications in the software industry. We extend our formalism to concurrent and potentially non-terminating programs with the language of concurrent computations. Apart from the use case method, we design a model-checker to verify the deadlock freedom of concurrent computations, by compiling the parallel composition to the non-deterministic choice operator using the language of blocking computations
Keywords : Coq Side effects
Complete list of metadatas

Cited literature [111 references]  Display  Hide  Download

https://hal.inria.fr/tel-01890983
Contributor : Abes Star <>
Submitted on : Monday, July 15, 2019 - 10:23:08 AM
Last modification on : Wednesday, November 6, 2019 - 4:14:59 AM

File

CLARET_Guillaume_2_complete_20...
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01890983, version 2

Collections

Citation

Guillaume Claret. Program in Coq. Formal Languages and Automata Theory [cs.FL]. Université Sorbonne Paris Cité, 2018. English. ⟨NNT : 2018USPCC068⟩. ⟨tel-01890983v2⟩

Share

Metrics

Record views

84

Files downloads

512