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.

New paper about categorical models of temporal logic and FRP

Temporal logic and functional reactive programming are related via a Curry–Howard correspondence, as has recently be shown by Alan Jeffrey and by myself. Given this intriguing connection, it seems to be worthwhile to look for a common categorical semantics of temporal logic and FRP. This undertaking is a current research topic of mine. I will present some results on this at this year’s MFPS conference under the title Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming. A preprint of the corresponding paper is now available online.

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.