Artifact status

The artifact aims to be available and functional, being the complete mechanized Coq and Agda proofs as described in the paper, along with the full prototype implementation that runs all examples listed in the paper.