Abstract:
Statically-checked, strongly-typed languages (i.e. Haskell) allow us to use the type checker at compile time to ensure certain properties hold over our programs. However, the type systems of many languages maintain a distinction between values and their types, restricting the expressiveness of the properties.
In a dependently-typed programming language, values and types are equal and interchangeable. The value of one function could be the type of another. As a result, a richer set of properties can be expressed. Theorems about the correctness of functions can often be formulated as dependent types. Proofs of these properties are expressions of the theorem type.
In this talk, I will discuss one such language, Agda and some of my experiences using it to verify program properties.