{"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:1716296963.0","currentOid":""},"activityList":{"items":[{"before":"0fb0ddfbf88f112e19cb76ba4a2f7ef8550ef858","after":"635572bf008833cfc5a05c28ef6faa640b3a0d2e","ref":"refs/heads/cleanup","pushedAt":"2024-07-26T15:04:12.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 map + foldr evaluation","shortMessageHtmlLink":"Fix map + foldr evaluation"}},{"before":"0fe772e952c11d1de85634040b6b66a9faafe28d","after":"700bd4e6d77a61c6bda014f01fb6b4869af05c66","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-07-25T11:42:30.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"bs_to_fs_val_reduction VTuple & VMap scope solved","shortMessageHtmlLink":"bs_to_fs_val_reduction VTuple & VMap scope solved"}},{"before":"e821f5c1f30aee7e422caaab144ae252e32cbf9c","after":"0fe772e952c11d1de85634040b6b66a9faafe28d","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-07-23T21:33:48.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":"bs_to_fs_val_reduction Map using box theorem with flatten_list","shortMessageHtmlLink":"bs_to_fs_val_reduction Map using box theorem with flatten_list"}},{"before":"011712cc388d9d3958cc309e237fee5c7870296b","after":"e821f5c1f30aee7e422caaab144ae252e32cbf9c","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-07-23T20:40:07.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":"comment fix","shortMessageHtmlLink":"comment fix"}},{"before":"6debe7db670e2d5a269b7aa9425629cef6a99f55","after":"011712cc388d9d3958cc309e237fee5c7870296b","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-07-23T20:28:08.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"bs_to_fs_val_reduction Map mostly proved, box theorem mixing","shortMessageHtmlLink":"bs_to_fs_val_reduction Map mostly proved, box theorem mixing"}},{"before":"19e8a2c06e535d7a591869f106c0c2e01641fb12","after":"6debe7db670e2d5a269b7aa9425629cef6a99f55","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-07-17T11:44:41.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"bs_to_fs_val_reduction Map proof started","shortMessageHtmlLink":"bs_to_fs_val_reduction Map proof started"}},{"before":"8f46ded9f0d78d749cbecc43ba8bb04a9ee75944","after":"19e8a2c06e535d7a591869f106c0c2e01641fb12","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-07-11T09:54:18.000Z","pushType":"push","commitsCount":16,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"bs_to_fs_val_reduction Tuple proof almost finished","shortMessageHtmlLink":"bs_to_fs_val_reduction Tuple proof almost finished"}},{"before":"f358a09e1c37cd202a3703904dfc5f05b09b9722","after":"0fb0ddfbf88f112e19cb76ba4a2f7ef8550ef858","ref":"refs/heads/cleanup","pushedAt":"2024-06-20T15:06:50.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 map evaluation in frame stack","shortMessageHtmlLink":"Fix map evaluation in frame stack"}},{"before":"d371cf15df840b77d785bdbc4e5971597792d46c","after":"f358a09e1c37cd202a3703904dfc5f05b09b9722","ref":"refs/heads/cleanup","pushedAt":"2024-06-20T13:11:34.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 big-step map evaluation, and a note about the issues of the small-step version","shortMessageHtmlLink":"Add big-step map evaluation, and a note about the issues of the small…"}},{"before":"1455bbb7d2b69a9ed1f5faecb607349adf554c44","after":"d371cf15df840b77d785bdbc4e5971597792d46c","ref":"refs/heads/cleanup","pushedAt":"2024-06-19T13:15:38.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 case guard exception semantics","shortMessageHtmlLink":"Finish case guard exception semantics"}},{"before":"15755312a940ffe47e1e5186c97a2033b014e7b2","after":"1455bbb7d2b69a9ed1f5faecb607349adf554c44","ref":"refs/heads/cleanup","pushedAt":"2024-06-14T12:31:53.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 case rule - proofs WIP","shortMessageHtmlLink":"Add case rule - proofs WIP"}},{"before":"784d2ec1fb1704d83d212bf05c0d7c476638bdde","after":"15755312a940ffe47e1e5186c97a2033b014e7b2","ref":"refs/heads/cleanup","pushedAt":"2024-06-13T08:09:20.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":"Refactoring steps for function/subst composition","shortMessageHtmlLink":"Refactoring steps for function/subst composition"}},{"before":"4f5d6accfcefa7f4f8d361e45582adac6737deec","after":"8f46ded9f0d78d749cbecc43ba8bb04a9ee75944","ref":"refs/heads/mpeti-equivalence","pushedAt":"2024-05-30T11:01:04.000Z","pushType":"push","commitsCount":19,"pusher":{"login":"breadking99","name":"Peter Miskolczi","path":"/breadking99","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/72017244?s=80&v=4"},"commit":{"message":"small progress","shortMessageHtmlLink":"small progress"}},{"before":"8e76b36b4b48d21a7ab440b403820ef774120442","after":"784d2ec1fb1704d83d212bf05c0d7c476638bdde","ref":"refs/heads/cleanup","pushedAt":"2024-05-29T15:50: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":"Progress with comments","shortMessageHtmlLink":"Progress with comments"}},{"before":"20729093fb6cce2715f73967f877fb4b139f2f30","after":"8e76b36b4b48d21a7ab440b403820ef774120442","ref":"refs/heads/cleanup","pushedAt":"2024-05-23T09:45:30.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":"Comments up to Auxiliaries.v","shortMessageHtmlLink":"Comments up to Auxiliaries.v"}},{"before":"72a98c669ccc3ba2efdec8ac064d34bd55ec530d","after":null,"ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-05-21T13:08:59.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":"2b9511f59f797bb38c477597cff68bc151881d18","after":"f9bebc50b89db5e7b8a96b26069cb5ad92b7ae3d","ref":"refs/heads/master","pushedAt":"2024-05-21T13:08:56.000Z","pushType":"pr_merge","commitsCount":21,"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 #26 from harp-project/concurrency-normalisation\n\nBisimulation examples","shortMessageHtmlLink":"Merge pull request #26 from harp-project/concurrency-normalisation"}},{"before":"1a3778acf2e791f59522553a8596bb8364482316","after":"72a98c669ccc3ba2efdec8ac064d34bd55ec530d","ref":"refs/heads/concurrency-normalisation","pushedAt":"2024-05-21T11:55:12.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":"Remove warnings","shortMessageHtmlLink":"Remove warnings"}},{"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 & 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 & 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"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEiidddAA","startCursor":null,"endCursor":null}},"title":"Activity · harp-project/Core-Erlang-Formalization"}