Skip to content
@epfl-systemf

SYSTEMF lab

Systems and Formalisms lab, EPFL IC, led by Prof. Clément Pit-Claudel
README.md

We're a programming languages, formal methods, and systems engineering lab at EPFL, led by Clément Pit-Claudel (@cpitclaudel). We use (and invent!) mathematical formalisms and interactive tools to explore new ways to develop computer systems. More at our official website: systemf.epfl.ch.

Pinned Loading

  1. logical-pinning logical-pinning Public

    The mechanized formalization of logical pinning, a lightweight borrowing model and proof discipline for precise reasoning about container-internal pointers.

    Rocq Prover 10

  2. librrd librrd Public

    Railroad diagram (RRD) layout library. Try it out at https://systemf.epfl.ch/etc/librrd/.

    Scala 6

  3. StrictOrderSolver StrictOrderSolver Public

    Complete solver for strict orders (transitive+irreflexive relations) for Rocq

    Rocq Prover 6

  4. verified-bootstraping verified-bootstraping Public

    Forked from myreen/imp_bootstrap

    Verified bootstrapping of an imperative compiler

    Rocq Prover 1

Repositories

Showing 10 of 25 repositories
  • camltac Public

    OCaml as a Tactic Language for the Rocq Prover

    epfl-systemf/camltac's past year of commit activity
    OCaml 20 LGPL-2.1 1 0 0 Updated Sep 16, 2026
  • ppx_rocq Public

    Syntax extensions for quoting Rocq terms in OCaml

    epfl-systemf/ppx_rocq's past year of commit activity
    OCaml 5 LGPL-2.1 1 0 0 Updated Sep 16, 2026
  • lorikeet Public

    Flexible code rewriting tool for Scala based on Scalafix

    epfl-systemf/lorikeet's past year of commit activity
    Scala 2 Apache-2.0 0 0 0 Updated Sep 16, 2026
  • verified-bootstraping Public Forked from myreen/imp_bootstrap

    Verified bootstrapping of an imperative compiler

    epfl-systemf/verified-bootstraping's past year of commit activity
    Rocq Prover 1 2 0 0 Updated Sep 10, 2026
  • mltac2 Public

    Ltac2 APIs for OCaml

    epfl-systemf/mltac2's past year of commit activity
    OCaml 0 LGPL-2.1 1 0 0 Updated Sep 8, 2026
  • poll Public

    Proof-oriented layout language

    epfl-systemf/poll's past year of commit activity
    Rocq Prover 0 0 0 0 Updated Aug 20, 2026
  • sepviz Public

    Automatic rendering of separation-logic diagrams for Iris and CFML in Alectryon and VSRocq

    epfl-systemf/sepviz's past year of commit activity
    TypeScript 6 0 1 0 Updated Jul 27, 2026
  • librrd Public

    Railroad diagram (RRD) layout library. Try it out at https://systemf.epfl.ch/etc/librrd/.

    epfl-systemf/librrd's past year of commit activity
    Scala 6 MIT 0 1 0 Updated Jun 29, 2026
  • koika Public Forked from mit-plv/koika

    A core language for rule-based hardware design 🦑

    epfl-systemf/koika's past year of commit activity
    Rocq Prover 0 LGPL-2.1 21 0 0 Updated Jun 28, 2026
  • dvar-track Public

    An Emacs Lisp dynamic variable reference tracker

    epfl-systemf/dvar-track's past year of commit activity
    C 2 0 0 0 Updated Jun 9, 2026
View all repositories

Top languages

Loading…

Most used topics

Loading…