Skip to content

@Yann-Leray Yann Leray

Change the repository type filter

All

    Repositories list

    23 repositories

    • acc-in-sprop

      Public
      Rocq Prover
      •0•0•0•0•Updated Mar 29, 2026Mar 29, 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
      •720•0•0•1•Updated Mar 24, 2026Mar 24, 2026

    • vsrocq

      Public
      Visual Studio Code extension for Coq
      OCaml
      •
      MIT License
      •100•0•0•0•Updated Mar 24, 2026Mar 24, 2026

    • rewriter

      Public
      Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
      Rocq Prover
      •
      Other
      •24•0•0•0•Updated Feb 17, 2026Feb 17, 2026

    • rocq-lean-import

      Public
      OCaml
      •
      GNU Lesser General Public License v2.1
      •12•0•0•0•Updated Feb 11, 2026Feb 11, 2026

    • metacoq

      Public
      Metaprogramming in Coq
      Coq
      •
      MIT License
      •96•0•0•0•Updated Feb 6, 2026Feb 6, 2026

    • ocaml

      Public
      The core OCaml system: compilers, runtime system, base libraries
      OCaml
      •
      Other
      •1.2k•0•0•0•Updated Feb 2, 2026Feb 2, 2026

    • hierarchy-builder

      Public
      High level commands to declare a hierarchy based on packed classes
      Rocq Prover
      •
      MIT License
      •28•0•0•0•Updated Jan 27, 2026Jan 27, 2026

    • UniMath

      Public
      This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
      Rocq Prover
      •
      Other
      •187•0•0•0•Updated Jan 26, 2026Jan 26, 2026

    • yann-leray.github.io

      Public
      CSS
      •
      MIT License
      •0•0•0•0•Updated Jan 8, 2026Jan 8, 2026

    • coq-tactician

      Public
      A Seamless, Interactive Tactic Learner and Prover for Coq
      OCaml
      •
      MIT License
      •25•0•0•0•Updated Oct 7, 2025Oct 7, 2025

    • reduction-effects

      Public
      A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
      Makefile
      •
      Mozilla Public License 2.0
      •7•0•0•0•Updated Oct 2, 2025Oct 2, 2025

    • coq-elpi

      Public
      Coq plugin embedding elpi
      OCaml
      •
      GNU Lesser General Public License v2.1
      •70•0•0•0•Updated Oct 1, 2025Oct 1, 2025

    • paramcoq

      Public
      Old Coq plugin for parametricity [maintainer=@ppedrot]
      Coq
      •
      Other
      •29•0•0•0•Updated Oct 1, 2025Oct 1, 2025

    • Coq-Equations

      Public
      A function definition package for Coq
      Coq
      •
      GNU Lesser General Public License v2.1
      •55•0•0•0•Updated Oct 1, 2025Oct 1, 2025

    • rocq-stdlib

      Public
      Stdlib for the Rocq Prover
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •31•0•0•0•Updated Sep 22, 2025Sep 22, 2025

    • coq-lsp

      Public
      Visual Studio Code Extension and Language Server Protocol for Coq
      OCaml
      •
      GNU Lesser General Public License v2.1
      •52•0•0•0•Updated Jun 17, 2025Jun 17, 2025

    • QuickChick

      Public
      Randomized Property-Based Testing Plugin for Coq
      Coq
      •
      Other
      •50•0•0•0•Updated Mar 31, 2025Mar 31, 2025

    • vscoq

      Public
      Visual Studio Code extension for Coq
      OCaml
      •
      MIT License
      •100•0•0•0•Updated Jan 10, 2025Jan 10, 2025

    • coq-serapi

      Public
      Coq Protocol Playground with Se(xp)rialization of Internal Structures.
      OCaml
      •
      Other
      •41•0•0•0•Updated Feb 5, 2024Feb 5, 2024

    • Mtac2

      Public
      Coq
      •
      Other
      •25•0•0•0•Updated Feb 5, 2024Feb 5, 2024

    • coqhammer

      Public
      CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
      OCaml
      •
      Other
      •36•0•0•0•Updated Feb 5, 2024Feb 5, 2024

    • coq-dpdgraph

      Public
      Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
      Coq
      •
      GNU Lesser General Public License v2.1
      •33•0•0•0•Updated Feb 5, 2024Feb 5, 2024
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.