LeFUNK 2026

Leipziger Workshop Funktionale Programmierung

bringing together functional programming developers, researchers, enthusiasts and beginners to listen to talks, take part in tutorials, and join in interesting conversations.

continuing the tradition of “Haskell in Leipzig”, (cf. HaL1 - 2006, HaL 2016)

News

  • August 21: registration info, abstracts of presentations
  • August 10: published list of presentations, moved registration dates

Workshop schedule and program (tentative)

Tuesday September 29:

Wednesday September 30:

  • 09 - 12: talks
  • 13 - 16: Leipzig autotool https://git.imn.htwk-leipzig.de/waldmann/autotool#leipzig-autotool user and developer meeting. Short talks and demonstrations:
    • J. Voigtländer (U Duisburg) Aufgabendiversität in Autotool
    • J. Waldmann (HTWK Leipzig) Neue Haskell-Lückentext-Aufgaben: endliche algebraische Datentypen, Striktheit
    • M. Lehmann: LTI-Schnittstelle (progress report)
    HTWK-Studenten: hier können Sie Entwurf und technische Details kennenlernen sowie die Richtung der weiteren Entwicklung. Zu dieser können Sie selbst beitragen durch Praktika, Projekte und Abschlußarbeiten.

Talks (click on title to see abstract):

  • Christian Berg. Serving Regulated APIs: An Experience Report The German energy market regulates supplier changes through EBD~594 (Entscheidungsbaum-Diagramm “E_0594_Anfrage vom LF prüfen”), a BDEW-published decision tree for identifying market locations (Marktlokationen). Our production Haskell service, MaloIdent, encodes this decision tree directly as data, one algebraic value per decision node. This experience report covers two type-level techniques that worked (an EDSL that transcribes the specification, and type-level regex constraints wired to the OpenAPI schema through deriving via) and three things types did not help with. We had to invert the spec-generation toolchain, because every generator we tried choked on errors in the published specification. One production incident came down to duplicate data that no type could have flagged: a grid operator resent four million rows we already had. And we still cannot check statically that our Haskell encoding covers the decision tree completely. We close with planned work: an index-creation DSL over Beam.
  • Olaf Klinke. Refinement types for the digital information age Digitalization is, at least to some extent, the art of exchanging information electronically that formally was exchanged on paper. For exchanging structured electronic information, we have syntactic vehicles such as XML or JSON. Within a problem domain, pinning down the set of meaningful documents (the schema) is done with the aid of machine-readable languages that express properties and invariants, for example XSD and Schematron. For the de-serialization boundary problem, that is, from document to in-memory representation, we have parsers.

    But what about the other direction? How can we make sure that data generated by our program meets all specifications? The property languages are meant to give rise to validators. But what if, instead, we used them to design a data type that has all properties and invariants baked in? Make illegal states unrepresentable, is the motto.

    We demonstrate how, starting out from a naive translation of a schema, one can construct a refinement type from a set of properties. We do this with the help of generic programming in Haskell and explain how Stone duality can play an integral part of the process.

  • Sascha Lucas. Ganeti: Introduction to a virtual machine cluster management tool Ganeti is a virtual machine cluster management tool built on top of existing virtualization technologies such KVM and other open source software. It’s main goals are: self-contained (no extras services like a database needed), aim for high-availability and reliability, low complexity, Debian as its home Linux distribution and purely open source.

    Further it has a unique concept in managing and using local storage in a high-available manner utilizing DRBD (termed hyperconverged today).

    During it’s 19 years of history Google developers introduced Haskell as a secondary language. Initially for solving an optimization problem (kind of bin packing). Later central daemons were transformed from Python to Haskell. But around 2017 Google abandoned the project. Since then the community tries to maintain the project, but the Haskell part doesn’t make it easier.

    This talk will give an introduction on how Ganeti works generally, how it manages DRBD and what challenges has to be solved with the Haskell resource planning tools.

  • Gerardo Medina-Deniz. Constraint Programming for the Algorithmic Composition of Polyphonic Music Constraint Programming offers a transparent, rule-guaranteeing alternative to generative black-box models for algorithmic music composition, yet has remained confined to academic programming environments. This work presents Constraint Composer, a browser-based, serverless system that generates polyphonic Western tonal music from declarative rules, usable without programming knowledge. Three questions guide the work: do music-theory rules map formally to constraints (RQ1), does the solver stay interactive (RQ2), and do listeners find the output plausible (RQ3)?

    From the textbook tradition of harmony and counterpoint, 75 rules across five structure-forming dimensions (pitch material, rhythm, harmony, melody/counterpoint, and form) are catalogued; twelve are formalized directly and, with indirectly subsumed rules, about half the catalogue is covered. These run in a three-step pipeline that decomposes the interdependence problem of polyphonic music into tractable subproblems: form structure, chord progression as optimization on a weighted chord graph, and per-voice pitch assignment as a finite-domain model in MiniZinc, a solver-agnostic declarative modeling language. Unlike black boxes, every generated note is traceable to declarative rules. The implementation runs in the browser via JS+WebAssembly and is released under the MIT license.

    We report on modeling music theory as constraints, interactive client-side solver performance, and a listening study with musically experienced participants, and discuss constraint-based modeling as a bridge from music theory to declarative programming.

  • Jürgen Nicklisch. Massimult: Demonstrating Massively Simultaneous Combinator Reduction Massimult is an experimental compiler and runtime for massively simultaneous combinator reduction. It asks a question at the boundary of functional-language implementation and computer architecture: can the dependency structure of a functional program serve directly as its parallel execution model? The system combines a small Hindley-Milner-typed language, LambdaM, with an explicit lowering pipeline through an untyped intermediate form into configurable combinator bases, and finally into a compact graph of fixed-size Matrima cells.

    This talk is a live, end-to-end demonstration. We parse and type-check representative LambdaM programs, inspect intermediate forms across multiple combinator bases, compile to the Matrima graph, and execute it with both reference and multithreaded C++ engines before reading the result back into a source-level value. The centerpiece is the current spine-based evaluator: independent arguments become schedulable child spines, while atomic per-cell ownership prevents duplicate work on shared subgraphs and keeps results independent of scheduling order. Golden round-trip tests and benchmark tooling make reduction counts, timing, and graph size directly observable.

    The demonstration is candid about what works and what doesn’t yet: where parallel work actually appears, which workloads fail to benefit, and which synchronization and allocation costs remain open research targets on the path toward a dedicated reduction architecture.

  • Johann Rudloff. Compiling Idris to (Efficient) Machine Code While dependent type systems are strongly established in the space of proof assistants, their use in software development is just emerging. Dependently typed programming languages allow encoding certain properties of a program inside the types of the program under development which facilitates ensuring and reasoning about correctness. We present Rapid, an LLVM-based compiler backend for the dependently-typed general purpose programming language Idris 2. Rapid is able to compile Idris programs to efficient machine code and includes an RTS with a generational, moving GC. We highlight some interesting aspects of the code generation and runtime system and discuss in more detail some of the optimising transformations. Some unique challenges inherent to compiling dependently-typed code are described, followed by an outlook towards future optimisations.
  • Justus Sagemüller. Near-WYSIWYG Typesetting of Mathematical Formulas as Haskell Source Code LaTeX has proven its flexibility by remaining the dominant format for scientific documents over multiple decades. It is in particular the near-universal standard for typesetting mathematical formulas. Yet, as a user-facing language it is in several ways problematic. The arcane unstructured syntax can make it difficult to get documents to compile as intended. And despite being Turing-complete, few people would consider it usable for serious computation purposes, requiring the use of external tools. Even in the role as a maths markup language it is suboptimal, since nontrivial formulas are verbose and hard to read in the source.

    By contrast, Haskell is well suited for structuring many kinds of information as eDSLs, in addition to being a powerful general-purpose computational tool. This talk demonstrates the TeX-my-math package, a tool extending the HaTeX bindings library with concise Unicode syntax for typesetting maths in a manner that is easily readable and matches the mathematical semantics in the Haskell AST.

There will be extra space (and coffee) available for discussion and side projects.

Participation fees

when registering before September 1

  • student: 15 EUR
  • researcher: 50 EUR
  • industry: 100 EUR (you sponsor the workshop, and get to advertise your company)

That fee covers attendance to talks, coffee breaks, performance night with simple BBQ (Grill). It does not cover: lunches (there are several options within walking distance), drinks at BBQ (you pay on-site).

students and staff of HTWK Leipzig:

  • free access to talks, but do register by email (so you get a name tag, and we can estimate attendance numbers)
  • for performance night: register and pay student fee

Registration

  • send email to the local organizer with subject “LEFUNK2026 registration” containing
    • your full name and postal address (Rechnungsanschrift)
    • your name (2 lines) and affiliation (1 line) for name tag (we will use a large font)
    • your status and expected fee (if student - attach proof)
    • your BBQ food preference (meat, vegan meat surrogate, vegetables)
    • your language preference (are you OK with talks and discussion in German)
  • you will get an invoice by email
  • you pay the invoice by bank transfer (no credit card payments, no cash)

Dates/Deadlines

  • submissions: July 12

    submit a short abstract (plaintext, approx. 200 words) and an extended abstract (PDF, up to 5 pages) via https://easychair.org/conferences/?conf=lefunk2026

    languages: for submission: English. for presentation: English or German - ask the audience.

  • author notification: August 7

  • early registration: August 31

  • workshop: September 29-30 (Tuesday, Wednesday)

Location

HTWK Leipzig, Germany

Topics

in general: functional programming in applications, teaching, research.

in particular: we welcome contributions in these areas

  • expressive types
  • interactive programming and proving
  • functional programming for music and arts

a contribution can be: a talk (30 min), a tutorial (90 min), a performance.

When in doubt, contact any member of the program committee.

Program Committee

Local Information