#+OPTIONS: toc:nil num:nil

#+BEGIN_EXPORT html
<h1>Write-ups</h1>

<article class="index">
#+END_EXPORT

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 [[mailto:lthms@soap.coffee][email]], or start a discussion on
whichever site you like (I personnaly enjoy [[https://lobste.rs][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.

- [[./posts/AlgebraicDatatypes.html][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.

- [[./posts/ClightIntroduction.html][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.

- [[./posts/MiniHTTPServer.html][Implementing and Certifying a Web Server in Coq]] ::
  An explanation on how to write an almost pure Coq, and working (albeit
  minimal) HTTP server.

- [[./posts/Ltac101.html][Ltac 101]] ::
  Ltac is the “tactic language” of Coq. It allows for writing proof scripts
  which construct proof terms later checked by Coq.

- [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
  The ~rewrite~ tactics are really useful, since they are not limited to the Coq
  built-in equality relation.

- A Series on Strongly-Specified Funcions in Coq ::
  Coq ~Prop~ sort allows for defining properties function arguments have to
  satisfy, such that using such a function requires providing a proof the
  property is satisfied.

  1. [[./posts/StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
  2. [[./posts/StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]

* About Haskell

Haskell is a pure, lazy, functional programming language with a very expressive
type system.

- [[./posts/ExtensibleTypeSafeErrorHandling.html][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.

- [[./posts/MonadTransformers.org][Monad Transformers are a Great Abstraction]] ::
  Monads are hard to get right, monad transformers are harder. Yet, they remain
  a very powerful abstraction.

* About Common Lisp

Common Lisp is a venerable programming languages like no other I know.

- [[./posts/DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
  From the creation of a Lisp package up to the creation of a standalone
  executable.

* About this website

One of my goal with this website is for it to /feel/ simple, but the truth is
under the hood it is generated from a bunch of files using a not-that-simple
process.

- [[./cleopatra.html][A Series on Generating this Static Website]] ::
  This series consolidates the [[https://cleopatra.soap.coffee][*~cleopatra~*]]
  generation processes used to build this website. That is, each write-up is a
  literate program responsible for a particular step of the build process, and
  you are guaranteed that the code you read is the code that has been used to
  generate the HTML page you read it from.

  1. [[./cleopatra/theme.org][Theming with SASS ~(TODO)~]]
  2. [[./cleopatra/coq.org][Authoring Contents As Coq Documents ~(TODO)~]]
  3. [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]]
  4. [[./cleopatra/soupault.org][Processing HTML with ~soupault~]]

- [[./posts/Thanks.html][Thanks!]] ::
  If it were not for many awesome FOSS projects, this corner of the Internet
  would not exist. This is my attempt to give well-deserved credit to them and
  their creators.

- [[./posts/CleopatraV1.html][*~cleopatra~* the First]] ::
  This write-up is the literate program of the first version of *~cleopatra~*,
  before it became a command-line program implemented in Rust.

#+BEGIN_EXPORT html
</article>
#+END_Export