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
|
#+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
machine-checked proofs.
- [[./posts/StronglySpecifiedFunctions.org][A Series on Strongly-Specified 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 “strongly-specified” 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 dependently-typed
functions can be challenging.
- [[./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
built-in 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 write-up, 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, 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.
* Miscellaneous
- [[./posts/DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
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.
|