Repositories list

• MPCTT

  Public
  Modeling and Proving in Computational Type Theory

  Rocq Prover

  •12•122•0•0•Updated Apr 4, 2026Apr 4, 2026

• coq-library-undecidability

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

  coq

  coq

  Coq

  •

  Mozilla Public License 2.0

  •32•133•13•5•Updated Apr 2, 2026Apr 2, 2026

• coq-synthetic-computability

  Public
  Rocq Prover

  •

  MIT License

  •4•18•0•0•Updated Feb 16, 2026Feb 16, 2026

• autosubst-ocaml

  Public
  Coq

  •

  MIT License

  •12•19•4•4•Updated Nov 24, 2025Nov 24, 2025

• coq-library-fol

  Public
  Rocq Prover

  •

  MIT License

  •10•13•4•1•Updated Nov 5, 2025Nov 5, 2025

• smpl

  Public
  A Coq plugin providing an extensible tactic similar to first.

  Coq

  •

  MIT License

  •5•6•3•2•Updated Oct 29, 2025Oct 29, 2025

• L-extraction

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

  Coq

  •0•0•0•0•Updated Oct 7, 2024Oct 7, 2024

• coq-library-complexity

  Public
  Coq

  •

  Other

  •3•35•0•1•Updated Jul 14, 2023Jul 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"

  Coq

  •

  Other

  •0•3•0•0•Updated Jul 5, 2023Jul 5, 2023

• CoqTM

  Public
  Formalising Turing Machines In Coq (bachelor's thesis)

  simulatorlambda-calculuscoq-formalization+ 2

  simulatorlambda-calculuscoq-formalizationbachelor-thesisturing-machine

  Coq

  •

  MIT License

  •2•12•0•1•Updated Jul 5, 2023Jul 5, 2023

• autosubst2

  Public
  Official repository of the Autosubst 2 project.

  coqformalizationmetatheory-language

  coqformalizationmetatheory-language

  Haskell

  •

  Other

  •5•25•5•1•Updated May 8, 2023May 8, 2023

• intuitionistic-epistemic-logic

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

  Coq

  •0•4•0•0•Updated Nov 20, 2022Nov 20, 2022

• coq-synthetic-incompleteness

  Public
  Coq

  •

  Other

  •0•3•0•0•Updated Oct 18, 2022Oct 18, 2022

• coq-posts-theorem

  Public
  MIT License

  •1•2•0•0•Updated Jun 17, 2022Jun 17, 2022

• coq-undecidability-subtyping

  Public
  Coq

  •0•0•0•0•Updated Mar 28, 2022Mar 28, 2022

• metacoq_plugins

  Public
  Coq

  •2•2•0•1•Updated Mar 22, 2022Mar 22, 2022

• Prog

  Public
  OCaml

  •13•91•0•0•Updated Feb 5, 2022Feb 5, 2022

• second-order-logic

  Public
  Coq

  •0•3•0•0•Updated Jan 18, 2022Jan 18, 2022

• autosubst-metacoq

  Public
  Coq

  •0•1•0•0•Updated Oct 26, 2021Oct 26, 2021

• coq-kolmogorov-complexity

  Public
  A Formalization of Kolmogorov Complexity in Synthetic Computability Theory

  HTML

  •0•2•0•0•Updated Aug 24, 2021Aug 24, 2021

• H10-LMCS-v1.1

  Public
  HTML

  •

  Other

  •0•0•0•0•Updated May 27, 2021May 27, 2021

• tm-verification-framework

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

  HTML

  •

  Other

  •0•7•0•0•Updated Apr 22, 2021Apr 22, 2021

• constructive-and-synthetic-reducibility-in-coq

  Public
  Coq

  •0•2•0•0•Updated Mar 15, 2021Mar 15, 2021

• synthetic-reducibilility-in-coq

  Public
  0•0•0•0•Updated Mar 15, 2021Mar 15, 2021

• cook-levin

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

  HTML

  •

  Other

  •1•6•0•0•Updated Feb 3, 2021Feb 3, 2021

• ACT

  Public
  Coq

  •0•1•0•0•Updated Jan 24, 2021Jan 24, 2021

• psl-opam-repository

  Public
  Opam scripts for smpl plugin

  1•0•0•0•Updated Dec 16, 2020Dec 16, 2020

• churchs-thesis-coq

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

  HTML

  •

  MIT License

  •0•10•0•0•Updated Oct 31, 2020Oct 31, 2020

• certifying-extraction-with-time-bounds

  Public
  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

  •

  MIT License

  •0•4•0•0•Updated Oct 29, 2020Oct 29, 2020

• base-library

  Public
  Coq

  •

  MIT License

  •4•3•0•0•Updated Oct 26, 2020Oct 26, 2020