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 Lobste.rs 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 machinechecked proofs.
 A Study of Clight and its Semantics
 Clight is a “simplified” C AST used by CompCert, the certified C compiler. In this writeup, 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.
 Ltac 101
 Ltac is the “tactic language” of Coq. It allows for writing proof scripts which construct proof terms later checked by Coq.
 Rewriting in Coq

The
rewrite
tactics are really useful, since they are not limited to the Coq builtin equality relation.  A Series on StronglySpecified 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.
About Haskell
Haskell is a pure, lazy, functional programming language with a very expressive type system.
 Extensible, TypeSafe Error Handling In Haskell
 Ever heard of “extensible effects?” By applying the same principle, but for error handling, the result is nice, typesafe 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
trivialgamekit
 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 notthatsimple process.
 A Series on Generating this Static Website

The toolchain behind the generation of this website —called
cleopatra
— is a literate program which build itself in addition to the HTML files composing this corner of the Internet. This series iscleopatra
.  Thanks!
 If it were not for many awesome FOSS projects, this corner of the Internet would not exist. This is my attempt to give welldeserved credit to them and their creators.