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.

- Thanks!
- 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.