Vector representation comparison

[blaxill]

As a low priority side task I'd like us to collect vector representations.

We've talked about using a different vector representation, but it's difficult to make an informed decision without experimentation. This could also help us have more concrete reasoning on when to dependently type datatypes vs simpler typing.

[atondwal]

Might be worth looking into the tools by Ringer et al --- their motivating example is typically lifting proofs about lists to vectors

On Mon, Apr 12, 2021 at 7:29 AM Ben Blaxill @.***> wrote:

As a low priority side task I'd like us to collect vector representations.

We've talked about using a different vector representation, but it's difficult to make an informed decision without experimentation. This could also help us have more concrete reasoning on when to dependently type datatypes vs simpler typing.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/project-oak/silveroak/issues/731, or unsubscribe https://github.com/notifications/unsubscribe-auth/AACTYCEWSCBEEGFTXMWUS23TIL7VHANCNFSM42ZNDIBA .