{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":224431756,"defaultBranch":"master","name":"Core-Erlang-Formalization","ownerLogin":"harp-project","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2019-11-27T12:58:50.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/57445458?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1715606764.0","currentOid":""},"activityList":{"items":[{"before":null,"after":"20729093fb6cce2715f73967f877fb4b139f2f30","ref":"refs/heads/cleanup","pushedAt":"2024-05-13T13:26:04.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Start commenting","shortMessageHtmlLink":"Start commenting"}},{"before":"eca4e27c6d72cc367028ee0d9e47ba669f287a31","after":"4f5d6accfcefa7f4f8d361e45582adac6737deec","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-05-08T18:12:30.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"defining bigstep_eq_framstack","shortMessageHtmlLink":"defining bigstep_eq_framstack"}},{"before":"61c1a5dd8b91daf16e8e122ce4906a7f77a629f4","after":"1a3778acf2e791f59522553a8596bb8364482316","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-05-08T12:30:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Further cleanup","shortMessageHtmlLink":"Further cleanup"}},{"before":"e45d9f88e11a21ea5c273660d7a1cc1612d30125","after":"61c1a5dd8b91daf16e8e122ce4906a7f77a629f4","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-05-06T16:56:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"cleanup + exceptions for trap_exit","shortMessageHtmlLink":"cleanup + exceptions for trap_exit"}},{"before":"9ec4bd620684ba626596c02c019bc5d827f6c956","after":"eca4e27c6d72cc367028ee0d9e47ba669f287a31","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-04-28T14:00:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"mesure_exp & mesure_val for Program Fixpoint","shortMessageHtmlLink":"mesure_exp &amp; mesure_val for Program Fixpoint"}},{"before":"28f93870227c03f892c623ed00900c5c70caba7b","after":"9ec4bd620684ba626596c02c019bc5d827f6c956","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-04-27T15:43:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"mapM and VClos fid refactor up to BigStep.v\n\nEquivalence:\n* sequence . map -> mapM\n* todo: dual define value_to_exp & subst_bigstep\n\nRefactor:\n* Equalites: opt funid dec refl eq theorems added, profs fixed\n* Enivorment & Bigstep: properly defined\n* Others: added None parameter to VClos","shortMessageHtmlLink":"mapM and VClos fid refactor up to BigStep.v"}},{"before":"359a2ec2fe46aef30a4d3760eb5808da2d3632a8","after":"28f93870227c03f892c623ed00900c5c70caba7b","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-04-23T09:11:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"option map fix & make subst_bigstep optional\n\nRenamed valueToExpression to value_to_expression and substB to subst_bigstep.\nInstead mapOption I use (sequence . map), sequence is defined by me.\nI made subst_bistep return option Expression.","shortMessageHtmlLink":"option map fix &amp; make subst_bigstep optional"}},{"before":"e8c9183bfacad2e117121bd039a594edaa9baf18","after":"e45d9f88e11a21ea5c273660d7a1cc1612d30125","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-04-22T12:37:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Add more tau actions","shortMessageHtmlLink":"Add more tau actions"}},{"before":"5dcf5e4dfd71852dbbd52b474e5d29290f1d855f","after":"e8c9183bfacad2e117121bd039a594edaa9baf18","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-04-18T13:21:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Unnecessary condition removed","shortMessageHtmlLink":"Unnecessary condition removed"}},{"before":null,"after":"359a2ec2fe46aef30a4d3760eb5808da2d3632a8","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-04-16T11:12:44.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"Syntac Value VClos fid FunctionIdentifier added","shortMessageHtmlLink":"Syntac Value VClos fid FunctionIdentifier added"}},{"before":"5296a5325cc3d3f7b6fdd512960f9f5baf00265e","after":"5dcf5e4dfd71852dbbd52b474e5d29290f1d855f","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-04-09T08:53:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Finish map ~ pmap equivalence (if no errors occur)","shortMessageHtmlLink":"Finish map ~ pmap equivalence (if no errors occur)"}},{"before":"173093bd7c1995b8a49f6a236e42151d24fcc2f3","after":"5296a5325cc3d3f7b6fdd512960f9f5baf00265e","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-04-08T16:03:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"1 admit solved, 1 remains in map ~ pmap","shortMessageHtmlLink":"1 admit solved, 1 remains in map ~ pmap"}},{"before":"36b0fea16b7b1cce36b454a1b179086bf2c45d81","after":"173093bd7c1995b8a49f6a236e42151d24fcc2f3","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-04-03T09:36:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Getting stuck again with spawned process (almost) termination","shortMessageHtmlLink":"Getting stuck again with spawned process (almost) termination"}},{"before":"a8c158875b5e78ee1f0fc62e4a022cf03c3fbb1d","after":"36b0fea16b7b1cce36b454a1b179086bf2c45d81","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-04-02T15:03:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Proved map ~ pmap - except 2 Admitted lemmas","shortMessageHtmlLink":"Proved map ~ pmap - except 2 Admitted lemmas"}},{"before":"7e3c4bdd3aae4b145855ad8919973194a6e050b6","after":"a8c158875b5e78ee1f0fc62e4a022cf03c3fbb1d","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-04-01T12:39:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Map ~ pmap <- direction, sequential parts","shortMessageHtmlLink":"Map ~ pmap &lt;- direction, sequential parts"}},{"before":"42af3e7dde2b63fbf2f8165298a49a2de301b92d","after":"7e3c4bdd3aae4b145855ad8919973194a6e050b6","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-03-28T14:42:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Multiple improvements\n\n- Fixed the syntax of EReceive - remove_message was missing\n- Simple concurrent equivalences - which have not that simple proofs\n- => direction of the map-parallel map equivalence","shortMessageHtmlLink":"Multiple improvements"}},{"before":"255ab973707d02e18083f057a72deb5af9953a06","after":"42af3e7dde2b63fbf2f8165298a49a2de301b92d","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-03-26T09:15:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"arrive confluence in normalisation","shortMessageHtmlLink":"arrive confluence in normalisation"}},{"before":"43edbd0da2d003409b7a1a96586dd02648cacd63","after":"255ab973707d02e18083f057a72deb5af9953a06","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-03-25T17:49:11.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Progress with normalisation subgoals","shortMessageHtmlLink":"Progress with normalisation subgoals"}},{"before":"10b8266aaba4a1267bc303c00d0763a0e5797409","after":"43edbd0da2d003409b7a1a96586dd02648cacd63","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-03-20T16:29:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"More progress with ether update bisim","shortMessageHtmlLink":"More progress with ether update bisim"}},{"before":"dd00126ea38685703aedae0672ecfaca20fe6b3f","after":"10b8266aaba4a1267bc303c00d0763a0e5797409","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-03-20T13:39:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Progress with etherUpdate","shortMessageHtmlLink":"Progress with etherUpdate"}},{"before":"35976f14949e88c05e9127531a387939c98a6e2b","after":"dd00126ea38685703aedae0672ecfaca20fe6b3f","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-03-20T08:43:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Progress with spawn bisims","shortMessageHtmlLink":"Progress with spawn bisims"}},{"before":"79ef94b724ef27ebe2dfc6795f5709c15b14051c","after":"35976f14949e88c05e9127531a387939c98a6e2b","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-03-13T16:27:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Fix major bug in spawn_link, progress with equivalence for spawn_link","shortMessageHtmlLink":"Fix major bug in spawn_link, progress with equivalence for spawn_link"}},{"before":null,"after":"79ef94b724ef27ebe2dfc6795f5709c15b14051c","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-03-12T12:39:18.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"tau steps make a bisimulation","shortMessageHtmlLink":"tau steps make a bisimulation"}},{"before":"0f9755e6f325f567d2276c737d2a928eaa992d85","after":null,"ref":"refs/heads/concurrency-w-output-interface","pushedAt":"2024-03-11T12:25:30.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"}},{"before":"2a663b6482718bed1ebd547ec55d019033ac7731","after":"2b9511f59f797bb38c477597cff68bc151881d18","ref":"refs/heads/master","pushedAt":"2024-03-11T12:25:27.000Z","pushType":"pr_merge","commitsCount":120,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Merge pull request #25 from harp-project/concurrency-w-output-interface\n\nUnnecessary axioms, bisimulations, renaming equivalence in the concurrent setup and Coq 8.18","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2163550968\" data-permission-text=\"Title is private\" data-url=\"https://github.com/harp-project/Core-Erlang-Formalization/issues/25\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/harp-project/Core-Erlang-Formalization/pull/25/hovercard\" href=\"https://github.com/harp-project/Core-Erlang-Formalization/pull/25\">#25</a> from harp-project/concurrency-w-output-interface"}},{"before":"c9298d14b9e76c652a4b876cd10595ec3879d919","after":"0f9755e6f325f567d2276c737d2a928eaa992d85","ref":"refs/heads/concurrency-w-output-interface","pushedAt":"2024-03-11T11:14:36.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Finished cleanup","shortMessageHtmlLink":"Finished cleanup"}},{"before":"9d6be109eda5b4550b8bf07d5293656e78c116b2","after":"c9298d14b9e76c652a4b876cd10595ec3879d919","ref":"refs/heads/concurrency-w-output-interface","pushedAt":"2024-03-08T16:05:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Solve non-experimental admits","shortMessageHtmlLink":"Solve non-experimental admits"}},{"before":"383988c6dcfa2ea1e45432d4ef75d310ab2a06ce","after":"9d6be109eda5b4550b8bf07d5293656e78c116b2","ref":"refs/heads/concurrency-w-output-interface","pushedAt":"2024-03-07T12:34:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Getting rid of more admits","shortMessageHtmlLink":"Getting rid of more admits"}},{"before":"ab87ebe70ac6aa0f8a27a76ade7013bbec47c872","after":"383988c6dcfa2ea1e45432d4ef75d310ab2a06ce","ref":"refs/heads/concurrency-w-output-interface","pushedAt":"2024-03-06T16:51:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Add foldr-map equivalence","shortMessageHtmlLink":"Add foldr-map equivalence"}},{"before":"b03960f2eeec43384a3c3f10f038b326e78769db","after":"ab87ebe70ac6aa0f8a27a76ade7013bbec47c872","ref":"refs/heads/concurrency-w-output-interface","pushedAt":"2024-03-05T14:26:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"berpeti","name":"Péter Bereczky","path":"/berpeti","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/30949137?s=80&v=4"},"commit":{"message":"Beta equivalence","shortMessageHtmlLink":"Beta equivalence"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAESHBAugA","startCursor":null,"endCursor":null}},"title":"Activity · harp-project/Core-Erlang-Formalization"}