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

#+OPTIONS: toc:nil num:nil
#+BEGIN_EXPORT html
<h1>Technical Articles</h1>
#+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/search?q=domain%3Asoap.coffee&what=stories&order=relevance][Lobste.rs]]
very much).
* About Coq
:PROPERTIES:
:CUSTOM_ID: coq
:END:
Coq is a formal proof management system which provides a pure functional
language with nice dependent types together with an environment for writing
machinechecked proofs.
 A Series on StronglySpecified Funcions in Coq ::
Using dependent types and the ~Prop~ sort, it becomes possible to specify
functions whose arguments and results are constrained by properties.
Using such a “stronglyspecified” function requires to provide a proof that
the supplied arguments satisfy the expected properties, and allows for soundly
assuming the results are correct too. However, implementing dependentlytyped
functions can be challenging. In this series, we explore several approaches
available to Coq developers.
1. [[./posts/StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
2. [[./posts/StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
 [[./posts/Ltac.org][A Series on Ltac]] ::
Ltac is the “tactic language” of Coq. It is commonly advertised as the common
approach to write proofs, which tends to bias how it is introduced to new Coq
users (/e.g./, in Master courses). In this series, we present Ltac as the
metaprogramming tool it is, since fundamentally it is an imperative language
which allows for constructing Coq terms interactively and incrementally.
 [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
The ~rewrite~ tactics are really useful, since they are not limited to the Coq
builtin equality relation.
 [[./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 writeup, we prove a straighforward functional property of a small C
function, as an exercise to discover the Clight semantics.
 [[./posts/AlgebraicDatatypes.html][Proving Algebraic Datatypes are “Algebraic”]] ::
The set of types which can be defined in a language together with ~+~ and ~*~
form an “algebraic structure” in the mathematical sense, hence the name. It
means the definitions of ~+~ and ~*~ have to satisfy properties such as
commutativity or the existence of neutral elements.
* About Haskell
Haskell is a pure, lazy, functional programming language with a very expressive
type system.
 [[./posts/ExtensibleTypeSafeErrorHandling.html][Extensible, TypeSafe Error Handling In Haskell]] ::
Ever heard of “extensible effects?” By applying the same principle, but for
error handling, the result is nice, typesafe API for Haskell, with a lot of
GHC magic under the hood.
* Miscellaneous
 [[./posts/DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivialgamekit~]] ::
Common Lisp is a venerable programming languages like no other I know. From
the creation of a Lisp package up to the creation of a standalone executable,
we explore the shore of this strange beast.
