diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | site/cleopatra/Theme.org | 3 | ||||
| -rw-r--r-- | site/index.html | 72 | ||||
| -rw-r--r-- | site/index.org (renamed from site/posts/index.org) | 20 |
4 files changed, 12 insertions, 85 deletions
@@ -16,6 +16,7 @@ site/posts/ClightIntroduction.html site/posts/StronglySpecifiedFunctions.html site/posts/RewritingInCoq.html site/posts/Ltac101.html +site/index.html site/news/ColorlessThemes-0.2.html site/cleopatra/Contents.html site/cleopatra/index.html @@ -25,7 +26,6 @@ site/cleopatra/Soupault.html site/cleopatra/Contents/Org.html site/cleopatra/Contents/Coq.html site/posts/Thanks.html -site/posts/index.html site/posts/DiscoveringCommonLisp.html site/posts/ExtensibleTypeSafeErrorHandling.html site/posts/MonadTransformers.html diff --git a/site/cleopatra/Theme.org b/site/cleopatra/Theme.org index 47bef25..41faa8b 100644 --- a/site/cleopatra/Theme.org +++ b/site/cleopatra/Theme.org @@ -89,8 +89,7 @@ noscript.parentNode.removeChild(noscript); <nav> <ul> <li> <a href="/news">News</a></li> - <li> <a href="/posts">Write-ups</a></li> - <li> <a href="/">About</a></li> + <li> <a href="/">Write-ups</a></li> </ul> </nav> <header> diff --git a/site/index.html b/site/index.html deleted file mode 100644 index deddc99..0000000 --- a/site/index.html +++ /dev/null @@ -1,72 +0,0 @@ -<!doctype html> -<html lang="en"> - <head> - <meta charset="utf-8"> - <meta name="viewport" content="width=device-width, initial-scale=1.0"> - <link rel="icon" type="image/ico" href="/img/merida.webp"> - <link rel="stylesheet" href="/style/main.css"> - <noscript id="lazyloading"> - <link rel="stylesheet" href="https://soap.coffee/+vendors/fira-code.2+swap/font.css"> - <link rel="stylesheet" href="https://soap.coffee/+vendors/et-book+swap/font.css"> - <link rel="stylesheet" href="https://soap.coffee/+vendors/fork-awesome.1.1.7+swap/css/fork-awesome.min.css"> - </noscript> - <title></title> - </head> - <body id="vcard"> - <article> - <img src="/img/merida.webp" - alt="Merida in the movie Ralph 2.0" /> - <p> - Hi, awesome stranger. - </p> - - <p> - I am <strong>lthms</strong>, and I welcome you in my little corner of - the Internet. - </p> - - <nav> - <dl> - <dt><a href="/posts/">my write-ups</a></dt> - <dd> - You may find interesting my articles if you are into functional - programming languages. - </dd> - </dl> - <dl> - <dt><a href="https://code.soap.coffee"><i class="fa fa-code" aria-hidden="true"></i> code.soap.coffee</a></dt> - <dd> - A collection of personal git repositories, including a set of - dotfiles (emacs, sway…), a set of tools for story writers. - </dd> - </dl> - <dl> - <dt><a rel="me" href="https://mastodon.social/@lthms"><i class="fa fa-mastodon" aria-hidden="true"></i> @lthms@mastodon.social</a></dt> - <dd> - My personal account on the fediverse. I mostly toot about functional - programming languages, formal methods, and my Emacs configuration. - </dd> - </dl> - <dl> - <dt><a href="https://dblp.org/pers/hd/l/Letan:Thomas">my academic publications</a></dt> - <dd> - I have a PhD in computer science, and I focus my research on - applying formal methods approaches to prove security properties. - </dd> - </dl> - </nav> - - <p> - I wish you a wonderful day. - </p> - </article> - <script> - let noscript = document.getElementById('lazyloading'); - let resources = noscript.innerText.split('\n'); - - for (var ix in resources) { - noscript.insertAdjacentHTML('beforebegin', resources[ix]); - } - </script> - </body> -</html> diff --git a/site/posts/index.org b/site/index.org index 6b2e304..2a5e085 100644 --- a/site/posts/index.org +++ b/site/index.org @@ -19,20 +19,20 @@ 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]] :: +- [[./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. -- [[./MiniHTTPServer.html][Implementing and Certifying a Web Server in Coq]] :: +- [[./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. -- [[./Ltac101.html][Ltac 101]] :: +- [[./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. -- [[./RewritingInCoq.html][Rewriting in 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. @@ -41,20 +41,20 @@ machine-checked proofs. 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]] + 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. -- [[./ExtensibleTypeSafeErrorHandling.html][Extensible, Type-Safe Error Handling In Haskell]] :: +- [[./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. -- [[./MonadTransformers.org][Monad Transformers are a Great Abstraction]] :: +- [[./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. @@ -62,7 +62,7 @@ type system. Common Lisp is a venerable programming languages like no other I know. -- [[./DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] :: +- [[./posts/DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] :: From the creation of a Lisp package up to the creation of a standalone executable. @@ -83,7 +83,7 @@ process. 4. [[/cleopatra/Contents/Coq.org][Generating Contents from Coq Documents ~(TODO)~]] 5. [[/cleopatra/Theme.html][Theming and Templating ~(TODO)~]] -- [[./Thanks.html][Thanks!]] :: +- [[./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. |