Hi, I’m lthms.

I don’t like syntax highlighting, but I like types and functional programming languages. He/him.

Interested in starting a discussion? Don’t hesitate to shoot me an email.

Technical Articles

Over the past years, I have tried to capitalize on my findings. More often than not, I have lacked in regularity, but I hope I have made up for it in exoticism.

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.

A Series on Strongly-Specified Funcions in Coq
Using dependent types and the Prop sort, it becomes possible to specify functions whose arguments and results are constrained by properties. Using such a “strongly-specified” function requires to provide a proof that the supplied arguments satisfy the expected properties, and allows for soundly assuming the results are correct too. However, implementing dependently-typed functions can be challenging.
A Series on Ltac
Ltac is the “tactic language” of Coq. It is commonly advertised as the common approach to write proofs, which tends to bias how it is introduced to new Coq users (e.g., in Master courses). In this series, we present Ltac as the metaprogramming tool it is, since fundamentally it is an imperative language which allows for constructing Coq terms interactively and incrementally.
Rewriting in Coq
The rewrite tactics are really useful, since they are not limited to the Coq built-in equality relation.
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.
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 Series on coqffi
coqffi generates Coq FFI modules from compiled OCaml interface modules (.cmi). In practice, it greatly reduces the hassle to together OCaml and Coq modules within the same codebase, especially when used together with the dune build system.

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.

Miscellaneous §

Over the years, I have made a habit of learning new programming languages, out of curiosity, and I intend to continue this way for the time being.

Discovering Common Lisp with trivial-gamekit
Common Lisp is a venerable programming languages like no other I know. From the creation of a Lisp package up to the creation of a standalone executable, we explore the shore of this strange beast.
Writing a Function Whose Argument is a Polymorphic Function in OCaml
In OCaml, it is not possible to write a function whose argument is a polymorphic function. Trying to write such a function results in the type-checker complaining back at you. The trick to be able to write such a function is to use records.

About this Website §

The generation of this website is far from being trivial, and requires the combination of —probably too— many tools. For instance, even if I mostly use Org mode for authoring content, most of my write-ups about Coq are actually Coq files, and I use coqdoc to generate the HTML pages you read.

This website could not exist without many awesome free software projects. Although I could not list them all even if I wanted, my desire is at least to try keeping up-to-date a curated description of the most significant ones.