Almost every programming language possess some kind of type system. These systems ensures some safety over the code execution, be it statically at compile-time or dynamically at run-time. Effectively, these types encode a specification of an object, allowing them to be composed in a relatively safe manner. Most type systems only allow for weak specifications, for instance there is no way to say that a list is sorted in its type. This is something you can do with dependent types, which was first introduced by Per Martin-Löf in 1972. This, together with the relationship between programs and proofs knows as the Curry-Howard correspondence, allows us to treat programs written in these type systems as proofs.

In this talk I will explain the correspondence between propositional logic and simply typed lambda calculus, and show how this extends to dependent types. I will also explain what a dependent type is and show examples of these types in Agda and Coq, which are both proof assistants and programming languages.