[Agda] Challenge: can you exploit a known bug in Cubical Agda?

[Jan Bessai]

We still have room for a presentation at the Unsound workshop:
https://2022.splashcon.org/home/unsound-2022

The topic is a perfect match and if someone is willing and able to talk about
this, you'd be very welcome!

On Tue, Oct 18, 2022 at 10:58:08AM +0200, Andreas Abel wrote:
> Tom Jack has found a bug in the implementation of transp for Glue (and hcomp
> for U) in Cubical Agda, where a system that should be
> 
>    [psi -> ..., forall i phi -> ...]
> 
> became
> 
>    [phi -> ..., forall i phi -> ...].
> 
> Details of the bug (and the fix) are at:
> 
>   https://github.com/agda/agda/pull/6197
> 
> Question: can one exploit this bug with reasonable resources?
> 
> In particular, we are using for a rather short test case that either
> - makes Agda crash, or
> - proves False.
> 
> Ideally, this test should run in reasonable time (less than a minute, say)
> using reasonable resources (not more than 4G memory), so we can add it to
> the regression test suite.
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
> 
> andreas.abel at gu.se
> http://www.cse.chalmers.se/~abela/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda