Matúš Tejiščák
ziman@functor.sk
Erasure in Dependently Typed Programming
— PhD dissertation, 2020
A Dependently Typed Calculus with Pattern Matching and Erasure Inference
— paper appearing in ICFP 2020