diff options
author | Thomas Letan <lthms@soap.coffee> | 2020-03-20 21:31:21 +0100 |
---|---|---|
committer | Thomas Letan <lthms@soap.coffee> | 2020-03-20 21:31:21 +0100 |
commit | b4a2c6e9cdda16c8bf4a154d0c90508538c33830 (patch) | |
tree | 602290871c2f5eb29bd4713bb745e564d8396c31 /site/posts | |
parent | Add a new post about Clight and its semantics (diff) |
Remove the “About” page and use the “Write-up” page as default index
Diffstat (limited to 'site/posts')
-rw-r--r-- | site/posts/index.org | 93 |
1 files changed, 0 insertions, 93 deletions
diff --git a/site/posts/index.org b/site/posts/index.org deleted file mode 100644 index 6b2e304..0000000 --- a/site/posts/index.org +++ /dev/null @@ -1,93 +0,0 @@ -#+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][announcement]] 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. - -- [[./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. - -- [[./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. - -- [[./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. - -- [[./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)~]] - -- [[./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 |