Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

Linear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n-1) + f(n-2) and the quite non-obvious closed form (φ^n - (-φ)^(-n)) / sqrt(5) where φ is the golden ratio. The work presented here builds on existing tools in Isabelle/HOL – such as formal power series and polynomial factorisation algorithms – to develop a theory of these recurrences and derive a fully executable solver for them that can be exported to programming languages like Haskell. Based on this development, I also provide an efficient method to prove ‘Big-O’ asymptotics of a solution automatically without explicitly finding the closed-form solution first.

Tue 15 Jan

16:00 - 17:30: CPP 2019 - Research Papers: Formalization of Mathematics and Computer Algebra at Sala XII
Chair(s): Zhong ShaoYale University
CPP-201916:00 - 16:30
Research paper
Yannick ForsterSaarland University, Dominik KirstSaarland University, Gert SmolkaSaarland University
CPP-201916:30 - 17:00
Research paper
Manuel EberlTechnische Universität München
CPP-201917:00 - 17:30
Assia MahboubiINRIA, Magnus O. MyreenChalmers University of Technology, Sweden