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.
- Proving Algebraic Datatypes are “Algebraic”
The set of types which can be defined in a language together with
*form an “algebraic structure” in the mathematical sense, hence the name. It means the definitions of
*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.
- 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
This series consolidates the
cleopatrageneration 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.
- 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.
This write-up is the literate program of the first version of
cleopatra, before it became a command-line program implemented in Rust.