Skip to content
@uds-psl

Programming Systems Lab, Saarland University

Pinned Loading

  1. MPCTT MPCTT Public

    Modeling and Proving in Computational Type Theory

    Rocq Prover 122 12

  2. Prog Prog Public

    OCaml 93 13

  3. coq-library-undecidability coq-library-undecidability Public

    A library of mechanised undecidability proofs in the Coq proof assistant.

    Rocq Prover 135 32

  4. coq-library-complexity coq-library-complexity Public

    Coq 35 3

  5. coq-synthetic-computability coq-synthetic-computability Public

    Rocq Prover 18 5

  6. autosubst2 autosubst2 Public

    Official repository of the Autosubst 2 project.

    Haskell 25 5

Repositories

Showing 10 of 44 repositories
  • MPCTT Public

    Modeling and Proving in Computational Type Theory

    uds-psl/MPCTT’s past year of commit activity
    Rocq Prover 122 12 0 0 Updated Apr 21, 2026
  • coq-library-undecidability Public

    A library of mechanised undecidability proofs in the Coq proof assistant.

    uds-psl/coq-library-undecidability’s past year of commit activity
    Rocq Prover 135 MPL-2.0 32 13 4 Updated Apr 14, 2026
  • coq-synthetic-computability Public
    uds-psl/coq-synthetic-computability’s past year of commit activity
    Rocq Prover 18 MIT 5 0 0 Updated Feb 16, 2026
  • autosubst-ocaml Public
    uds-psl/autosubst-ocaml’s past year of commit activity
    Coq 19 MIT 12 5 4 Updated Nov 24, 2025
  • coq-library-fol Public
    uds-psl/coq-library-fol’s past year of commit activity
    Rocq Prover 13 MIT 10 4 1 Updated Nov 5, 2025
  • smpl Public Forked from sigurdschneider/smpl

    A Coq plugin providing an extensible tactic similar to first.

    uds-psl/smpl’s past year of commit activity
    Coq 6 MIT 5 3 2 Updated Oct 29, 2025
  • L-extraction Public

    Extraction framework into weak call-by-value lambda-calculus.

    uds-psl/L-extraction’s past year of commit activity
    Coq 0 0 0 0 Updated Oct 7, 2024
  • coq-library-complexity Public
    uds-psl/coq-library-complexity’s past year of commit activity
    Coq 35 3 0 1 Updated Jul 14, 2023
  • time-invariance-thesis-for-L Public

    Coq development of the paper "A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus"

    uds-psl/time-invariance-thesis-for-L’s past year of commit activity
    Coq 3 0 0 0 Updated Jul 5, 2023
  • CoqTM Public

    Formalising Turing Machines In Coq (bachelor's thesis)

    uds-psl/CoqTM’s past year of commit activity
    Coq 12 MIT 2 0 1 Updated Jul 5, 2023
View all repositories

Top languages

Loading…

Most used topics

Loading…