Reseña: Stream fusion for Isabelle’s code generator
Se ha publicado un artículo de automatización del razonamiento formalizado en Isabelle/HOL Stream fusion for Isabelle’s code generator.
Sus autores son Andreas Lochbihler y Alexandra Maximova (del Information Security Group en la Escuela Politécnica Federal de Zúrich, Suiza).
Su resumen es
Stream fusion eliminates intermediate lists in functional code. We formalise stream fusion for finite and coinductive lists in Isabelle/HOL and implement the transformation in the code preprocessor. Our initial results show that optimisations during code extraction can boost the performance of the generated code, but the transformation requires further engineering to be usable in practice.
Su contenido es un resumen de la tesis de Máster Stream Fusion for Isabelle’s Code Generator realizada por Alexandra Maximova y dirigida por Andreas Lochbihler.
El trabajo se presentó el 25 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).
El código de las correspondientes teorías en Isabelle se encuentra aquí.