Dependently typed programming and theorem proving in Haskell

Programming languages with dependent types allow us to specify powerful properties of values using the type system. By employing the Curry–Howard correspondence, we can also use these languages as proof languages for higher-order logics. In this blog post, I want to demonstrate that Haskell as supported by the Glasgow Haskell Compiler (GHC) can give us almost the same features.

Introduction

So I have finally set up my blog on various things that I am interested in and that are roughly related to my work. In the near future, you should be able to read here about topics ranging from foundations of mathematics to text editors.