site/posts/CleopatraV1.org

+#+END_EXPORT
+
~Makefile~ serves two purposes: it initiates a few global variables, and it
provides a rule to generate ~bootstrap.mk~. At this point, some readers may
wonder /why/ we need ~Makefile~ in this context, and the motivation behind this
diff --git a/site/posts/ClightIntroduction.v b/site/posts/ClightIntroduction.v
index 0d53f33..13bf773 100644
--- a/site/posts/ClightIntroduction.v
+++ b/site/posts/ClightIntroduction.v
@@ -8,10 +8,9 @@ Import ListNotations.
you write is preserved by CompCert compilation passes up to the generated
machine code.
- I have been interested in CompCert for quite some times now. Today (##March 18, 2020##), I have challenged myself to study
- Clight and its semantics. This write-up is the result of this challenge,
- written as I was progressing.
+ I had been interested in CompCert for quite some times, and ultimately
+ challenged myself to study Clight and its semantics. This write-up is the
+ result of this challenge, written as I was progressing.
##
diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.org b/site/posts/ExtensibleTypeSafeErrorHandling.org
index 3af3d44..cc276f0 100644
--- a/site/posts/ExtensibleTypeSafeErrorHandling.org
+++ b/site/posts/ExtensibleTypeSafeErrorHandling.org
@@ -1,8 +1,8 @@
#+BEGIN_EXPORT html
This article has originally been published on February 04, -2018.

+This article has originally been published on February 04, 2018.

#+END_EXPORT #+TOC: headlines 2 diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v index 1bc9907..bd539e7 100644 --- a/site/posts/Ltac101.v +++ b/site/posts/Ltac101.v @@ -1,12 +1,12 @@ (** * Ltac 101 - This article has originally been published on #October - 16, 2017#. *) + This article has . *) -(** In this article, I give an overview of my findings about the Ltac language, - more precisely how it can be used to automate the construction of proof - terms. If you never wrote a tactic in Coq and are curious about the subject, - it might be a good starting point. *) +(** In this article (originally published on #October 16, 2017#), I give an overview of my + findings about the Ltac language, more precisely how it can be used to + automate the construction of proof terms. If you never wrote a tactic in Coq + and are curious about the subject, it might be a good starting point. *) (** ## diff --git a/site/posts/MonadTransformers.org b/site/posts/MonadTransformers.org index 4c28fe5..b2bd2ca 100644 --- a/site/posts/MonadTransformers.org +++ b/site/posts/MonadTransformers.org @@ -1,8 +1,8 @@ #+BEGIN_EXPORT htmlThis article has originally been published on July 15, -2017.

+This article has originally been published on July 15, 2017.

#+END_EXPORT #+OPTIONS: toc:nil diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v index 9c2efaf..0020a3e 100644 --- a/site/posts/RewritingInCoq.v +++ b/site/posts/RewritingInCoq.v @@ -1,17 +1,13 @@ -(** * Rewriting in Coq - - This article has originally been published on #May 13, - 2017.# *) - -(** I have to confess something. In the published codebase of SpecCert lies a - shameful secret. It takes the form of a set of axioms which are not - required. I thought they were when I wrote them, but it was before I heard - about “generalized rewriting,” setoids and morphisms. - - Now, I know the truth. I will have to update SpecCert eventually. But, - in the meantime, let me try to explain how it is possible to rewrite a - term in a proof using a ad-hoc equivalence relation and, when - necessary, a proper morphism. *) +(** * Rewriting in Coq *) + +(** I have to confess something. In the codebase of SpecCert lies a shameful + secret. It takes the form of a set of unnecessary axioms. I thought I + couldn’t avoid them at first, but it was before I heard about “generalized + rewriting,” setoids and morphisms. Now, I know the truth, and I will have + to update SpecCert eventually. But, in the meantime, let me try to explain + in this article originally published on #May + 13, 2017 how it is possible to rewrite a term in a proof using a + ad-hoc equivalence relation and, when necessary, a proper morphism. *) (** ## diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v index ac55b7e..5d0e69a 100644 --- a/site/posts/StronglySpecifiedFunctions.v +++ b/site/posts/StronglySpecifiedFunctions.v @@ -1,11 +1,11 @@ -(** * Strongly-Specified Functions in Coq, part 1: using the <