The Coq mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

You might also be interested in our paper:

  A Coq Library For Internal Verification of Running-Times
  McCarthy, Fetscher, New, Feltey, Findler
  Science of Computer Programming (SCP) 2018
  https://www.eecs.northwestern.edu/~robby/pubs/papers/scp2018-mfnff.pdf

There are some other good papers that are worth checking out described
in the related work section, too.

(It actually was first at FLOPS in 2016; Elsevier took a surprisingly
long time to publish the revised version.)

Robby

On Thu, Oct 18, 2018 at 9:50 AM Xuanrui Qi 
<xqi01 AT cs.tufts.edu>
 wrote:
>
> Hello Siddharth,
>
> In general, to prove things about complexity, you would define a cost
> semantics, i.e. a recursive running function that defines time costs.
> Then you'd prove your desired complexity properties against that.
>
> Here's a recent paper about formalizing and proving amortized
> complexity in a theorem prover (but Isabelle, not Coq): "Amortized
> Complexity Verified", by Tobias Nipkow, in ITP '15 (
> http://isabelle.in.tum.de/~nipkow/pubs/itp15.pdf).
>
> Also, for something in Coq, there's Arthur Charguéraud and François
> Pottier's 2017 JAR paper, "Verifying the Correctness and Amortized
> Complexity of a Union-Find Implementation in Separation Logic with Time
> Credits". Those might be helpful.
>
> I'm not an expert in cost semantics, so this is just to get you
> started. I suppose the list knows much more about the specifics of
> functional cost analysis.
>
> -Ray
>
> --
> Xuanrui "Ray" Qi
>
> Department of Computer Science
> Tufts University
> Halligan Hall, 161 College Ave
> Medford, MA 02144, USA
>
> Email: 
> xqi01 AT cs.tufts.edu
>
> On Thu, 2018-10-18 at 19:49 +0530, Siddharth Bhat wrote:
> > Hello,
> >
> > I was interested in implementing data structures from Okasaki's
> > "purely functional data structures", but I'm not sure how to actually
> > prove theorems about the amortized analysis -- in terms of the
> > banker's method / physicist's method, while still being able to
> > extract such a data structure out to Haskell code.
> >
> > So, TL;DR:
> > How do I define data structures in Coq such that it is:
> > 1. Extractable to code
> > 2. Allows reasoning to prove bounds using Okasaki's methods?
> >
> > Thanks,
> > ~Siddharth
> > --
> > Sending this from my phone, please excuse any typos!
>