The PARKAS group runs and contributes to several software projects.

Find us on GitHub.


Synchronous programming with ODEs.

Zélus is an experimental language for simulating hybrid systems. It is a first-order synchronous language without clocks that has been augmented with first-order Ordinary Differential Equations (ODEs) that can be reset. Hybrid programs are compiled into the discrete subset and executed by an external numerical solver; currently the Sundials CVODE solver via an OCaml Interface.


Hunting concurrency compiler bugs.

Compilers sometimes generate correct sequential code but break the concurrency memory model of the programming language: these subtle compiler bugs are observable only when the miscompiled functions interact with concurrent contexts, making them particularly hard to detect. The cmmtest tool performs differential testing to hunt concurrency compiler bugs in C and C++ compilers against the C11/C++11 memory model. The tool has identified several mistaken write introductions and other unexpected behaviours in the latest release of the gcc compiler.


Contributions to the GNU Compiler Collection.

Licence: GPLv3+ and LGPLv3+

The GNU Compiler Collection includes front ends for C, C++, Objective-C, Fortran, Java, Ada, and Go, as well as libraries for these languages (libstdc++, libgcj,...). GCC was originally written as the compiler for the GNU operating system. The GNU system was developed to be 100% free software, free in the sense that it respects the user's freedom.

PARKAS contributes to the polyhedral compilation framework, Graphite. The team also distributes OpenStream, an experimental stream-programming extension of OpenMP, borrowing key design elements from synchronous and data-flow languages. Members of the team contributed to the design and implementation of the induction variable analysis framework of GCC.


Lustre with discrete controller synthesis and arrays.

Heptagon is a synchronous dataflow language whose syntax and semantics is inspired from Lustre, with a syntax allowing the expression of control structures (e.g., switch or mode automata).

Heptagon is also a research compiler, whose aim is to facilitate experimentation. The current version of the compiler includes the following features:

  • Inclusion of discrete controller synthesis within the compilation: the language is equipped with a behavioral contract mechanisms, where assumptions can be described, as well as an "enforce" property part. The semantics of this latter is that the property should be enforced by controlling the behaviour of the node equipped with the contract. This property will be enforced by an automatically built controller, which will act on free controllable variables given by the programmer. This extension has been named BZR in previous works.

  • Expression and compilation of array values with modular memory optimization. The language allows the expression and operations on arrays (access, modification, iterators). With the use of location annotations, the programmer can avoid unnecessary array copies.

Heptagon is developed in the Parkas (ENS) and Pop-Art (LIG/INRIA) research teams.


Integer Set Library.

Licence: MIT

isl is a library for manipulating sets and relations of integer points bounded by linear constraints. Supported operations on sets include intersection, union, set difference, emptiness check, convex hull, (integer) affine hull, integer projection, and computing the lexicographic minimum using parametric integer programming. It also includes an ILP solver based on generalized basis reduction and transitive closure computation heuristics. It comes with a state-of-the-art code generator and supports a hybrid syntax-tree/polyhedral representation of programs.


A high-level programming language for digital circuits.

Jazz is a high-level programming language for expressing, in a concise and accurate way, large digital synchronous circuits. From a language-designer perspective, Jazz is a declarative, single-assignment, higher-order, lazy, functional, and object-oriented language with parameterized types and multi-methods.

Jazz is strongly-typed (with a type-system derived from ML-sub) and supports both the explicit and implicit declaration of variables and methods thanks to a powerful constraint-based type-inference algorithm. The syntax of Jazz and its object model are Java-like and should look familiar to any Java programmer.


Contributions to the LLVM Compiler Infrastructure.

Licence: University of Illinois/NCSA Open Source License

LLVM is a collection of modular and reusable compiler and toolchain technologies. Its core libraries provide a modern source- and target-independent optimizer, along with code generation support for many CPUs. These libraries are built around a well specified code representation known as LLVM IR.

PARKAS contributes to the polyhedral compilation framework, Polly, and hosts the Polly Labs research and technology transfer in LLVM-based polyhedral compilation.

Lucid Synchrone

Higher-order synchronous dataflow programming.

Lucid Synchrone is an experimental language for the implementation of reactive systems. It is based on the synchronous model of time as provided by Lustre combined with some features from ML languages. The main characteristics of the language are the following:

  • It is a strongly typed, higher-order functional language managing infinite sequences or streams as primitive values. These streams are used for representing input and output signals of reactive systems and are combined through the use of synchronous data-flow primitives à la Lustre.
  • The language is founded on several type systems (e.g., type and clock inference, causality and initialization analysis) which statically guarantee safety properties on the generated code.
  • Programs are compiled into sequential imperative code.
  • The language is built above Objective Caml used as the host language. Combinatorial values are imported from Objective Caml and programs are compiled into Objective Caml code. A simple module system is provided for importing values from the host language or from other synchronous modules.


An n-synchronous extension of Lustre.

Lucy-n is a language to program in the n-synchronous model. The language is similar to Lustre with a buffer construct. The Lucy-n compiler ensures that programs can be executed in bounded memory and automatically computes buffer sizes. Hence this language allows to program Kahn networks with bounded FIFOs.


A tool for the working semanticist.

Ott is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition.


Polyhedral Parallel Code Generator

Licence: MIT

PPCG is our source-to-source research tool for automatic parallelization in the polyhedral model. It serves as a test bed for many compilation algorithms and heuristics published by our group, and is currently the best automatic parallelizer for CUDA and OpenCL on the Polybench suite and a variety of benchmarks.

PPCG compiles a subset of C99 with parallelization- and acceleration-friendly extensions called PENCIL. An overview paper was published at the PACT 2015 conference.

pencilcc is a more complete and integrated framework built on top of PPCG, with additional support for PENCIL, accelerated runtime interfaces to OpenCL devices, and multiple additional quirks. A tutorial recapitulates the design of PENCIL and the practical usage of pencilcc.


A programming language for interactive systems.

Compiler licence: Q Public Licence 1.0

Library licence: GNU Library General Public Licence 2.0

ReactiveML is a programming language dedicated to the implementation of interactive systems as found in graphical user interfaces, video games or simulation problems. ReactiveML is based on the synchronous reactive model of Boussinot embedded in an ML language (here Objective Caml). The synchronous reactive model provides synchronous parallel composition and dynamic features like the dynamic creation of processes. In ReactiveML, the reactive model is integrated at the language level (not as a library) which leads to safer and more natural programming.


OCaml interface to the Sundials numeric solvers.

[Sundials/ML] 1 is a comprehensive OCaml interface to the [Sundials] 2 suite of numerical solvers (CVODE, CVODES, IDA, IDAS, KINSOL, ARKODE). Its structure mostly follows that of the Sundials library, both for ease of reading the existing documentation and for adapting existing source code, but several changes have been made for programming convenience and to increase safety, namely:

  • solver sessions are mostly configured via algebraic data types rather than multiple function calls;
  • errors are signalled by exceptions not return codes (also from user-supplied callback routines);
  • user data is shared between callback routines via closures (partial applications of functions);
  • vectors are checked for compatibility (using a combination of static and dynamic checks); and
  • explicit free commands are not necessary since OCaml is a garbage-collected language.

OCaml versions of the standard examples usually have an overhead of about 50% compared to the original C versions, and almost never more than 100%.


A Lustre compiler in Coq

Vélus is a compiler for a subset of Lustre and Scade that is specified in Coq (with some OCaml. It integrates the CompCert C compiler to define the semantics of machine operations (integer addition, floating-point multiplication, etcetera) and to generate assembly code for different architectures. The research challenges are

  1. to mechanize (i.e., put into Coq) the semantics of the programming constructs used in modern languages for Model-Based Development;
  2. to implement compilation passes and prove them correct;
  3. to interactively verify source programs and guarantee that the obtained invariants also hold of the generated code.

This project is a collaboration with Lélio Brun, Pierre-Évariste Dagand, Paul Jeanmaire, Xavier Leroy, Marc Pouzet, and Lionel Rieg.


LaTeX package for compiling verbatim text.

User manuals and papers about programming languages usually contain many code samples, often with accompanying compiler messages giving the types of declarations or error messages explaining why certain declarations are invalid.

The checklistings package augments the fancyvrb and listings packages for including source code in LaTeX documents with a way to pass the source code through a compiler and also include the resulting messages in the document.

The motivation is to check the code samples in a document for syntax and typing errors and to facilitate the inclusion of inferred types and compiler warnings or errors in a text. This package is intentionally very lightweight and unlike packages like python it is not intended for interacting with an interpretor or including the execution traces of code. While checklistings does not focus on a specific programming language, it is designed to work well with ML-like languages.

The source code is available on GitHub.