lthms' avatar, a hand drawing looking person, wearing a headset, close to a window on a raining night
Thomas Letan
lthms · he/him

Did you come across something which caught your attention? Don’t hesitate to shoot me an email in my public inbox.


Implementing an Echo Server in Coq with coqffi.1.0.0 (

In this article, we will demonstrate how coqffi can be used to implement an echo server, i.e., a TCP server which sends back any input it receives from its clients.

coqffi.1.0.0 In A Nutshell (

For each entry of a cmi file, coqffi tries to generate an equivalent (from the extraction mechanism perspective) Coq definition. In this article, we walk through how coqffi works.

Pattern Matching on Types and Contexts (

Ltac allows for pattern matching on types and contexts. In this article, we give a short introduction on this feature of key importance. Ltac programs (“proof scripts”) generate terms, and the shape of said terms can be very different regarding the initial context. For instance, induction x will refine the current goal using an inductive principle dedicated to the type of x.

Ltac is an Imperative Metaprogramming Language (

Ltac generates terms, therefore it is a metaprogramming language. It does it incrementally, by using primitives to modifying an implicit state, therefore it is an imperative language. Henceforth, it is an imperative metaprogramming language.

Mixing Ltac and Gallina for Fun and Profit (

One of the most misleading introduction to Coq is to say that “Gallina is for programs, while tactics are for proofs.” Gallina is the preferred way to construct programs, and tactics are the preferred way to construct proofs. The key word here is “preferred.” Coq actually allows for mixing Ltac and Gallina together.

Proving Algebraic Datatypes are “Algebraic” (

The set of types which can be defined in a language together with ++ and * form an “algebraic structure” in the mathematical sense, hence the name. It means the definitions of ++ and * have to satisfy properties such as commutativity or the existence of neutral elements. In this article, we prove the sum and prod Coq types satisfy these properties.

A Study of Clight and its Semantics (

Clight is a “simplified” C AST used by CompCert, the certified C compiler. In this write-up, we prove a straighforward functional property of a small C function, as an exercise to discover the Clight semantics.

Rewriting in Coq (

The rewrite tactics are really useful, since they are not limited to the Coq built-in equality relation.

Implementing Strongly-Specified Functions with the Program Framework (

Program is the heir of the refine tactic. It gives you a convenient way to embed proofs within functional programs that are supposed to fade away during code extraction.

Implementing Strongly-Specified Functions with the refine Tactic (

We see how to implement strongly-specified list manipulation functions in Coq. Strong specifications are used to ensure some properties on functions' arguments and return value. It makes Coq type system very expressive.