uds-psl/ill-undecidability uds-psl/ill-undecidability

  • Stars
    star
    2
  • Language Coq
  • License
    Other
  • Created about 6 years ago
  • Updated about 6 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
uds-psl/ill-undecidability
github

uds-psl

Reviews

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

Repository Details

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

More 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

ACT

Coq
1
star
27

coq-synthetic-incompleteness

Coq
1
star
28

H10

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

ba-gaeher

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

coq-kolmogorov-complexity

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