Stream: MetaCoq

Topic: Efficient substitutions For Reals


view this post on Zulip Pierre-Marie Pédrot (Dec 08 2020 at 16:43):

Dear MetaCoq mother brain, I'd like to bring to your attention the following Coq PR: https://github.com/coq/coq/pull/13537. It's an asymptotically efficient implementation of substitutions to be used in the kernel. It's a nifty structure I am quite proud of, which boils down to the infernal hybrid of Okazaki skewed lists with a writer monad tracking shifts. I may probably write a blog post on the topic when I have a bit of time, but in the meantime, I thought that if you were fed up with η-expansion, you might give a try at its implementation (and proof of correctness) in MetaCoq. It's a purely functional data structure that is quite easily implemented in Coq, so the proof shouldn't be too hard. Who knows, it might even be useful for your own development...

view this post on Zulip Pierre-Marie Pédrot (Dec 08 2020 at 16:43):

Forgot to mention the efficiency: O(1) cons and O(log n) retrieval.

view this post on Zulip Matthieu Sozeau (Dec 08 2020 at 18:19):

I looks like it could go into a general "wishes for formalization" list that people interested in learning/developing MetaCoq could tackle, I'll link it from there.


Last updated: Aug 11 2022 at 01:03 UTC