uds-psl/time-invariance-thesis-for-L uds-psl/time-invariance-thesis-for-L

  • Stars
    star
    3
  • Rank 3,963,521 (Top 79 %)
  • Language Coq
  • License
    Other
  • Created almost 4 years ago
  • Updated over 1 year ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
uds-psl/time-invariance-thesis-for-L
github

uds-psl

Reviews

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

Repository Details

Coq development of the paper "A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value 位-Calculus"

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鈥檚 thesis and related axioms in Coq鈥檚 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

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
19

metacoq_plugins

Coq
2
star
20

second-order-logic

Coq
2
star
21

coq-posts-theorem

2
star
22

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
23

constructive-and-synthetic-reducibility-in-coq

Coq
2
star
24

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
25

ill-undecidability

Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Coq
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