[Agda] Challenge: can you exploit a known bug in Cubical Agda?
jan.bessai at tu-dortmund.de
Tue Oct 18 19:50:12 CEST 2022
We still have room for a presentation at the Unsound workshop:
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 -> ...]
> [phi -> ..., forall i phi -> ...].
> Details of the bug (and the fix) are at:
> 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
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda