Danila Fedorin DanilaFe
0 Followers · 0 Following
Repositories
11
 Projects Packages Code Public Activity Starred Repositories
DanilaFe pushed to master at Nix-Configs/server-config 2024-05-13 19:51:13 -07:00
fc0ff8a586 Update flake.lock with new nixpkgs etc.
355dc7cf9d Update to proper version of nix.package
Compare 2 commits »
DanilaFe pushed to master at Nix-Configs/blog-static-flake 2024-05-13 19:46:21 -07:00
6b8fa513b4 Update lock to new dependency versions
DanilaFe pushed to master at Nix-Configs/blog-static-flake 2024-05-13 19:43:44 -07:00
c1283b0165 Use instable nix pkgs
DanilaFe pushed to master at Web-Projects/blog-static 2024-05-13 19:16:58 -07:00
1df315612a Update "typesafe interpreter" article to new math delimiters
15beddf96b Update btree article with new math delimiters
20d8b18a9b Update 'stack language recursion' article to new math delimiters
53ff0c39e4 Update "search as polynomial" article to new math delimiters
357a3bef09 Update the modulo patterns article to use new delimiters
Compare 31 commits »
DanilaFe pushed to master at Web-Projects/blog-static 2024-05-12 18:59:09 -07:00
e063ff6aa5 Update the vanilla theme
DanilaFe pushed to master at Web-Projects/vanilla-hugo 2024-05-12 18:58:39 -07:00
2c13bf93cb Add a shortcode to just get the URL of a code file
DanilaFe pushed to master at Web-Projects/blog-static 2024-05-12 18:54:32 -07:00
6179c86919 Show the basic Nat lattice.
a20fe07a56 Move original 'monotone function' text into new post and heavily rework it
2b5dcf12d7 Rename the SPA intro to have a specific name
5873c1ca96 Write a high-level introduction for the SPA series
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-05-10 22:31:58 -07:00
7d2928ed81 Prove that the sign analysis is correct
5f946de5e8 Remove last remaining assumption for correctness
04bafb2d55 Prove that the inputs to wrap are empty
Compare 3 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-05-10 00:01:08 -07:00
e0248397b7 Prove that predecessors imply edges
41ada43047 Move predecessor code into Graphs
a081edb881 Add a proof about filter's distributivity
Compare 3 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-05-09 22:52:10 -07:00
3d2a507f2f Almost prove correctness
82027ecd04 Move predecessor computation into Graphs
734e82ff6d Wrap generated graphs to ensure entry and exit nodes have no extra edges
69d1ecebae Prove that the bottom map's valyes are all bottoms
b78cb91f2a Strengthen lemma about IterProd bottom to definition equality
Compare 14 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-05-08 23:38:41 -07:00
f0b0d51b48 Add unproven lemma about fold implication
8ff88f9f9e Move helper code into separate function
c1581075d3 Add more test programs
838aaf9c58 Start end-to-end proof of correctness
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-05-08 22:53:56 -07:00
4ac9dffa9b Prove that the var->lattice maps respect equality
3f5551d70c Add a lemma about the effect of joinAll
5837fdf19b Prove that 'updateAll' has preservation
4350919871 Add proof about setVariablesForState
7fe46b014c Slightly simplify evaluation code
Compare 12 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-30 22:15:54 -07:00
3859826293 Define interpretation of the sign lattice
be50c76cb1 Add more higher-order primitives
112a5087ef Tentative start on proving correctness
ccb7abc501 Remove unused code from Utils
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-29 21:28:45 -07:00
91b5d108f6 Simplify proofs about 'loop' using concatenation lemma
c574ca9c56 Prove that graphs build by buildCfg are sufficient
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-28 15:16:35 -07:00
bbfba34e05 Prove another (simple) case
aec15573fc Add properties of end-to-end traces on loops
b4d395767d Simplify operations used for constructing graphs
Compare 3 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-28 12:25:19 -07:00
07550bc214 Prove 'sufficiency' for if-else.
9366ec4a97 Allow promoting end-to-end traces too
0fb884eb07 Use implicit arguments for more things
6b44ac1feb Make graph arguments implicit where possible
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-28 00:27:06 -07:00
69a4e8eb5c Add some helpers and rewrite code
4fee16413a Define end-to-end path concatenation and prove one more case
316e56f2bc Dip toes into creating end-to-end traces
ab40a27e78 Formulate correctness of buildCfg using end-to-end traces
f555947184 Promote traces through loop
Compare 8 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-25 23:22:17 -07:00
f2b8084a9c Delete code that won't be used for this approach
c00c8e3e85 Use different graph operations to implement construction
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-20 21:42:53 -07:00
b134c143ca Start working on proving 'sufficiency'
e218d1b7a3 Add formalization of 'traces through graph'
6e3f06ca5d Add a new 'properties' module
54b11d21b0 Start working on proving facts about graph construction
f3e0d5f2e3 Use 'data' instead of aliases to prove reasoning properties
Compare 6 commits »
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2024-04-20 14:10:26 -07:00
14b63fccc2 Revert "Reduce gas for proof search"