3 files changed, 19 insertions, 2 deletions
diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org
new file mode 100644
index 0000000..9bd488d
--- /dev/null
+++ b/site/posts/StronglySpecifiedFunctions.org
@@ -0,0 +1,17 @@
+#+OPTIONS: toc:nil num:nil
+
+#+BEGIN_EXPORT html
+<h1>A Series on Strongly-Specified Functions in Coq</h1>
+#+END_EXPORT
+
+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. In this series, we explore several approaches available to Coq
+developers.
+
+- [[./StronglySpecifiedFunctionsRefine.html][Using the ~refine~ Tactics]] ::
+
+- [[./StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]] ::
diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v
index f7f84df..8ffb70c 100644
--- a/site/posts/StronglySpecifiedFunctionsProgram.v
+++ b/site/posts/StronglySpecifiedFunctionsProgram.v
@@ -3,7 +3,7 @@
     This is the second article (initially published on #<span
     id="original-created-at">January 01, 2017</span>#) of a series of two on how
     to write strongly-specified functions in Coq. You can read the previous part
-    #<a href="./StronglySpecifiedFunctions.html">here</a>#. # *)
+    #<a href="./StronglySpecifiedFunctionsRefine.html">here</a>#. # *)
 
 (** #<div id="generate-toc"></div>#
 
diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctionsRefine.v
index 5d0e69a..d9bb3aa 100644
--- a/site/posts/StronglySpecifiedFunctions.v
+++ b/site/posts/StronglySpecifiedFunctionsRefine.v
@@ -21,7 +21,7 @@
 
     #<div id="generate-toc"></div>#
 
-    #<div id="history">site/posts/StronglySpecifiedFunctions.v</div># *)
+    #<div id="history">site/posts/StronglySpecifiedFunctionsRefine.v</div># *)
 
 (** ** Is this list empty? *)