| f7e9adc | Dominique Larchey-Wendling | 12 December 2019, 12:13:34 UTC | some cleanup in dio_logic and dio_bounded mostly better comments | 12 December 2019, 12:13:34 UTC |
| eba1051 | Dominique Larchey-Wendling | 11 December 2019, 12:32:56 UTC | tracking duplications in encodings | 11 December 2019, 12:32:56 UTC |
| 8732580 | Dominique Larchey-Wendling | 11 December 2019, 12:18:13 UTC | starting to make optimisation with a less dramatic effect | 11 December 2019, 12:18:13 UTC |
| 55ee683 | Dominique Larchey-Wendling | 11 December 2019, 12:09:47 UTC | further optimisations of the encoding algo | 11 December 2019, 12:09:47 UTC |
| 0f138dc | Dominique Larchey-Wendling | 11 December 2019, 11:55:30 UTC | reintroduced x = y for smaller encodings | 11 December 2019, 11:55:30 UTC |
| 3639c3c | Dominique Larchey-Wendling | 11 December 2019, 08:28:27 UTC | some cleanup | 11 December 2019, 08:28:27 UTC |
| 46b3729 | Dominique Larchey-Wendling | 11 December 2019, 08:13:30 UTC | improvement in the shapa analysis to produce shorter formulas | 11 December 2019, 08:13:30 UTC |
| 3594fa3 | Dominique Larchey-Wendling | 10 December 2019, 15:04:50 UTC | better notation for De Bruijn extensions wrt the paper | 10 December 2019, 15:04:50 UTC |
| fada11c | Dominique Larchey-Wendling | 10 December 2019, 13:17:10 UTC | a more systematic use of "dio by lemma" | 10 December 2019, 13:17:10 UTC |
| b816b09 | Dominique Larchey-Wendling | 10 December 2019, 13:08:59 UTC | some more comments | 10 December 2019, 13:08:59 UTC |
| c397f3e | Dominique Larchey-Wendling | 10 December 2019, 12:34:29 UTC | reworked the definitions dio_expr now becomes dio_fun which is much more acurate. It could be possible to rework the shape of the Diophantine characterization of alpha and expo to take dio_fun better into account ... | 10 December 2019, 12:34:29 UTC |
| 88e60c7 | Dominique Larchey-Wendling | 10 December 2019, 00:39:24 UTC | last cleanup for tonight | 10 December 2019, 00:39:24 UTC |
| 476e5f5 | Dominique Larchey-Wendling | 10 December 2019, 00:32:56 UTC | much more efficient and cleaner dio auto tactic the only problem is that the size of generate formula is increase at each cleaning changing atoms to elem simplified lost of proofs but got me much bigger encodings in the end ... it does really matter since efficiency is not the objective here | 10 December 2019, 00:32:56 UTC |
| 42b3c41 | Dominique Larchey-Wendling | 09 December 2019, 21:00:35 UTC | cleanup and replaced with dependent reduction ... maybe it would be good to move the definition of reduction_dependent from FRACTRAN_DIO.v to where is belongs ... somewhere in ILL.Definitions | 09 December 2019, 21:00:35 UTC |
| f386a03 | Dominique Larchey-Wendling | 09 December 2019, 15:16:50 UTC | started modifying dio_logic to simplify atoms to something close to dio_elem | 09 December 2019, 15:16:50 UTC |
| 5c8a306 | Dominique Larchey-Wendling | 05 November 2019, 08:55:04 UTC | completed the missing lemma about the godel_beta encoding of list of triples | 05 November 2019, 08:55:04 UTC |
| 0961c52 | Dominique Larchey-Wendling | 04 November 2019, 14:40:19 UTC | added a second universal MuRec based on the alternate constraints of Andrej Dudenhefner 1+x+y^2=z it is 1/4 of the size of the previous one thanks to a much lighter use of decomp_r (which a big MuRec) Unfinished is the fact that nat_h10luc_surj the encoding of list h10uc into nat is total not that hard but a bit tricky though because of the flat_map replacing (x,y,z) -> x##y##z##vec_nil | 04 November 2019, 14:40:19 UTC |
| d74c601 | Dominique Larchey-Wendling | 30 October 2019, 22:06:46 UTC | removed unneeded messages that were poluting the output of make | 30 October 2019, 22:06:46 UTC |
| 8c735b3 | Dominique Larchey-Wendling | 30 October 2019, 19:40:20 UTC | Merge branch 'master' into better_bezout_extraction | 30 October 2019, 19:40:20 UTC |
| 6ddce39 | Dominique Larchey-Wendling | 30 October 2019, 19:25:25 UTC | cleanup of the MM -> FRACTRAN_REG -> MMA2 reduction files remove some unneeded Check and Print Assumptions | 30 October 2019, 19:25:25 UTC |
| 50e31e6 | Dominique Larchey-Wendling | 30 October 2019, 17:40:18 UTC | removed .d files inherited from the CPP'19 developments | 30 October 2019, 17:40:18 UTC |
| 7750f3d | Dominique Larchey-Wendling | 29 October 2019, 23:43:21 UTC | Corrected for 8.8.2 and also cleanup of the mess arround FRACTRAN and MMA2 Now the reduction is MM -> FRACTRAN_REG -> MMA2 and FRACTRAN (non reg) halting could be removed but I also added the trivial FRACTRAN_REG -> FRACTRAN | 29 October 2019, 23:43:21 UTC |
| fc3ec56 | Dominique Larchey-Wendling | 29 October 2019, 20:18:32 UTC | large cleanup of the construction of the universal recalg | 29 October 2019, 20:18:32 UTC |
| ac854d0 | Yannick Forster | 29 October 2019, 11:04:00 UTC | Merge pull request #21 from uds-psl/murec A BIG commit containing the DIO_SINGLE -> µ-REC -> MM reductions | 29 October 2019, 11:04:00 UTC |
| 934f393 | Yannick Forster | 29 October 2019, 11:01:19 UTC | Merge pull request #18 from dominik-kirst/master Trakhtenbrot's theorem | 29 October 2019, 11:01:19 UTC |
| 992e9b1 | Dominique Larchey-Wendling | 28 October 2019, 22:07:51 UTC | added a universal µ-recursive algorithm of size 8708 and of arity 1 that can decide any H10C problem, hence its own termination problem must be undecidable | 28 October 2019, 22:07:51 UTC |
| f190272 | Dominique Larchey-Wendling | 27 October 2019, 11:27:28 UTC | updated gcd and extension of the CRT for preparation with Godel Beta encoding of lists of nats | 27 October 2019, 11:27:28 UTC |
| 3dc1281 | Dominique Larchey-Wendling | 25 October 2019, 21:35:48 UTC | A BIG commit containing the DIO_SINGLE -> µ-REC -> MM reductions The details are going to be comment in the PR Notice that to avoid having several definitions of MM, I needed to generalize the definition to an arbitrary type of registers of which we only use the instance nat and pos _ but this implies changing mm_instr n with mm_instr (pos n) at not so many but several places in the code the rest will be commented in the PR description | 25 October 2019, 21:35:48 UTC |
| 833b141 | Yannick Forster | 25 October 2019, 16:55:45 UTC | Delete .DS_Store | 25 October 2019, 16:55:45 UTC |
| 0aee30f | Yannick Forster | 25 October 2019, 15:28:32 UTC | Merge pull request #17 from uds-psl/induction_on_PR Fixing the induction-on mess | 25 October 2019, 15:28:32 UTC |
| 0226fdd | Yannick Forster | 25 October 2019, 15:27:55 UTC | Merge pull request #16 from fakusb/patch-2 Require Program to avoid spurious compilation bug | 25 October 2019, 15:27:55 UTC |
| a2d831c | Yannick Forster | 25 October 2019, 15:27:42 UTC | Merge pull request #15 from fakusb/patch-1 Update README.md | 25 October 2019, 15:27:42 UTC |
| 7e5482b | Yannick Forster | 25 October 2019, 15:18:38 UTC | fix equations import | 25 October 2019, 15:18:38 UTC |
| 3349e33 | Yannick Forster | 25 October 2019, 14:58:12 UTC | Full qualification for imports | 25 October 2019, 14:58:12 UTC |
| f450bf3 | Fabian Kunze | 25 October 2019, 14:18:32 UTC | Update firstorder.v | 25 October 2019, 14:18:32 UTC |
| 0988442 | Fabian Kunze | 25 October 2019, 14:17:52 UTC | Requiring Program before using measure_wf and MR This hopefully fixes a spurious compilation bug that affects some users. WIP, DO NOT MERGE | 25 October 2019, 14:17:52 UTC |
| 8c6dd6c | Dominique Larchey-Wendling | 25 October 2019, 14:16:22 UTC | cleanup the induction-on tactic mess. remember induction-on revealed a bug in 8.10.0, hopefully getting fixed in 8.10.1 also remove unnecessary Check and Print Assumptions that were bloating the output of make all The one should compile under 8.9.1 (I tested it) | 25 October 2019, 14:16:22 UTC |
| f5f16da | Yannick Forster | 25 October 2019, 14:11:26 UTC | take HOU in again | 25 October 2019, 14:11:26 UTC |
| 365201b | Dominik Kirst | 25 October 2019, 13:58:58 UTC | trakhtenbrot's theorem | 25 October 2019, 13:58:58 UTC |
| 3e4a9b8 | Fabian Kunze | 25 October 2019, 13:43:38 UTC | Update README.md Readme now adds opam repo for equations | 25 October 2019, 13:43:38 UTC |
| b5c5e7d | Yannick Forster | 25 October 2019, 13:25:24 UTC | disable HOU to make travis work once | 25 October 2019, 13:25:24 UTC |
| 92e1029 | Yannick Forster | 25 October 2019, 10:57:36 UTC | Update opam | 25 October 2019, 10:57:36 UTC |
| 81eea1b | Yannick Forster | 24 October 2019, 09:27:22 UTC | Update README.md | 24 October 2019, 09:27:22 UTC |
| 47c8d17 | Yannick Forster | 23 October 2019, 14:54:12 UTC | travis icon | 23 October 2019, 14:54:12 UTC |
| dbf4cf8 | Yannick Forster | 23 October 2019, 14:52:45 UTC | update README | 23 October 2019, 14:52:45 UTC |
| 34e8d80 | Yannick Forster | 23 October 2019, 14:09:53 UTC | Update README | 23 October 2019, 14:09:53 UTC |
| 4544d71 | Yannick Forster | 23 October 2019, 14:06:11 UTC | Add metacoq dependency to opam file | 23 October 2019, 14:06:25 UTC |
| e406355 | Yannick Forster | 23 October 2019, 11:00:02 UTC | fix L for 8.9.1 | 23 October 2019, 11:00:02 UTC |
| b68c48e | Dominique Larchey-Wendling | 16 October 2019, 08:59:50 UTC | some more in the README | 16 October 2019, 08:59:50 UTC |
| 5b17c1c | Dominique Larchey-Wendling | 16 October 2019, 08:57:16 UTC | added "good seed" tags | 16 October 2019, 08:57:16 UTC |
| 0346d27 | Dominique Larchey-Wendling | 16 October 2019, 08:51:07 UTC | Merge branch 'extraction' of github.com:uds-psl/coq-library-undecidability into extraction | 16 October 2019, 08:51:07 UTC |
| b1b7e14 | Dominique Larchey-Wendling | 16 October 2019, 08:50:50 UTC | updated some links in README | 16 October 2019, 08:50:50 UTC |
| f1ae464 | Yannick Forster | 16 October 2019, 07:57:17 UTC | we don't need all of metacoq | 16 October 2019, 07:57:17 UTC |
| 46ccb2e | Yannick Forster | 16 October 2019, 07:33:12 UTC | Merge pull request #12 from fakusb/mergedTMrepo Merged changes from TM-verification repository | 16 October 2019, 07:33:12 UTC |
| fc165f4 | Fabian Kunze | 15 October 2019, 13:41:24 UTC | merged commits after 95967cf up to 31e8023765 verified-turing-machines repo | 15 October 2019, 13:44:17 UTC |
| ffb39b7 | Yannick Forster | 10 October 2019, 19:14:10 UTC | Test for both 8.8.2 and 8.9.1 | 10 October 2019, 19:14:10 UTC |
| 549368f | Yannick Forster | 01 October 2019, 16:03:07 UTC | compilation works locally | 01 October 2019, 16:03:07 UTC |
| 2377511 | Yannick Forster | 01 October 2019, 10:14:15 UTC | travis typo | 01 October 2019, 10:14:15 UTC |
| 7ea5ad4 | Yannick Forster | 01 October 2019, 10:07:22 UTC | Use MetaCoq from opam | 01 October 2019, 10:07:22 UTC |
| edddc56 | Yannick Forster | 01 October 2019, 08:57:36 UTC | Qualify all MetaCoq imports, reorder Makefile | 01 October 2019, 08:57:36 UTC |
| 9591c53 | Yannick Forster | 01 October 2019, 08:06:34 UTC | Fix MetaCoq import in _CoqProject | 01 October 2019, 08:06:34 UTC |
| 7386ea1 | Yannick Forster | 01 October 2019, 07:32:54 UTC | qualify metacoq import | 01 October 2019, 07:32:54 UTC |
| 18503a6 | Yannick Forster | 30 September 2019, 11:36:00 UTC | Fixed travis config | 30 September 2019, 11:36:00 UTC |
| 370c3d4 | Yannick Forster | 30 September 2019, 11:23:49 UTC | travis needs to call configure in template-coq until we have opam packages | 30 September 2019, 11:23:49 UTC |
| 5e7913a | Yannick Forster | 30 September 2019, 11:19:21 UTC | Fix right template-coq branch | 30 September 2019, 11:19:21 UTC |
| 45512bf | Yannick Forster | 30 September 2019, 10:47:47 UTC | Merge branch 'extraction' of github.com:uds-psl/coq-library-undecidability into extraction | 30 September 2019, 10:47:47 UTC |
| d0866db | Yannick Forster | 30 September 2019, 10:47:11 UTC | Add travis file | 30 September 2019, 10:47:11 UTC |
| aeae6cb | Yannick Forster | 30 September 2019, 10:11:10 UTC | Add undecidability of higher-order unification | 30 September 2019, 10:11:10 UTC |
| 52e3845 | Yannick Forster | 17 September 2019, 07:45:18 UTC | Add mTM to TM to CoqProject | 17 September 2019, 07:45:18 UTC |
| 6c2eeb2 | Yannick Forster | 22 May 2019, 13:55:40 UTC | Merge branch 'extraction' of github.com:uds-psl/coq-library-undecidability into extraction | 22 May 2019, 13:55:40 UTC |
| 6438c0d | Yannick Forster | 22 May 2019, 13:55:32 UTC | fixed ocaml version | 22 May 2019, 13:55:32 UTC |
| 9b51e00 | Yannick Forster | 22 May 2019, 13:55:17 UTC | Update README.md | 22 May 2019, 13:55:17 UTC |
| ac100be | Yannick Forster | 22 May 2019, 13:09:30 UTC | Update README Info on how to use right version of Coq and Ocaml using opam | 22 May 2019, 13:09:30 UTC |
| 5d7f36e | Yannick Forster | 22 May 2019, 13:08:32 UTC | Ported to newest template-coq, added opam file | 22 May 2019, 13:08:32 UTC |
| c59beb2 | Yannick Forster | 17 May 2019, 14:54:19 UTC | MM2 | 17 May 2019, 14:54:19 UTC |
| 6f0e996 | Yannick Forster | 17 May 2019, 14:52:54 UTC | re-added _Coqproject | 17 May 2019, 14:52:54 UTC |
| 3fe1201 | Yannick Forster | 17 May 2019, 14:17:34 UTC | Update README.md Fixed submodule instructions | 17 May 2019, 14:17:34 UTC |
| 141e12d | Yannick Forster | 17 May 2019, 10:50:34 UTC | Reduction from multi-tape TM halting to L | 17 May 2019, 10:50:34 UTC |
| afa5244 | Yannick Forster | 17 May 2019, 10:32:35 UTC | removed redundant _CoqProject file | 17 May 2019, 10:32:35 UTC |
| d6469d0 | Yannick Forster | 17 May 2019, 10:15:16 UTC | Merge remote-tracking branch 'origin/wip' into extraction | 17 May 2019, 10:15:16 UTC |
| 7c54049 | Yannick Forster | 17 May 2019, 09:46:57 UTC | Updated README | 17 May 2019, 09:46:57 UTC |
| fe697dc | Yannick Forster | 17 May 2019, 09:38:12 UTC | Added reduction from multi-tapes TMs to single-tape TMs | 17 May 2019, 09:38:12 UTC |
| 103ed89 | Yannick Forster | 16 May 2019, 10:35:16 UTC | Merge pull request #8 from fakusb/L_to_TM added reduction from L to TM | 16 May 2019, 10:35:16 UTC |
| 0e31092 | Fabian Kunze | 06 May 2019, 11:57:45 UTC | removed deleted file | 06 May 2019, 11:57:45 UTC |
| 342ac62 | Fabian Kunze | 06 May 2019, 11:55:43 UTC | moved reduction to Reductions-folder | 06 May 2019, 11:55:43 UTC |
| ffbaf74 | Fabian Kunze | 06 May 2019, 11:42:08 UTC | added reduction from L to TM | 06 May 2019, 11:42:08 UTC |
| f61c040 | Yannick Forster | 03 May 2019, 11:52:56 UTC | Merge branch 'extraction' of github.com:uds-psl/coq-library-undecidability into extraction | 03 May 2019, 11:52:56 UTC |
| cb0e4e0 | Yannick Forster | 03 May 2019, 11:51:57 UTC | L_halt to L_halt_closed to evaLin | 03 May 2019, 11:51:57 UTC |
| f9d16a5 | Yannick Forster | 03 May 2019, 11:22:49 UTC | Merge pull request #7 from fakusb/fix-LM_Lin-red Proof of reduction for LM_Lin compiles again | 03 May 2019, 11:22:49 UTC |
| a174234 | Fabian Kunze | 03 May 2019, 10:46:26 UTC | Proof of reduction for LM_Lin compiles again | 03 May 2019, 10:46:26 UTC |
| 9726fc2 | Yannick Forster | 02 May 2019, 16:01:56 UTC | Updated version of uds-psl-base | 02 May 2019, 16:01:56 UTC |
| ed6755b | Yannick Forster | 02 May 2019, 15:53:41 UTC | Moved website directory to top-level | 02 May 2019, 15:53:41 UTC |
| cb61992 | Yannick Forster | 02 May 2019, 15:49:49 UTC | Updated README file | 02 May 2019, 15:52:22 UTC |
| 722f364 | Yannick Forster | 02 May 2019, 15:16:53 UTC | Added external libraries as submodules | 02 May 2019, 15:16:53 UTC |
| 9dd3812 | Yannick Forster | 02 May 2019, 14:41:08 UTC | Added stack machines for L from APLAS '18 paper | 02 May 2019, 14:41:08 UTC |
| a10d5cd | Yannick Forster | 23 April 2019, 15:07:19 UTC | Everything compiles | 23 April 2019, 16:26:18 UTC |
| 10b94fa | Yannick Forster | 18 April 2019, 16:47:20 UTC | Absolute naming for all files | 18 April 2019, 16:47:20 UTC |
| 233a5c2 | Yannick Forster | 12 April 2019, 09:12:23 UTC | Reducing multi-tape halting on one tape to single-tape halting | 18 April 2019, 13:19:17 UTC |
| 3a4f164 | Yannick Forster | 12 April 2019, 09:24:59 UTC | Merge pull request #5 from uds-psl/mm2 2 counters Minsky machines | 12 April 2019, 09:24:59 UTC |
| 761e59f | Yannick Forster | 10 April 2019, 09:51:33 UTC | Fix TM compilation | 10 April 2019, 09:51:58 UTC |
