1 files changed, 88 insertions, 0 deletions
diff --git a/site/posts/index.org b/site/posts/index.org
new file mode 100644
index 0000000..3c583a5
--- /dev/null
+++ b/site/posts/index.org
@@ -0,0 +1,88 @@
+#+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.
+
+- [[./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.
+
+- [[./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.
+
+- [[./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. [[./StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
+  2. [[./StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
+
+* About Haskell
+
+Haskell is a pure, lazy, functional programming language with a very expressive
+type system.
+
+- [[./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/][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.
+
+- [[./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.
+
+- [[./meta.html][A Series on Generating this Static Website]] ::
+  The toolchain behind the generation of this website ---called *~cleopatra~*---
+  is a literate programming document which build itself in addition to the HTML
+  files composing this corner of the Internet.
+
+  1. [[./meta/Bootstrap.html][Bootstrapping an Extensible Toolchain]]
+  2. [[./meta/Contents.html][Authoring Contents and HTML Generation ~(WIP)~]]
+  3. [[./meta/Soupault.html][Configuring ~soupault~ ~(WIP)~]]
+  4. [[./meta/Theme.html][Theming and Templating ~(WIP)~]]
+
+
+- [[./Thanks.html][Thanks!]] ::
+  If it were not for many awesome FOSS projects, this corner of the Internet
+  would not exists. This is my attempt to give well-deserved credit to them and
+  their creators.
+
+#+BEGIN_EXPORT html
+</article>
+#+END_Export