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

Andreas Abel abela at chalmers.se
Tue Oct 18 10:58:08 CEST 2022

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

More information about the Agda mailing list