Programming Systems Lab, Saarland University (@uds-psl)
Guthub

uds-psl

Twitter logo Share LinkedIn logo Share Facebook logo Share
  • Stars
    star
    400
  • Global Org. Rank 27,349 (Top 9 %)
  • Registered over 7 years ago
  • Most used languages
    Coq     66.7 %
    HTML
         23.3 %
    TeX
         3.3 %
    Haskell
         3.3 %
    OCaml
         3.3 %
  • Location 🇩🇪 Germany
  • Country Total Rank 4,811
  • Country Ranking
    Coq     2
    OCaml
         8
    Haskell
         143
    HTML
         718
    TeX
         1,243

Top repositories

1

coq-library-undecidability

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

Prog

OCaml
79
star
3

MPCTT

Modeling and Proving in Computational Type Theory
Coq
75
star
4

coq-library-complexity

Coq
26
star
5

autosubst2

Official repository of the Autosubst 2 project.
Haskell
15
star
6

autosubst-ocaml

Coq
12
star
7

CoqTM

Formalising Turing Machines In Coq (bachelor's thesis)
Coq
11
star
8

churchs-thesis-coq

Mechanisation of the paper "Church’s thesis and related axioms in Coq’s type theory"
HTML
9
star
9

coq-synthetic-computability

Coq
6
star
10

coq-a-la-carte-cpp20

HTML
6
star
11

tm-verification-framework

Static version of https://github.com/uds-psl/coq-library-undecidability for paper "Verified Programming of Turing Machines in Coq"
HTML
6
star
12

cook-levin

Static copy of https://github.com/uds-psl/coq-library-complexity for paper 'Mechanising Complexity Theory: The Cook-Levin Theorem in Coq'
HTML
5
star
13

fol-completeness-theorems

Source code accompanying the Bachelor's thesis of Dominik Wehr.
Coq
4
star
14

coq-library-fol

Coq
4
star
15

base-library

Coq
3
star
16

metacoq-nested-induction

A plugin for induction principles of nested inductive types using MetaCoq
Coq
3
star
17

intuitionistic-epistemic-logic

Coq development accompanying the LFCS'22 paper "Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic"
Coq
3
star
18

time-invariance-thesis-for-L

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

certifying-extraction-with-time-bounds

This repository contains the Coq formalisation of the ITP 2019 paper "A certifying extraction with time bounds from Coq to call-by-value λ-calculus".
Coq
3
star
20

metacoq_plugins

Coq
2
star
21

second-order-logic

Coq
2
star
22

coq-posts-theorem

2
star
23

cbv-lambda-calculus-reasonable

The formalized part of the POPL 2020 Paper "The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space"
Coq
2
star
24

constructive-and-synthetic-reducibility-in-coq

Coq
2
star
25

ps-category-theory-seminar-17

Exercise sheets for the Category theory seminar at the Programming Systems Lab, Saarland University, summer term 2017. https://courses.ps.uni-saarland.de/ct_ss17/
TeX
2
star
26

ill-undecidability

Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Coq
2
star
27

ACT

Coq
1
star
28

coq-synthetic-incompleteness

Coq
1
star
29

H10

Static version of https://github.com/uds-psl/coq-library-undecidability for paper "Hilbert's tenth problem in Coq"
HTML
1
star
30

ba-gaeher

Bachelor project of Lennard Gäher.
HTML
1
star
31

coq-kolmogorov-complexity

A Formalization of Kolmogorov Complexity in Synthetic Computability Theory
HTML
1
star