uds-psl/churchs-thesis-coq

Stars
9
Rank 1,939,727 (Top 39 %)
Language
HTML
License
MIT License
Created over 4 years ago
Updated about 4 years ago

uds-psl/churchs-thesis-coq

uds-psl

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

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

coq-library-undecidability

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

Prog

MPCTT

Modeling and Proving in Computational Type Theory

coq-library-complexity

autosubst2

Official repository of the Autosubst 2 project.

autosubst-ocaml

CoqTM

Formalising Turing Machines In Coq (bachelor's thesis)

coq-synthetic-computability

coq-a-la-carte-cpp20

tm-verification-framework

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

cook-levin

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

fol-completeness-theorems

Source code accompanying the Bachelor's thesis of Dominik Wehr.

coq-library-fol

base-library

metacoq-nested-induction

A plugin for induction principles of nested inductive types using MetaCoq

intuitionistic-epistemic-logic

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

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"

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".

metacoq_plugins

second-order-logic

coq-posts-theorem

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"

constructive-and-synthetic-reducibility-in-coq

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/

ill-undecidability

Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines

ACT

coq-synthetic-incompleteness

H10

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

ba-gaeher

Bachelor project of Lennard Gäher.

coq-kolmogorov-complexity

A Formalization of Kolmogorov Complexity in Synthetic Computability Theory