uds-psl/metacoq-nested-induction

Stars
3
Rank 3,963,521 (Top 79 %)
Language Coq
Created over 4 years ago
Updated about 4 years ago

uds-psl/metacoq-nested-induction

uds-psl

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

A plugin for induction principles of nested inductive types using MetaCoq

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)

churchs-thesis-coq

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

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

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