Category Archives: Software

Mathematically Structured but not Necessarily Functional Programming

These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now.

Abstract: Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions as types, because it allows the realizers to use computational effects such as non-termination, store and exceptions. Therefore, we can use realizability as a framework for program development and extraction which allows any style of programming, not just the purely functional one that is supported by the Curry-Howard correspondence. In joint work with Christopher A. Stone we developed RZ, a tool which uses realizability to translate specifications written in constructive logic into interface code annotated with logical assertions. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools. In our experience, RZ is useful for specification of non-trivial theories. While the use of computational effects does improve efficiency it also makes it difficult to reason about programs and prove their correctness. We demonstrate this fact by considering non-purely functional realizers for a Brouwerian continuity principle.

Download: msfp2008-slides.pdf, msfp2008-abstract.pdf

Miniprolog

I have aded to the PL Zoo a mini prolog interpreter. It really is minimalistic, as it only handles pure Horn clauses. There is no arithmetic, lists, cuts, or disjunctions. Nevertheless, it ought to be possible to write a miniml interpreter in it… If anyone does it, please send me the code!

A toy call-by-push-value language

I have added two new languages to the PL Zoo. The minor addition is miniml+error, which is just MiniML with an error exception (raised by division by 0) that cannot be caught. The purpose is to demonstrate handling of fatal errors during runtime. The more interesting new animal is levy (written by Matija Pretnar and myself), an implementation of Paul Levy’s call-by-push-value language. If you only know about Haskell’s call-by-name and ML’s call-by-value, I invite you to learn about call-by-push-value. Start by reading Paul’s FAQ.

Exact real arithmetic in Haskell

HERA is an implementation of exact real arithmetic in Haskell using the approach by Andrej Bauer and Iztok Kavkler, see these and these slides. It uses the fast multiple precision floating point library MPFR. Download source, and see documentation and examples of usage at my home page.

[Note by Andrej: this is a guest post by Aleš Bizjak, a first-year student of mathematics at my department. I am very proud of the excellent work he did on his summer project.]

An object-oriented language Boa

I have added another language, called Boa, to the Programming Languages Zoo. It is an object-oriented language with the following features:

  • integers and booleans as base types,
  • first-class functions,
  • dynamically typed,
  • objects are extensible records with mutable fields,
  • there are no classes, instead we can define “prototype” objects and extend them
    to create instances.

Continue reading An object-oriented language Boa

The Programming Languages Zoo

I teach Theory of Programing Languages (page in Slovene). For the course I implemented languages which demonstrate basic concepts such as parsing, type checking, type inference, dynamic types, evaluation strategies, and compilation. My teaching assistant Iztok Kavkler contributed to the source code as well. I decided to publish the source code as a Programming Language Zoo for anyone who wants to know more about design and implementation of programming languages.
Continue reading The Programming Languages Zoo