< Retour au sommaire

Programs and their proofs in type theory : application to freshness and zero-copy packet processing

Pierre Nigron le

Lieu: bât 862, pièce 1073

Suivre en visio

Abstract

Monadic programming is an essential component in the toolbox of functional programmers. For the programmers who sometimes navigate the waters of certified programming in type theory, it is the only means to concisely implement the imperative traits of certain algorithms. Monads open up a portal to the imperative world, all that from the comfort of the functional world. The trend towards certified programming within type theory begs the question of reasoning about such programs. Effectful programs being encoded as pure programs in the host type theory, we can readily manipulate these objects through their encoding.

Following the idea that every monad deserves a dedicated program logic, I will present an experiment about freshness using separation logic. The experiment is accompanied by a study case on the SimplExpr of CompCert.

In the same vein, I will talk about packet processing and in particular the zero-copy property used by some libraries of combinator. The zero-copy property ensures that memory accesses returned by a parser give access to disjoint spaces. This property can be useful for users, in particular in a concurrent context. Inspired by the Nom library written in Rust, I have defined a library of combinator in Coq which also has a program logic allowing to prove the absence of aliasing.

If time permits, I will present a transformation phase by refinement whose objective is to eliminate redundant checks in the parsers and compile them (without certification) to C to obtain efficient programs.