blob: 805b944992ecff50602bf84516fb060b66faab6f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

#+OPTIONS: toc:nil num:nil
#+BEGIN_EXPORT html
<h1>A Series on StronglySpecified 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 “stronglyspecified” 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 dependentlytyped functions can
be challenging. In this series, we explore several approaches available to Coq
developers.
 [[./StronglySpecifiedFunctionsRefine.html][Implementing StronglySpecified Functions with the ~refine~ Tactic]] ::
 [[./StronglySpecifiedFunctionsProgram.html][Implementing StronglySpecified Functions with the ~Program~ Framework]] ::
