Towards a typed linear algebra formal semantics for spreadsheets

Abstract

This master dissertation addresses the problem of spreadsheet errors by using typed linear algebra in spreadsheet design. The study builds on previous efforts to solve this issue and presents an approach to improve the quality and reliability of spreadsheet systems. The outcome of this study shows that the adoption of a typed linear algebra approach in spreadsheet design can significantly reduce the risk of errors and improve the reliability of spreadsheet-based systems. The tool developed in this dissertation allows users to derive spreadsheet models in Haskell from formal specifications, which are then translated into a particular spreadsheet format. This process helps to ensure the accuracy and consistency of the generated spreadsheets, as it is based on precise and well typed specifications. Additionally, the use of typed linear algebra in the semantics of spreadsheet functions and constructions such as e.g. running totals provides a solid foundation for the correctness. Overall, the results of this study demonstrate the effectiveness of the typed linear algebra approach in improving the quality and reliability of spreadsheet systems.

Esta dissertação de mestrado aborda o problema de erros em folhas de cálculo, utilizando álgebra linear tipada no design de folhas de cálculo. O estudo baseia-se em esforços anteriores para resolver esta questão e apresenta uma abordagem para melhorar a qualidade e a confiabilidade de sistemas de folha de cálculo. Os resultados deste estudo mostram que a introdução de uma abordagem de álgebra linear tipada no design de folhas de cálculo pode reduzir significativamente o risco de erros e melhorar a confiabilidade dos sistemas de folhas de cálculo. A ferramenta desenvolvida nesta dissertação permite que os utilizadores criem especificações em Haskell de folhas de cálculo, que são então traduzidas para uma folha de cálculo correspondente. Este processo ajuda a garantir a precisão e a consistência da folha de cálculo gerada, pois ela é baseada numa especificação precisa e bem definida. Além disso, o uso de álgebra linear tipada na semântica de funções de folhas de cálculo e construções, como totais acumulados, proporciona uma base sólida para a correção destes elementos. Em geral, os resultados deste estudo demonstram a eficácia da abordagem de álgebra linear tipada na melhoria da qualidade e confiabilidade dos sistemas de folhas de cálculo.