1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
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
|