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).
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.
- 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.
- 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
rewritetactics are really useful, since they are not limited to the Coq built-in equality relation.
- A Series on Strongly-Specified Funcions in Coq
Propsort allows for defining properties function arguments have to satisfy, such that using such a function requires providing a proof the property is satisfied.
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
- 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
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 is
- 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.