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 |
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 |
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 |
240c83e | Yannick Forster | 10 April 2019, 09:51:14 UTC | Moved files | 10 April 2019, 09:51:14 UTC |
f2cb1e7 | Dominique Larchey-Wendling | 08 March 2019, 15:12:23 UTC | Merge branch 'wip' into mm2 | 08 March 2019, 15:12:23 UTC |
c62c42c | Dominique Larchey-Wendling | 08 March 2019, 15:06:50 UTC | added UNDEC for two counters Minsky machines with self-contained explanations | 08 March 2019, 15:06:50 UTC |
bbde09b | Dominique Larchey-Wendling | 08 March 2019, 12:08:32 UTC | some more comments | 08 March 2019, 12:08:32 UTC |
39635d3 | Dominique Larchey-Wendling | 08 March 2019, 12:01:37 UTC | adding a self contained description of MM2 (with 2 counters) not using vectors or pos etc ... | 08 March 2019, 12:01:37 UTC |
415cdf9 | Yannick Forster | 08 March 2019, 11:38:45 UTC | Added install and uninstall targets | 08 March 2019, 11:38:45 UTC |
3967674 | Yannick Forster | 08 March 2019, 09:50:07 UTC | Merge pull request #4 from uds-psl/constraints Constraints | 08 March 2019, 09:50:07 UTC |
b8c3875 | Yannick Forster | 08 March 2019, 09:49:08 UTC | Update README.md | 08 March 2019, 09:49:08 UTC |
3bc2e34 | Dominique Larchey-Wendling | 07 March 2019, 13:45:11 UTC | some comments about the encoding DIO_ELEM -> H10C | 07 March 2019, 13:45:11 UTC |
6140f38 | Dominique Larchey-Wendling | 07 March 2019, 11:50:36 UTC | added MM -> FRACTRAN in Reductions | 07 March 2019, 11:50:36 UTC |
659a205 | Dominique Larchey-Wendling | 07 March 2019, 09:36:32 UTC | update README | 07 March 2019, 09:36:32 UTC |
7acd984 | Dominique Larchey-Wendling | 07 March 2019, 09:30:29 UTC | added a self contained description of H10 on elementary constraints w/o parameters and a reduction from FRACTRAN | 07 March 2019, 09:30:29 UTC |
08e50c2 | Yannick Forster | 05 March 2019, 09:23:37 UTC | Merge branch 'wip' of github.com:uds-psl/coq-library-undecidability into wip | 05 March 2019, 09:23:37 UTC |
1389829 | Yannick Forster | 05 March 2019, 09:18:08 UTC | More transparent definitions for extraction | 05 March 2019, 09:18:08 UTC |
6529d8c | Dominique Larchey-Wendling | 02 March 2019, 08:41:47 UTC | added the licence file | 02 March 2019, 08:41:47 UTC |