{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":709006770,"defaultBranch":"main","name":"fiat2","ownerLogin":"mit-plv","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2023-10-23T20:32:39.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/11860253?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1715488072.0","currentOid":""},"activityList":{"items":[{"before":"7855874b30d3d1a6d2488ecd4b351e39821a1dae","after":"30f1c09ebf5116c9be43bd8f969a8c3131c4df25","ref":"refs/heads/main","pushedAt":"2024-05-21T16:03:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Prove typechecker soundness","shortMessageHtmlLink":"Prove typechecker soundness"}},{"before":"d2e07b33584fd2733e28b01f171fb2ff7bf83f0f","after":"7855874b30d3d1a6d2488ecd4b351e39821a1dae","ref":"refs/heads/main","pushedAt":"2024-05-17T21:50:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Define inductive typing judgements for unops and binops","shortMessageHtmlLink":"Define inductive typing judgements for unops and binops"}},{"before":"1f436993091d5303c0f8ca80eeddbf8984d0c8a8","after":"d2e07b33584fd2733e28b01f171fb2ff7bf83f0f","ref":"refs/heads/main","pushedAt":"2024-05-17T00:34:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Prove typechecker soundness for Records","shortMessageHtmlLink":"Prove typechecker soundness for Records"}},{"before":"5fb925918ffb7063bcbd238bdb9c8fc948ec22b5","after":"1f436993091d5303c0f8ca80eeddbf8984d0c8a8","ref":"refs/heads/main","pushedAt":"2024-05-13T18:54:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Prove first case of typechecker soundness for Records","shortMessageHtmlLink":"Prove first case of typechecker soundness for Records"}},{"before":"226d79d028b27d05937befe72ebbe7ae2a10d64f","after":null,"ref":"refs/heads/rel_constructors","pushedAt":"2024-05-12T04:27:52.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"}},{"before":"349c8308cd61258484fe24fa3835246c9e1628b2","after":"5fb925918ffb7063bcbd238bdb9c8fc948ec22b5","ref":"refs/heads/main","pushedAt":"2024-05-12T04:27:46.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Merge pull request #8 from mit-plv/rel_constructors\n\nAdd relational algebra constructors to expr","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2291160611\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mit-plv/fiat2/issues/8\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mit-plv/fiat2/pull/8/hovercard\" href=\"https://github.com/mit-plv/fiat2/pull/8\">#8</a> from mit-plv/rel_constructors"}},{"before":"9dbd81081c05fd0bb0a99c7fb5fe101b44be287a","after":"226d79d028b27d05937befe72ebbe7ae2a10d64f","ref":"refs/heads/rel_constructors","pushedAt":"2024-05-12T04:23:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Edit relational algebra constructs and the interpreter","shortMessageHtmlLink":"Edit relational algebra constructs and the interpreter"}},{"before":null,"after":"9dbd81081c05fd0bb0a99c7fb5fe101b44be287a","ref":"refs/heads/rel_constructors","pushedAt":"2024-05-06T16:21:03.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Update expr to include constructors for relational algebra","shortMessageHtmlLink":"Update expr to include constructors for relational algebra"}},{"before":"3244291494d98f3cc358335f410c4d5922dbf546","after":"349c8308cd61258484fe24fa3835246c9e1628b2","ref":"refs/heads/main","pushedAt":"2024-04-27T22:31:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Update relational IR and its interpretation\n\nDefine bidirectional type checking functions\n\nAdd git submodule for sorting, modified from the Coq standard library to work better with Sections","shortMessageHtmlLink":"Update relational IR and its interpretation"}},{"before":"605e761fc71bd7ecd5b38144e9e0249ff333b1b1","after":"3244291494d98f3cc358335f410c4d5922dbf546","ref":"refs/heads/main","pushedAt":"2024-04-19T03:44:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Initial attempt at using a non-dependent type system to formulate Fiat2","shortMessageHtmlLink":"Initial attempt at using a non-dependent type system to formulate Fiat2"}},{"before":"bd7a939ae916736f3343f49db90b3f9eddc09b73","after":"605e761fc71bd7ecd5b38144e9e0249ff333b1b1","ref":"refs/heads/main","pushedAt":"2024-04-19T03:32:01.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Merge pull request #7 from leognon/constant_fold_flatmap\n\nAdd flatmap folding optimization to constant folding","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2251186072\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mit-plv/fiat2/issues/7\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mit-plv/fiat2/pull/7/hovercard\" href=\"https://github.com/mit-plv/fiat2/pull/7\">#7</a> from leognon/constant_fold_flatmap"}},{"before":"29eb5bcd6c4b7e780465e2f261162a315d289bec","after":"bd7a939ae916736f3343f49db90b3f9eddc09b73","ref":"refs/heads/main","pushedAt":"2024-04-10T20:55:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Optimize proofs for lifting","shortMessageHtmlLink":"Optimize proofs for lifting"}},{"before":"c128d6715a79588f0a16e381fd15b4f507865073","after":"29eb5bcd6c4b7e780465e2f261162a315d289bec","ref":"refs/heads/main","pushedAt":"2024-04-10T00:55:50.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Merge pull request #6 from leognon/constant_fold_assoc\n\nConstant fold assoc","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2234346110\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mit-plv/fiat2/issues/6\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mit-plv/fiat2/pull/6/hovercard\" href=\"https://github.com/mit-plv/fiat2/pull/6\">#6</a> from leognon/constant_fold_assoc"}},{"before":"570065bec8bdb1a9bb220c8e55b5410206061812","after":"c128d6715a79588f0a16e381fd15b4f507865073","ref":"refs/heads/main","pushedAt":"2024-03-20T21:53:53.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Merge pull request #5 from leognon/printing_notations\n\nAdd printing notations for elaborated commands","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2198525075\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mit-plv/fiat2/issues/5\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mit-plv/fiat2/pull/5/hovercard\" href=\"https://github.com/mit-plv/fiat2/pull/5\">#5</a> from leognon/printing_notations"}},{"before":"6630e5c8060be1afedc25181a9105885f80d15a2","after":"570065bec8bdb1a9bb220c8e55b5410206061812","ref":"refs/heads/main","pushedAt":"2024-03-18T17:12:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Define functions for lifting complex expressions\n\nProve the correctness and the soundness of the lifting functions","shortMessageHtmlLink":"Define functions for lifting complex expressions"}},{"before":"0992ed36a53d07ec52a6ae65e3abdc1d0f23822f","after":"6630e5c8060be1afedc25181a9105885f80d15a2","ref":"refs/heads/main","pushedAt":"2024-02-22T04:38:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Define Dictionaries in Fiat2","shortMessageHtmlLink":"Define Dictionaries in Fiat2"}},{"before":"c8354a759bb88f3cd550ab336b6af3bfc10d7fd6","after":"0992ed36a53d07ec52a6ae65e3abdc1d0f23822f","ref":"refs/heads/main","pushedAt":"2024-02-13T16:26:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Add examples of let-lifting","shortMessageHtmlLink":"Add examples of let-lifting"}},{"before":"cc83d6ec7de9f083bc6b156ff877e6e7839797af","after":"c8354a759bb88f3cd550ab336b6af3bfc10d7fd6","ref":"refs/heads/main","pushedAt":"2024-02-08T04:10:34.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Merge pull request #4 from leognon/fold_expr_correct\n\nFold expr correct","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2123957289\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mit-plv/fiat2/issues/4\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mit-plv/fiat2/pull/4/hovercard\" href=\"https://github.com/mit-plv/fiat2/pull/4\">#4</a> from leognon/fold_expr_correct"}},{"before":"10167584140d925835d65b652d5f1f82745370c0","after":"cc83d6ec7de9f083bc6b156ff877e6e7839797af","ref":"refs/heads/main","pushedAt":"2024-02-07T14:00:21.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Merge pull request #3 from psvenk/expression-compiler\n\nFinish expression compiler","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2122057510\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mit-plv/fiat2/issues/3\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mit-plv/fiat2/pull/3/hovercard\" href=\"https://github.com/mit-plv/fiat2/pull/3\">#3</a> from psvenk/expression-compiler"}},{"before":"b164f5eb3f11407ca13e631fb15344fc34629518","after":"10167584140d925835d65b652d5f1f82745370c0","ref":"refs/heads/main","pushedAt":"2024-01-31T23:13:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Improve the proof of let-lifting correctness; fix a bug in Queries.v","shortMessageHtmlLink":"Improve the proof of let-lifting correctness; fix a bug in Queries.v"}},{"before":"5af0e73dcfa5e84fa0e298f532052003fb56e717","after":"b164f5eb3f11407ca13e631fb15344fc34629518","ref":"refs/heads/main","pushedAt":"2024-01-29T18:04:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Prove the correctness of let-lifting","shortMessageHtmlLink":"Prove the correctness of let-lifting"}},{"before":"c18c7a268ed601c405a54cdf587450492a740df3","after":"5af0e73dcfa5e84fa0e298f532052003fb56e717","ref":"refs/heads/main","pushedAt":"2024-01-26T19:02:35.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Merge pull request #2 from leognon/move_filter\n\nAdd move filter optimization","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2102531973\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mit-plv/fiat2/issues/2\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mit-plv/fiat2/pull/2/hovercard\" href=\"https://github.com/mit-plv/fiat2/pull/2\">#2</a> from leognon/move_filter"}},{"before":"14d14aa837a2c33345008063da9a642ae80ecf07","after":"c18c7a268ed601c405a54cdf587450492a740df3","ref":"refs/heads/main","pushedAt":"2024-01-17T20:04:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Implement phoas_command and its conversions to and from command","shortMessageHtmlLink":"Implement phoas_command and its conversions to and from command"}},{"before":"3eb9dd0b2c1a6c7607c6a7f314a6f2a2ff5b0687","after":"14d14aa837a2c33345008063da9a642ae80ecf07","ref":"refs/heads/main","pushedAt":"2024-01-10T20:18:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Update bedrock2 submodule to the first commit where fiat2 (previously PyLevelLang) has been removed","shortMessageHtmlLink":"Update bedrock2 submodule to the first commit where fiat2 (previously…"}},{"before":"523f3f0dfe69e9eb5dc68ed8ef6098d91b641126","after":"3eb9dd0b2c1a6c7607c6a7f314a6f2a2ff5b0687","ref":"refs/heads/main","pushedAt":"2024-01-10T19:29:01.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Update logical paths from PyLevelLang to fiat2\nChange Makefiles, imports, scope names and custom names accordingly","shortMessageHtmlLink":"Update logical paths from PyLevelLang to fiat2"}},{"before":"4c45630c50ad3a29c2df41d51b2a775d2e9725cc","after":"523f3f0dfe69e9eb5dc68ed8ef6098d91b641126","ref":"refs/heads/main","pushedAt":"2024-01-04T03:38:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Implement flatmap_flatmap and fold_flatmap transformations on phoas expressions with correctness proofs","shortMessageHtmlLink":"Implement flatmap_flatmap and fold_flatmap transformations on phoas e…"}},{"before":"ee043ef5b5f580313456e4fae74e556c7ef47d50","after":"4c45630c50ad3a29c2df41d51b2a775d2e9725cc","ref":"refs/heads/main","pushedAt":"2023-12-22T17:25:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Prove soundness of fold_add pipeline for arbitrary expressions","shortMessageHtmlLink":"Prove soundness of fold_add pipeline for arbitrary expressions"}},{"before":"2129e54ced1aa9723c8e44c02d5a9ed78acb910d","after":"ee043ef5b5f580313456e4fae74e556c7ef47d50","ref":"refs/heads/main","pushedAt":"2023-12-21T15:45:11.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Add an example phoasify-transform-dephoasify pipeline with soundness proof and tactics for more automation","shortMessageHtmlLink":"Add an example phoasify-transform-dephoasify pipeline with soundness …"}},{"before":"566717bb53d9a3c22a31957b1146cf0a02849e4b","after":"2129e54ced1aa9723c8e44c02d5a9ed78acb910d","ref":"refs/heads/main","pushedAt":"2023-12-20T22:37:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Introduce phoas_env required by interp_phoas_expr in Phoas_Optimize.v","shortMessageHtmlLink":"Introduce phoas_env required by interp_phoas_expr in Phoas_Optimize.v"}},{"before":"e438663bd42841528e905ccc65bf8f20afff4bc3","after":"566717bb53d9a3c22a31957b1146cf0a02849e4b","ref":"refs/heads/main","pushedAt":"2023-12-20T18:04:48.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"amanda4zx","name":"Xin Zhang (Amanda)","path":"/amanda4zx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/50391546?s=80&v=4"},"commit":{"message":"Merge pull request #1 from leognon/Phoas_constant_folding\n\nFix JSON output; add large sample DB queries and PHOAS constant folding","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2049461963\" data-permission-text=\"Title is private\" data-url=\"https://github.com/mit-plv/fiat2/issues/1\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/mit-plv/fiat2/pull/1/hovercard\" href=\"https://github.com/mit-plv/fiat2/pull/1\">#1</a> from leognon/Phoas_constant_folding"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEUAxAtgA","startCursor":null,"endCursor":null}},"title":"Activity · mit-plv/fiat2"}