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