Skip to content

@epfl-systemf SYSTEMF lab

All

    Repositories list

    25 repositories

    • poll

      Public
      Proof-oriented layout language
      Rocq Prover
      •0•0•0•0•Updated Aug 20, 2026Aug 20, 2026

    • camltac

      Public
      OCaml as a Tactic Language for the Rocq Prover
      ocamlltac2rocq
      ocamlltac2rocqrocq-prover
      OCaml
      •
      GNU Lesser General Public License v2.1
      •1•20•0•0•Updated Aug 17, 2026Aug 17, 2026

    • ppx_rocq

      Public
      Syntax extensions for quoting Rocq terms in OCaml
      ocamlppxppx-rewriter
      ocamlppxppx-rewriterrocqrocq-prover
      OCaml
      •
      GNU Lesser General Public License v2.1
      •1•5•0•0•Updated Aug 17, 2026Aug 17, 2026

    • lorikeet

      Public
      Flexible code rewriting tool for Scala based on Scalafix
      scalarewriting
      scalarewriting
      Scala
      •
      Apache License 2.0
      •0•2•0•0•Updated Aug 5, 2026Aug 5, 2026

    • sepviz

      Public
      Automatic rendering of separation-logic diagrams for Iris and CFML in Alectryon and VSRocq
      automationdiagramseparation-logic
      automationdiagramseparation-logicheap-memoryrocq
      TypeScript
      •
      Other
      •0•6•1•0•Updated Jul 27, 2026Jul 27, 2026

    • mltac2

      Public
      Ltac2 APIs for OCaml
      OCaml
      •
      GNU Lesser General Public License v2.1
      •1•0•0•0•Updated Jul 25, 2026Jul 25, 2026

    • librrd

      Public
      Railroad diagram (RRD) layout library. Try it out at https://systemf.epfl.ch/etc/librrd/.
      Scala
      •
      MIT License
      •0•6•1•0•Updated Jun 29, 2026Jun 29, 2026

    • koika

      Public
      A core language for rule-based hardware design 🦑
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •21•0•0•0•Updated Jun 28, 2026Jun 28, 2026

    • dvar-track

      Public
      An Emacs Lisp dynamic variable reference tracker
      C
      •0•2•0•0•Updated Jun 9, 2026Jun 9, 2026

    • StrictOrderSolver

      Public
      Complete solver for strict orders (transitive+irreflexive relations) for Rocq
      solverltac2rocq
      solverltac2rocqstrict-order
      Rocq Prover
      •
      MIT License
      •0•6•0•0•Updated May 13, 2026May 13, 2026

    • 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
      •0•10•0•0•Updated May 13, 2026May 13, 2026

    • sepviz-vsrocq

      Public
      OCaml
      •
      MIT License
      •0•0•0•0•Updated May 7, 2026May 7, 2026

    • sepviz-software-foundations-slf

      Public
      Rocq Prover
      •
      MIT License
      •0•0•0•0•Updated May 7, 2026May 7, 2026

    • sepviz-iris-tutorial

      Public
      Rocq Prover
      •
      MIT License
      •0•0•0•0•Updated Apr 28, 2026Apr 28, 2026

    • sepviz-cfml-examples

      Public
      Rocq Prover
      •0•0•0•0•Updated Apr 28, 2026Apr 28, 2026

    • sepviz-software-foundations-vc

      Public
      HTML
      •
      MIT License
      •0•0•0•0•Updated Apr 27, 2026Apr 27, 2026

    • .github

      Public
      0•0•0•0•Updated Apr 16, 2026Apr 16, 2026

    • verified-bootstraping

      Public
      Verified bootstrapping of an imperative compiler
      Rocq Prover
      •2•1•0•0•Updated Feb 11, 2026Feb 11, 2026

    • scala3

      Public
      The Scala 3 compiler, also known as Dotty.
      Scala
      •
      Apache License 2.0
      •1.2k•0•0•1•Updated Jan 7, 2026Jan 7, 2026

    • coq

      Public
      Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an en…
      OCaml
      •
      GNU Lesser General Public License v2.1
      •755•1•0•0•Updated Nov 24, 2025Nov 24, 2025

    • v8-regex-jit

      Public
      Adding a linear regex engine with native compilation
      C++
      •
      Other
      •4.3k•1•0•0•Updated Jul 18, 2025Jul 18, 2025

    • grattlesnake-lang

      Public
      Scala
      •
      MIT License
      •2•1•0•0•Updated Jan 30, 2025Jan 30, 2025

    • rvm-compiler-project

      Public
      TeX
      •2•1•0•0•Updated Oct 3, 2024Oct 3, 2024

    • optitrust

      Public
      OptiTrust (w/ RVM case study)
      OCaml
      •
      MIT License
      •7•2•0•0•Updated Sep 18, 2024Sep 18, 2024

    • JumboTrace

      Public
      Java
      •
      MIT License
      •0•1•0•0•Updated Jan 5, 2024Jan 5, 2024
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.