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 128 12

  2. Prog Prog Public

    OCaml 95 13

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

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

    Rocq Prover 144 38

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

    Coq 37 4

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

    Rocq Prover 20 5

  6. autosubst2 autosubst2 Public

    Official repository of the Autosubst 2 project.

    Haskell 30 5

Repositories

Showing 10 of 44 repositories
  • coq-library-fol Public
    uds-psl/coq-library-fol's past year of commit activity
    Rocq Prover 16 MIT 10 4 2 Updated Sep 23, 2026
  • coq-synthetic-computability Public
    uds-psl/coq-synthetic-computability's past year of commit activity
    Rocq Prover 20 MIT 5 0 0 Updated Sep 9, 2026
  • MPCTT Public

    Modeling and Proving in Computational Type Theory

    uds-psl/MPCTT's past year of commit activity
    Rocq Prover 128 12 0 0 Updated Aug 11, 2026
  • autosubst-ocaml Public
    uds-psl/autosubst-ocaml's past year of commit activity
    Coq 22 MIT 14 5 4 Updated Jul 2, 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 144 MPL-2.0 38 13 6 Updated Jun 24, 2026
  • 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 6 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 37 4 0 2 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

Most used topics

Loading…