Practical dependent type checking using twin types. - Víctor López Juan; Nils Anders Danielsson (TyDe@ICFP, 2020)