print · source · login   

Made Available Software

  • The department is well known for its work on the functional programming language Clean.
    Like Haskell it is a pure and lazy functional language, additionally offering some special feautures like Uniqueness Typing, a hybride type system offering dynamics in addition to static typing, and support for type-driven generic functions. The compiler is very fast, and it generates excellent code.

  • iTask Much of the current Clean related research is focused around the iTask system. This is a toolkit for building web-based workflow management systems using a powerful workflow language embedded in Clean

  • SAPL To enable the execution of applications written in a functional language in a browser, we have an option to compile functional programs to JavaScript. Originally it has been developed to allow the execution of iTask tasks written in Clean on clients.
    Laszlo Domoszlai has made a stand-alone version enabling both Clean as well Haskell functions to be compiled to JavaScript such that they can be executed in the browser. It uses an interpreter technique invented by Jan-Martin Jansen.
  • TOMTE, a tool that fully automatically constructs abstractions for automata learning
  • Iris is a framework for program verification using higher-order concurrent separation logic, embedded in the Coq proof assistant. Iris involves active collaboration with (among others) Aarhus University, BedRock Systems, Boston College, CNRS/LRI, Groningen University, INRIA, ITU Copenhagen, KU Leuven, Microsoft Research, MIT, MPI-SWS, NYU, Saarland University, and Vrije Universiteit Brussel, and has been applied to languages like Rust, Go, OCaml, C, Scala, and more. See for more information.

  • std++ is an extended "Standard Library" for Coq, with extensive support for common data structures like lists, sets, maps, multisets. The development of std++ is led by Robbert Krebbers (Radboud University) and Ralf Jung (MPI-SWS), and has an active number of contributors.