Fun - fun playing with dependent types
Jeremy
Abstract
Recently we submitted a paper about a tiny dependent typed core language. In this talk, we will demonstrate the expressiveness of the core language through several use cases. In each use case, we will briefly talk about the theory behind it, notably the explicit type casts that we use to replace the conventional conversion rule seen in most dependently typed languages like Coq, Agda and Idris. Finally we will compare our work with others’, and talk about the future work.