33 search results for "author:"Yannick Forster""

Showing 1 - 33
  1. coq-certicoq

    No documentation

    A Verified Compiler for Gallina, Written in Gallina
    Andrew Appel Yannick Forster Anvay Grover Joomy Korkut John Li et al.
    0.9+8.19
    MIT
    Used by 0 other packages
    04 Jun 2024
  2. coq-library-complexity

    No documentation

    A Coq Library of Complexity Theory
    Fabian Kunze Lennard Gäher Maximilian Wuttke Yannick Forster Stefan Haan
    1.0+8.16
    CECILL-2.1
    Used by 0 other packages
    09 Nov 2022
  3. coq-library-fol

    No documentation

    A Coq Library for First-Order Logic
    Dominik Kirst Johannes Hostert Andrej Dudenhefner Yannick Forster Marc Hermes et al.
    1.0+8.20
    MIT
    Used by 0 other packages
    06 Feb 2025
  4. coq-library-undecidability

    No documentation

    A Coq Library of Undecidability Proofs
    Yannick Forster Dominique Larchey-Wendling Andrej Dudenhefner Edith Heiter Marc Hermes et al.
    1.1.2+8.20
    MPL-2.0
    Used by 1 other packages
    30 Sep 2024
  5. coq-metacoq

    No documentation

    A meta-programming framework for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 0 other packages
    03 Apr 2025
  6. coq-metacoq-common

    No documentation

    The common library of Template Coq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 4 other packages
    03 Apr 2025
  7. coq-metacoq-erasure

    No documentation

    Implementation and verification of an erasure procedure for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 5 other packages
    03 Apr 2025
  8. coq-metacoq-erasure-plugin

    No documentation

    Implementation and verification of an erasure procedure for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 2 other packages
    03 Apr 2025
  9. coq-metacoq-pcuic

    No documentation

    A type system equivalent to Coq's and its metatheory
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 6 other packages
    03 Apr 2025
  10. coq-metacoq-quotation

    No documentation

    Gallina quotation functions for Template Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 1 other packages
    03 Apr 2025
  11. coq-metacoq-safechecker

    No documentation

    Implementation and verification of safe conversion and typechecking algorithms for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 4 other packages
    03 Apr 2025
  12. coq-metacoq-safechecker-plugin

    No documentation

    Implementation and verification of an erasure procedure for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 1 other packages
    03 Apr 2025
  13. coq-metacoq-template

    No documentation

    A quoting and unquoting library for Coq in Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 8 other packages
    03 Apr 2025
  14. coq-metacoq-template-pcuic

    No documentation

    Translations between Template Coq and PCUIC and proofs of correctness
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 6 other packages
    03 Apr 2025
  15. coq-metacoq-translations

    No documentation

    Translations built on top of MetaCoq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 1 other packages
    03 Apr 2025
  16. coq-metacoq-utils

    No documentation

    The utility library of Template Coq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 3 other packages
    03 Apr 2025
  17. coq-smpl

    No documentation

    Smpl: An Extensible Tactic for Coq
    Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de> Yannick Forster <forster@cs.uni-saarland.de> Fabian Kunze <fabian.kunze@cs.uni-saarland.de> Kenji Maillard <kenji.maillard@inria.fr>
    8.20
    MIT
    Used by 1 other packages
    20 Oct 2024
  18. coq-verified-extraction

    No documentation

    A Verified Extraction from Gallina to OCaml, written in Gallina
    Yannick Forster Matthieu Sozeau Nicolas Tabareau
    0.9.2+8.19
    MIT
    Used by 0 other packages
    23 Jul 2024
  19. rocq-certirocq

    No documentation

    A Verified Compiler for Gallina, Written in Gallina
    Andrew Appel Yannick Forster Anvay Grover Joomy Korkut John Li et al.
    0.9.1+9.1
    MIT
    Used by 0 other packages
    18 Mar 2026
  20. rocq-metarocq

    No documentation

    A meta-programming framework for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 0 other packages
    12 Mar 2026
  21. rocq-metarocq-common

    No documentation

    The common library of Template Rocq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  22. rocq-metarocq-erasure

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  23. rocq-metarocq-erasure-plugin

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  24. rocq-metarocq-pcuic

    No documentation

    A type system equivalent to Rocq's and its metatheory
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  25. rocq-metarocq-quotation

    No documentation

    Gallina quotation functions for Template Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 1 other packages
    12 Mar 2026
  26. rocq-metarocq-safechecker

    No documentation

    Implementation and verification of safe conversion and typechecking algorithms for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  27. rocq-metarocq-safechecker-plugin

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 2 other packages
    12 Mar 2026
  28. rocq-metarocq-template

    No documentation

    A quoting and unquoting library for Rocq in Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  29. rocq-metarocq-template-pcuic

    No documentation

    Translations between Template Rocq and PCUIC and proofs of correctness
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 5 other packages
    12 Mar 2026
  30. rocq-metarocq-translations

    No documentation

    Translations built on top of MetaRocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 1 other packages
    12 Mar 2026
  31. rocq-metarocq-utils

    No documentation

    The utility library of Template Rocq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  32. rocq-smpl

    No documentation

    Smpl: An Extensible Tactic for Coq
    Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de> Yannick Forster <forster@cs.uni-saarland.de> Fabian Kunze <fabian.kunze@cs.uni-saarland.de> Kenji Maillard <kenji.maillard@inria.fr>
    9.0
    MIT
    Used by 0 other packages
    05 Sep 2025
  33. rocq-verified-extraction

    No documentation

    Verified extraction from Rocq to OCaml
    keyword:extraction category:Miscellaneous/Rocq Extensions logpath:VerifiedExtraction
    Yannick Forster Matthieu Sozeau Nicolas Tabareau
    1.0.0+9.1
    MIT
    Used by 0 other packages
    13 Mar 2026