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
89
90
91
92
93
94
95
96
97
98
99
|
#+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/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/coq.org][Authoring Contents As Coq Documents ~(TODO)~]]
2. [[./cleopatra/org.org][Authoring Contents As Org Documents ~(TODO)~]]
3. [[./cleopatra/theme.org][Theming with SASS ~(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
|