# Technical Articles

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 likeI personnaly enjoy Lobste.rs very much.

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

## 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.
- A Series on Generating this Website
- At some point, I felt like the whole process of generating this website was interesting enough so that it would deserve a write-up of its own. As a result, I spent quite some time turning my custom toolchain into a literate program, so that its actual code source would actually be the write-ups I wanted to add to my website.