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. Continue reading

New release of the ucs LaTeX package

The ucs package provides advanced support for using UTF-8 as the input encoding of LaTeX files. It goes much beyond the standard UTF-8 support of LaTeX. In particular, it enables you to use non-ASCII characters in the LaTeX input of mathematical formulas. This feature is particularly important for Agda programmers that use lhs2TeX to typeset their code. The lhs2TeX preprocessor relies on ucs for typesetting all those mathematical symbols and greek letters that you typically find in Agda code.

The ucs package was originally developed by Dominique Unruh. Dominique had stopped working on ucs several years ago. In 2011, I took over the maintainer role. Now, I have made a new release – which is the first ucs release since 7.5 years. The current version is 2.0. At the time of writing, it is available on CTAN and in TeXLive. Continue reading