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