Roman Leshchinskiy University of New South Wales Proofs in Haskell Under the Curry-Howard isomorphism, types and terms are interpreted as propositions and proofs, respectively. This correspondence forms the basis of automated theorem provers and also of dependently typed languages which are becoming increasingly popular. The latter allow us to reason about the properties and correctness of programs in the same language they are written in. But is the full power of dependent types really necessary for this? In this talk we demonstrate that a combination of recent extensions to Haskell can already take us a long way. We show how to encode a simple predicate logic within the type system and how to use it for reasoning about values by reflecting the latter on the type level. The resulting system is surprisingly powerful and allows us to prove many standard properties of data structures and programs.