diff options
Diffstat (limited to 'site/posts/index.org')
-rw-r--r-- | site/posts/index.org | 88 |
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 |