This repository contains the mechanised proof of soundness for the OOPSLA 2022 paper "A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning".
The initial "kick the tires" guide for getting started with the mechanisation can be found here and as a PDF here.
The detailed "step by step" guide explaining how to inspect the mechanised proof can be found here and as a PDF here.
- The
cdot/
directory contains sources of the mechanization of the iDOT calculus. The proof is an extension of pDOT soundness proof. - The
lambda2GMu/
directory contains sources of the mechanization of the Lambda2Gmu calculus andlambda2GMu_annotated/
contains sources of the variant with additional type annotations, as described in the paper. - The
translation/
directory contains lemmas related to the translation: the typing of thelib
term and an example showing inversion of tuple equality using our added inversion rules.