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

  • mTask The mTask system is a framework for programming complete IoT systems from a single source.The framework is powered by a multi-backend tagless embedded DSL embedded in the pure functional programming language Clean.With the bytecode generation backend and the iTask integration, mTask tasks can be embedded in iTask programs and shared data sources can be synchronized.The client runtime system runs on embedded devices such as Arduino/ESPxxx/Nucleo boards or on regular devices running linux, windows or mac.Traditionally IoT architectures are tiered architectures where different languages, protocols and paradigms are used in different layers.The mTask system generates all tiers from a single source specification.
  • 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.
  • TorXakis, an experimental model-based testing tool, based on the ioco-testing theory for labelled transition systems.