Static type systems are ubiquitous in programming languages. Many of the most popular languages like C and Java have static type systems. Static types give the programmer some level of guarantee that their program won't contain runtime errors by checking types at compile time. However, the level of safety guaranteed by the type system varies widely on the implementation and there are certainly plenty of type systems that are more expressive and powerful than the ones found in mainstream languages. Today we will be looking at one such group of type systems which support dependent types.