| layout | post |
|---|---|
| title | Fun - fun playing with dependent types |
| authors | Jeremy |
| date | 2015-09-10 14:30:00 +0800 |
| venue | CB 313 |
| categories | Jeremy 2015 |
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.