Proof-Producing Synthesis of CakeML from Monadic HOL Functions. Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan. Journal of Automated Reasoning, 64, 1287–1306, 2020. 2020
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic.Takamasa Okudono and Andy King. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science, vol 12078. 2020