lthms' avatar, a hand drawing looking person, wearing a headset, close to a window on a raining night

Hi, I’m Thomas Letan (lthms) (he/him).

You read something which caught your attention? Don’t hesitate to shoot me an email.


A series gathers together a collection of contents (that is, either posts or other series) into a coherent whole. This is by opposition to tags, which only allows for signaling that two posts refers to a given subject.

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

A Series on Strongly-Specified Functions in Coq

Using dependent types and the Prop sort, it becomes possible to specify functions whose arguments and results are constrained by properties. However, implementing such functions can be challenging. In this series, we explore several approaches available to Coq developers.


A collection of articles I have written to reflect on what happened at a given time. It is heavily inspired by Drew DeVault “status update” series.