Danila Fedorin

DanilaFe pushed to master at Nix-Configs/blog-static-flake

2024-05-16 16:17:36 -07:00

7dad80f44d Update blog source with theme fix

DanilaFe pushed to master at Web-Projects/blog-static

2024-05-16 16:17:07 -07:00

d787548915 Update theme

DanilaFe pushed to master at Web-Projects/vanilla-hugo

2024-05-16 16:16:58 -07:00

f3bf27d4a1 Remove newlines from 'codeurl'

DanilaFe pushed to master at Nix-Configs/blog-static-flake

2024-05-16 16:10:10 -07:00

9ea42f306b Udjust for blog no longer requiring a generated config file

DanilaFe pushed to master at Web-Projects/blog-static

2024-05-16 15:53:19 -07:00

a29bca499f Switch to using data/ for submodule information

DanilaFe pushed to master at Web-Projects/vanilla-hugo

2024-05-16 15:53:14 -07:00

77b8d5e65b Draw from 'data/' for submodule links

DanilaFe pushed to master at Nix-Configs/blog-static-flake

2024-05-14 21:52:09 -07:00

1c3436fdc3 Update blog source

DanilaFe pushed to master at Web-Projects/blog-static

2024-05-14 21:43:31 -07:00

60d3b3025a Flesh out the Lattices post some more

c036041339 Update theme

Compare 2 commits »

DanilaFe pushed to master at Web-Projects/vanilla-hugo

2024-05-14 20:32:32 -07:00

e2fb9362f6 Tweak formattng of tables

038c8e0ac6 Enable bold Raleway loading

Compare 2 commits »

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 »