Dependent Type-Checking Modulo Associativity and Commutativity
L.H.C. Holten (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Programming Languages)
L.F.B. Escot – Mentor (TU Delft - Programming Languages)
MM Weerdt – Graduation committee member (TU Delft - Algorithmics)
More Info
expand_more
Source code for the Agda implementation of definitional AC functions.
https://github.com/LHolten/agda-commassocOther than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Writing software that follows its specification is important for many applications. One approach to guarantee this is formal verification in a dependently-typed programming language. Formal verification in these dependently-typed languages is based on proof writing. Sadly, while proofs are easy to check for computers, writing proofs can be tedious for developers. One particular proof component that currently requires developers attention in many systems, is associative and commutative (AC) reasoning.
We contribute an extension of dependent type-systems to fully automate AC reasoning. This alleviates developers from this task and allows them to concentrate on other proof components. Our approach works by modifying the conversion checker and doesn't compromise soundness or completeness. Furthermore, our approach reuses existing type-checking components, making it easier to implement. We also implemented our theory as an extension of the Agda type-checker. This allowed us to use this implementation to experiment with some example programs.
This thesis can help language designers decide if they want automatic AC reasoning in their language. For language users it can serve as inspiration on how to use such a type-system and finally for researchers we have ideas for future work.