The Coq mailing list

[Xuanrui Qi <xqi01 AT cs.tufts.edu>]

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!