issues
search
uds-psl
/
coq-library-undecidability
A library of mechanised undecidability proofs in the Coq proof assistant.
Mozilla Public License 2.0
111
stars
30
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
separated L extraction framework
#227
mrhaandi
opened
1 month ago
6
reductions to `HaltLclosed` and `L_computable_closed` without the `L` framework
#226
mrhaandi
closed
1 month ago
1
dealt with some 8.20 warnings
#225
mrhaandi
closed
2 months ago
0
Adapt to Coq PR #18591: better refolding of List.app inducing "simpl never" now better respected
#224
herbelin
closed
4 months ago
0
Adapt to coq/coq#18973.
#223
rlepigre
closed
4 months ago
1
Inversion lemma for formulas
#222
Janis-Bai
opened
6 months ago
2
improve performance of TM/Single/StepTM.v
#221
mrhaandi
closed
6 months ago
0
Higher-order beta-matching
#220
mrhaandi
closed
3 months ago
0
Address Coq 8.20 warnings
#219
mrhaandi
closed
7 months ago
0
fix Arguments typo
#218
mrhaandi
closed
7 months ago
0
Adapt for coq/coq#18563
#217
andres-erbsen
closed
9 months ago
0
Adapt to metacoq primitive arrays
#216
SkySkimmer
closed
9 months ago
1
Adapt to https://github.com/coq/coq/pull/17576
#215
proux01
closed
1 year ago
1
Change license from CeCILL v2 to MPL-2.0 (more permissive) (#208)
#214
yforster
closed
1 year ago
0
Update README.md
#213
yforster
closed
1 year ago
0
Use docker in CI on 8.18
#212
yforster
closed
1 year ago
0
Use docker in CI
#211
yforster
closed
1 year ago
0
adapt to https://github.com/coq/coq/pull/18164
#210
mrhaandi
closed
1 year ago
0
As agreed, remove the reference to the former CeCILL v2 license (second step)
#209
DmxLarchey
closed
1 year ago
0
Change license from CeCILL v2 to MPL-2.0 (more permissive)
#208
DmxLarchey
closed
1 year ago
4
Consider changing to a permissive or weak copyleft license
#207
palmskog
opened
1 year ago
16
Fix coq-17129
#206
mrhaandi
closed
1 year ago
0
Add Intersection Type related problems
#205
mrhaandi
closed
1 year ago
5
faster HaltKOSBTM_to_HaltBSM.v
#204
mrhaandi
closed
1 year ago
0
Refactor L_computable_closed
#203
mrhaandi
closed
1 year ago
0
No warnings for Coq 8.18
#202
mrhaandi
closed
1 year ago
0
Fix CI
#201
yforster
closed
1 year ago
1
Fix name
#200
ghost
closed
1 year ago
1
Adapt w.r.t. coq/coq#17564.
#199
ppedrot
closed
1 year ago
4
follow up on fix for coq 17538
#198
mrhaandi
closed
1 year ago
0
Update README.md with availability of opam package
#197
yforster
closed
1 year ago
0
fix coq-17538
#196
mrhaandi
closed
1 year ago
0
Prepare for 8.17 release
#195
mrhaandi
closed
1 year ago
1
Faster ZF
#194
mrhaandi
closed
1 year ago
0
master CI fails with "/usr/bin/git ls-files" exited with code 128
#193
mrhaandi
closed
1 year ago
2
Coq 8.17 simplifications
#192
mrhaandi
closed
1 year ago
0
Adapt w.r.t. coq/coq#17304
#191
LasseBlaauwbroek
closed
1 year ago
0
Remove dependency on Synthetic.Undecidability for non-_undec files
#190
JoJoDeveloping
closed
1 year ago
1
FOL Rework
#189
JoJoDeveloping
closed
1 year ago
10
more robust TM proofs
#188
mrhaandi
closed
1 year ago
0
faster MuRec extraction
#187
mrhaandi
closed
1 year ago
0
faster SOL, TM_to_BSM
#186
mrhaandi
closed
1 year ago
0
reduced Shared usage and global side effects
#185
mrhaandi
closed
1 year ago
0
removed many 8.17 warnings
#184
mrhaandi
closed
1 year ago
0
more robust TM
#183
mrhaandi
closed
1 year ago
0
less Shared.ListAutomation
#182
mrhaandi
closed
2 years ago
0
Update README.md with instructions for manual installation
#181
yforster
closed
2 years ago
0
Proof of decidable equality for Mu-recursive algorithms
#180
DmxLarchey
closed
2 years ago
7
add computableTime instance for Nat.sqrt
#179
haansn08
closed
2 years ago
4
replace to_list_length with stdlib version
#178
haansn08
closed
2 years ago
0
Next