ucs 2.1 soon to appear on CTAN

I have just uploaded version 2.1 of the LaTeX ucs package to CTAN, so it should appear there within the next few days. Some small bugs have been fixed, and mappings for several characters, mostly musical notes and special arrows, have been added. A big thank you goes to Ralf Meyer, who has contributed considerably to this release. Continue reading

Slides of my MFPS talk now online

MFPS took place a month ago, and today I finally managed to publish the slides of my talk ;-). The topic of these slides is similar to the topic of the seminar talk I gave at 10 May, but the overlap is not too large. So you might be interested in having a look.

Talk about categorical models of temporal logic and FRP

I recently gave a talk about the main points of my MFPS ’12 paper. The title of the talk was Categorical Models for Two Intuitionistic Modal Logics. Continue reading

Category theory crash course

I recently gave an introduction to category theory at the Institute of Cybernetics. This crash course introduced several of the basic categorical notions that are of interest from a computer science and logic perspective, while assuming no previous knowledge about category theory. Everything necessary to understand my upcoming talk about categorical models of modal logics was covered. Continue reading

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

Natural numbers in Haskell

It is a bit surprising that Haskell has no type for natural numbers. The Haskell Report defines only Integer for, well, integers and Int for integers that are reasonably small. The base package then adds Word as the unsigned variant of Int as well as types for signed and unsigned integers with a fixed number of bits. An unsigned variant of Integer is missing. Continue reading

New Foundations

It was around the beginning of my undergraduate studies when I became interested in foundations of mathematics in general and axiomatic set theory in particular. Shortly after, I started reading parts of Abraham Fraenkel’s brilliant book Einleitung in die Mengenlehre. I read the second edition of this book, which had originally been published in the 1920ies. In his book, Fraenkel first introduces set theory in a naïve way, then discusses certain paradoxes arising from the naïve treatment, and finally presents the axiomatic set theory developed by Ernst Zermelo and himself.

A few weeks ago, I stumbled across set theory again when Sergei Tupailo gave two talks at the Institute of Cybernetics on an alternative axiomatic set theory called New Foundations. The first talk was about a classical proof by Ernst Specker, the second one was about a contribution by Tupailo himself. Tupailo’s talks caused me to have a look at these “new foundations”, which were, in fact, completely new to me. In this blog post, I want to tell you a bit about this interesting topic. Continue reading