- Neovim, OCaml Interfaces, Tree-Sitter and LSP (
Can we all agree that witnessing syntax highlighting being absolutely off is probably the most annoying thing that can happen to anybody?
- 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.
Implementing an Echo Server in Coq with
In this article, we will demonstrate how
coqffican be used to implement an echo server, i.e., a TCP server which sends back any input it receives from its clients.
coqffi.1.0.0In A Nutshell (
For each entry of a cmi file, coqffi tries to generate an equivalent (from the extraction mechanism perspective) Coq definition. In this article, we walk through how coqffi works.
Hi, I’m Thomas Letan (lthms) (he/him).
You read something which caught your attention and you are interested in starting a discussion? Don’t hesitate to shoot me an email.