totality-checker
This repository is a work-in-progress Haskell implementation of a type checker with dependent types and totality checks. The totality checks include
- strict positivity checks,
- pattern matching coverage checks, and
- termination checks.
I follow some of the works of
-
Termination checking for a dependently typed language by Karl Mehltretter (2007) and
-
Towards a practical programming language based on dependent type theory by Ulf Norell (2007).
-
Elaborating dependent (co)pattern matching: No pattern left behind by Jesper Cockx and Andreas Abel (2020)
See the reference for a complete reference.