Merida in the movie Ralph 2.0


Over the past years, I have tried to capitalize on my findings. What I have lacked in regularity I made up for in subject exoticism.

If you like what you read, have a question or for any other reasons really, you can shoot an email, or start a discussion on whichever site you like (I personnaly enjoy very much).

About Coq

Coq is a formal proof management system which provides a pure functional language with nice dependent types together with an environment for writing machine-checked proofs.

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.
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.
Implementing and Certifying a Web Server in Coq
An explanation on how to write an almost pure Coq, and working (albeit minimal) HTTP server.
A Series on Ltac
Ltac is the “tactic language” of Coq. It allows for writing proof scripts which construct proof terms later checked by Coq.
  1. Ltac 101
  2. Mixing Ltac and Gallina for Fun and Profit
Rewriting in Coq
The rewrite tactics are really useful, since they are not limited to the Coq built-in equality relation.
A Series on Strongly-Specified Funcions in Coq
Coq Prop sort allows for defining properties function arguments have to satisfy, such that using such a function requires providing a proof the property is satisfied.
  1. Using the refine Tactics
  2. Using the Program Framework

About Haskell

Haskell is a pure, lazy, functional programming language with a very expressive type system.

Extensible, Type-Safe Error Handling In Haskell
Ever heard of “extensible effects?” By applying the same principle, but for error handling, the result is nice, type-safe API for Haskell, with a lot of GHC magic under the hood.
Monad Transformers are a Great Abstraction
Monads are hard to get right, monad transformers are harder. Yet, they remain a very powerful abstraction.

About Common Lisp

Common Lisp is a venerable programming languages like no other I know.

Discovering Common Lisp with trivial-gamekit
From the creation of a Lisp package up to the creation of a standalone executable.

About this website

One of my goal with this website is for it to feel simple, but the truth is under the hood it is generated from a bunch of files using a not-that-simple process.

A Series on Generating this Static Website
This series consolidates the cleopatra generation processes used to build this website. That is, each write-up is a literate program responsible for a particular step of the build process, and you are guaranteed that the code you read is the code that has been used to generate the HTML page you read it from.
  1. Theming with SASS (TODO)
  2. Authoring Contents As Coq Documents (TODO)
  3. Authoring Contents As Org Documents (TODO)
  4. Processing HTML with soupault
If it were not for many awesome FOSS projects, this corner of the Internet would not exist. This is my attempt to give well-deserved credit to them and their creators.
cleopatra the First
This write-up is the literate program of the first version of cleopatra, before it became a command-line program implemented in Rust.