https://github.com/uds-psl/coq-library-undecidability

sort by:
Revision Author Date Message Commit Date
32fa1f0 Cleanup coqdoc and _CoqProject (#97) 24 November 2020, 12:45:44 UTC
8c1f0bd Merge pull request #96 from yforster/unified_fol_compiled Unified FOL syntax without universe inconsistency 23 November 2020, 17:40:42 UTC
43d62c5 Local Notation vec := Vector.t 23 November 2020, 13:47:47 UTC
1b4b470 Fix vec definition to circumvent universe inconsistency 23 November 2020, 13:39:45 UTC
96d36da Fix From Undecidability in ProgrammingTools.v 23 November 2020, 12:52:05 UTC
c795739 Merge branch 'unified_fol' into coq-8.12 23 November 2020, 09:21:04 UTC
de12c77 restart CI 20 November 2020, 18:51:28 UTC
bd2dfc4 Merge pull request #94 from mrhaandi/opam_info added opam update and opam list --installed to CI 20 November 2020, 17:52:05 UTC
ff50c74 import statements and commments 20 November 2020, 17:02:16 UTC
d30e029 Merge pull request #72 from fakusb/Compiler_L_TM Compiler from L to TMs 20 November 2020, 16:30:28 UTC
8030f89 removed eval $(opam env) 20 November 2020, 16:09:57 UTC
45fbc21 Merge branch 'opam_info' of https://github.com/mrhaandi/coq-library-undecidability into opam_info 20 November 2020, 16:08:48 UTC
3612439 reset eval $(opam env) 20 November 2020, 16:07:40 UTC
c4c1acc Merge pull request #2 from yforster/bettercompiler Finished compiler for natural numbers 20 November 2020, 16:01:03 UTC
bbc3a91 synthesised step counts for eval 20 November 2020, 16:00:10 UTC
483b8d0 little fixes 20 November 2020, 13:21:51 UTC
10ef6c0 added eval $(opam env) 20 November 2020, 13:20:56 UTC
d9d61cc Merge branch 'coq-8.12' into unified_fol 20 November 2020, 13:17:39 UTC
0050d59 cleanup 20 November 2020, 12:29:56 UTC
8603907 enumerability proof 20 November 2020, 12:26:04 UTC
a033e5b added opam upgrade 20 November 2020, 12:25:16 UTC
78e1a6b enumerability proof 20 November 2020, 12:11:35 UTC
41cc25d added opam update and opam list --installed to CI 20 November 2020, 12:10:28 UTC
39d7fa3 Merge pull request #93 from mrhaandi/cleaner_synthetic documented (via comments) synthetic definitions 20 November 2020, 11:16:04 UTC
2f98b87 Delete uncompiled files (#90) * delete uncompiled files * rename files, fix compilation 20 November 2020, 10:44:22 UTC
e8a9f63 documented (via comments) synthetic definitions separated non-informative and informative definitions encapsulated non-essential notations 20 November 2020, 10:19:36 UTC
6eadcf3 finished L to TM compiler for nat 20 November 2020, 10:07:34 UTC
d6f1ca7 facts file 20 November 2020, 09:21:11 UTC
88373ec two admits remaining 20 November 2020, 09:21:03 UTC
ebb4537 proved discreteness 19 November 2020, 17:42:49 UTC
f188292 only discreteness left 19 November 2020, 15:17:29 UTC
fa93aa6 compiling version, some admits 19 November 2020, 13:27:56 UTC
84c9529 1 + k + n 19 November 2020, 12:20:02 UTC
6fdc1a3 Improved README file (#84) 19 November 2020, 11:19:50 UTC
ff3fd69 ported first reduction file 19 November 2020, 11:11:15 UTC
47d36c1 problem summary 19 November 2020, 09:39:04 UTC
db71be4 Merge pull request #86 from DmxLarchey/fixpoints change Fixpoint to Definition ... := fix to avoid a warning 19 November 2020, 09:21:41 UTC
4e80cc3 Merge pull request #89 from yforster/TSR_undec TSR_undec 19 November 2020, 09:11:44 UTC
bec2f56 solved conflicting format directive for the vector/environment component access notation 19 November 2020, 08:34:08 UTC
94d4d87 TSR_undec 19 November 2020, 07:30:57 UTC
b6c2f92 fixed compilation and added final lemma for tyhe bool-fun-compiler 18 November 2020, 18:56:50 UTC
e73635a working on Kripke soundness 18 November 2020, 18:11:03 UTC
b6a8b91 fixed bool_bool names due to grepping 18 November 2020, 17:30:01 UTC
4c543ad replaced syntax, tarski and deduction 18 November 2020, 17:28:42 UTC
c034be6 renamed encTM to encBoolsTM 18 November 2020, 17:20:26 UTC
bc91433 Merge pull request #88 from yforster/PCSnf_undec.v Add PCSnf_undec file 18 November 2020, 17:16:59 UTC
a54c65e renamed computability notion for bool-list-functions 18 November 2020, 16:54:41 UTC
5f408d5 Merge branch 'fakusb-Compiler-L-TM' into Compiler_L_TM 18 November 2020, 16:41:42 UTC
5080132 Split L list functions for more compilation parallelism. 18 November 2020, 16:02:44 UTC
24c49a8 Add PCSnf_undec file 18 November 2020, 15:54:30 UTC
a079dce finish proof 18 November 2020, 15:43:24 UTC
fcab214 finish proof 18 November 2020, 15:43:02 UTC
a59721f wip factoring L/Datatypes/List 18 November 2020, 11:53:01 UTC
4bf71c7 make compile 18 November 2020, 11:48:52 UTC
331904e progress 18 November 2020, 11:46:02 UTC
540a54e cleanup 18 November 2020, 10:04:40 UTC
31eb751 Merge pull request #87 from fakusb/speedup-HOU-firstorder Cleanup HOU/firstorder.v proofs 18 November 2020, 09:37:31 UTC
bb3c397 Optimized HOU/firstorder.v proofs 18 November 2020, 08:09:03 UTC
79891b9 Optimized HOU/firstorder.v proofs 18 November 2020, 00:01:31 UTC
f777be1 Merge remote-tracking branch 'origin/coq-8.12' into Compiler_L_TM 17 November 2020, 22:47:15 UTC
b3c0f9a Finished equivalence of TM-function-computability and closed L-computability 17 November 2020, 22:35:33 UTC
7a6c59c change Fixpoint to Definition ... := fix to avoid a warning 17 November 2020, 22:21:37 UTC
18a7baf Merge pull request #85 from mrhaandi/sysF_cleanup cleaned up System F and Semi-unification reductions 17 November 2020, 19:50:13 UTC
d6aff9e Merge pull request #83 from yforster/PCSnf Post canonical systems in normal form and Thue systems 17 November 2020, 17:39:33 UTC
b1eb6ae cleaned up System F reductions cleaned up Semi-unifications reductions 17 November 2020, 15:42:34 UTC
0c86298 fix compilation 17 November 2020, 12:37:26 UTC
1e34fc5 Merge branch 'coq-8.12' into PCSnf 17 November 2020, 12:29:17 UTC
debf8ec Merge pull request #82 from yforster/cleanupFOL Cleanup regarding FOL 17 November 2020, 12:28:57 UTC
a92429e get rid of Shared.Prelims 17 November 2020, 12:20:38 UTC
9c54b3d fix workflow 17 November 2020, 12:12:13 UTC
7c60554 same workflow as repo 17 November 2020, 12:11:38 UTC
6cbe603 simplifications 17 November 2020, 12:10:25 UTC
163d85d Add Thue systems 17 November 2020, 12:10:22 UTC
24c91fc Reduction from SR to PCSnf 17 November 2020, 12:09:52 UTC
1f3af0e Add PCSnf file 17 November 2020, 12:09:52 UTC
44d5a60 use opam exec 17 November 2020, 12:09:52 UTC
3b4edc1 eval opam env 17 November 2020, 12:09:52 UTC
90eb3ef use flambda 17 November 2020, 12:09:52 UTC
7cdb5a6 move workflos dir 17 November 2020, 12:08:23 UTC
3025899 Add config for GitHub Actions 17 November 2020, 12:07:22 UTC
b5b14aa Added decodable encodings 17 November 2020, 11:46:14 UTC
427d668 moved unneeded definition out of Compiler-Spec 17 November 2020, 11:32:17 UTC
bdecda3 fix notation warnings 17 November 2020, 11:22:12 UTC
ae671b0 termination of boollist-L-to_m-compiler 17 November 2020, 11:01:10 UTC
dbb880a FOL_undec file 17 November 2020, 10:44:54 UTC
86e1b47 move problems more, introduce FOL problem names 17 November 2020, 10:37:14 UTC
72e7b93 move FOLFS files 17 November 2020, 09:57:59 UTC
b821998 Rename Utils to Util 17 November 2020, 09:51:01 UTC
6968fbf Remove LICENSE and Readme from FOL 17 November 2020, 09:47:23 UTC
8cb97da Remove FOL 17 November 2020, 09:44:00 UTC
29f18f7 Remove redundant files 17 November 2020, 08:29:21 UTC
eade0b0 Merge pull request #80 from yforster/NoSharedPrelim Remove Shared.Prelim 17 November 2020, 08:08:03 UTC
c155fbf Remove Shared.Prelim 16 November 2020, 13:13:31 UTC
666aa96 termination of unfold heap 16 November 2020, 09:28:39 UTC
aa1676b Merge pull request #79 from fakusb/IncludePslBase Removed external dependency on PslBase 16 November 2020, 07:48:19 UTC
bf61860 commit to run ci 15 November 2020, 12:30:43 UTC
1b1ec43 Merge pull request #74 from DmxLarchey/imsell Undecidability for IMSELL with 3 modalities 15 November 2020, 11:42:01 UTC
4b82c39 termination of UnfoldHeap-step-tm done 14 November 2020, 20:30:34 UTC
ecbaf50 Merge branch 'IncludePslBase' into Compiler_L_TM 14 November 2020, 20:30:05 UTC
3833971 fixed wrong "Contributors" listing 14 November 2020, 19:19:50 UTC
back to top