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
|
#+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/][A Series on Generating this Static Website]] ::
The toolchain behind the generation of this website ---called *~cleopatra~*---
is a literate program which build itself in addition to the HTML files
composing this corner of the Internet. This series /is/ *~cleopatra~*.
1. [[/cleopatra/Bootstrap.html][Bootstrapping an Extensible Toolchain]]
2. [[/cleopatra/Soupault.html][~soupault~ Configuration]]
3. [[/cleopatra/Contents/Org.org][Generating Contents from Org Documents ~(TODO)~]]
4. [[/cleopatra/Contents/Coq.org][Generating Contents from Coq Documents ~(TODO)~]]
5. [[/cleopatra/Theme.html][Theming and Templating ~(TODO)~]]
- [[./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.
#+BEGIN_EXPORT html
</article>
#+END_Export
|