The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

I think using this for optimization by memoization is feasible, since by moving a fold into the index of a type itself, you are storing the result, and retrieval should be constant time. If you have a specific use case you are thinking of, I would love to see it. It's a use case I had entertained, but I hadn't fleshed it out with a particular example.

The conversion of functions and proofs works by a program transformation directly on the terms. 

On Fri, Mar 22, 2019, 10:58 PM Siddharth Bhat <siddu.druid AT gmail.com> wrote:

Hey,

This is cool stuff! 

How does the automatic conversion from non indexed to indexed types work? I'd love some insight into this. Does this automatically provide the indexed versions of say, getters and setters? Could this be used to increase performance asymptotically (O(n) to O(1) for things like indexing), while still keeping proofs easy (since we can reason over the inductive list structure)?

Thanks a ton,

~Siddharth

On Sat, 23 Mar, 2019, 11:23 Talia Ringer, <tringer AT cs.washington.edu> wrote:

Hi all,

I'm excited to release a plugin I've been working on with Nate Yazdani. The plugin is called DEVOID, and the code is here.

The basic idea of the plugin is to derive functions and proofs over indexed types like vectors from non-indexed versions of those types like lists. It can do this automatically for a certain class of types without any extra user input. For example, you don't have to supply the relation between lists and vectors; the tool finds it automatically.

This is a preliminary release of the tool, which has some glitches to iron out, but if you're interested, take a look at the plugin and play with some of the examples. I'd love feedback, bug reports, external contributions, and so on.

Best,

Talia

--

Sending this from my phone, please excuse any typos!