Type-level Property Based Testing

Thomas Ekström Hansen, Edwin Brady

We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking a…