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

# Monthly Archives: April 2012

# 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. 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