#+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 email to [[mailto:~lthms/lthms.xyz@lists.sr.ht][the dedicated mailing list]] (see the [[https://lists.sr.ht/~lthms/lthms.xyz/%3C20190127111504.n27ttkvtl7l3lzwb%40ideepad.localdomain%3E][annoucement]] for a
guide on how to subscribe).

* 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/MiniHTTPServer/][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/][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/][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/][Using the ~refine~ Tactics]]
  2. [[/posts/StronglySpecifiedFunctionsProgram][Using the ~Program~ Framework]]

* About Haskell

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

- [[/posts/ExtensibleTypeSafeErrorHandling/][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/][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/][Discovering Common Lisp with ~trivial-gamekit~]] ::
  From the creation of a Lisp package up to the creation of a standalone
  executable.

#+BEGIN_EXPORT html
</article>
#+END_Export