Dependent Type Checking Modulo Associativity and Commutativity

Lucas Holten


Date: Tue, September 12, 2023
Time: 10:00
Room: F 206, building 22 (Applied Physics), meeting room E3-1
Note: This is a Masters defense.


Writing correct software is important for many applications. Dependently typed programming languages can be used to eliminate many kinds of bugs through formal proof of correctness. This proof is easy to check for a computer, but hard to write for developers. One particular task that makes writing proofs hard, is the need to reason about associative and commutative (AC) functions.

We contribute an extension of dependent type systems to fully automate AC reasoning. It works by modifying the conversion checker and doesn’t compromise soundness or completeness. Our work can help language designers decide if they want this feature 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.

Previous: Jeff Smits |
Next: Daniel Pelsmaeker |