This paper applies long short-term memory models to precipitation disaggregation. In particular, it shows promising results in the Australian context, reducing error compared to previous attempts by around 30%.

This paper compares the Coq and Idris2 interactive theorem provers to provide a qualitative evaluation of their performance via a proof of the correctness of insertion sort. The paper’s key contribution is comparing these systems through a user experience lens, rather than purely the underlying logic upon which the system relies.