Danila Fedorin

DanilaFe pushed to main at DanilaFe/agda-spa

2024-04-08 22:49:57 -07:00

3e2719d45f Turn old proof into a hole to clean up later.

78252b6c9e Add proof of node preservation for adding edges.

Compare 2 commits »

DanilaFe pushed to main at DanilaFe/agda-spa

2024-04-08 22:21:45 -07:00

85fdf544b9 Translate informal proof of (node) transitivity into formal one.

DanilaFe pushed to main at DanilaFe/agda-spa

2024-04-08 00:30:58 -07:00

4f14a7b765 Successfully prove that monotonic updates preserve existing indices

bc5b4b7d9e Explicitly write metas for missing functions

520b2b514c Clear up vector reindexing

f7ac22257e Beat head against the vector-cast wall.

b72ad070ba Try using index-based comparisons

Compare 7 commits »

DanilaFe pushed to main at DanilaFe/agda-spa

2024-04-04 22:34:38 -07:00

b505063771 Start working on proofs of Graph-related things

844c99336a Intermediate commit: add while loops and start trying to formalize them.

Compare 2 commits »

DanilaFe pushed to main at DanilaFe/agda-spa

2024-03-24 12:11:10 -07:00

5d56a7ce2d Fix comments in Forward.agda

2e096bd64e Extract common parts of forward analyses into Forward.agda

1a7b2a1736 Adjust behavior of eval to not require constant 'k in vars' threading

Compare 3 commits »

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

2024-03-14 22:25:39 -07:00

c6e2ecb996 Add first section of Agda program analysis article

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

2024-03-13 16:04:33 -07:00

2130b00752 Narrow some of the tags

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

2024-03-13 15:06:02 -07:00

474c3a8348 Switch bracket types in Agda expression pattern post

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

2024-03-11 23:26:20 -07:00

29a18b8b37 Add description to expr_pattern

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

2024-03-11 23:21:17 -07:00

21ab4f0a8b Update theme

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

2024-03-11 23:20:52 -07:00

9c9ced66c3 Allow hiding code in code blocks

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

2024-03-11 23:16:20 -07:00

7d2842fd64 Add article about the 'deeply embedded expression' pattern

cd4c121e07 Update the theme

d0570f876e Add the SPA code as a submodule

Compare 3 commits »

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

2024-03-11 15:50:33 -07:00

9b9a6dca5f Decorate blockquotes a bit

DanilaFe pushed to main at DanilaFe/agda-spa

2024-03-11 14:10:14 -07:00

f0da9a9020 Move more code out of Sign and into Main

040c13caba Use instances to simplify printing code

56da61b339 Delete the bundles since they did not turn out all that useful

Compare 3 commits »

DanilaFe pushed to main at DanilaFe/agda-spa

2024-03-10 22:25:16 -07:00

3e88a64ed9 Add some debugging code to sign analysis to print the results

8a85c4497c Prove that evaluation is monotonic and complete sign analysis

8964ba59a1 Prove monotonicity of eval

96f3ceaeb2 Use the previous join function directly in GeneralizedUpdate

237250cf72 Stop using modules in 'Sign' analysis

Compare 11 commits »

DanilaFe pushed to main at DanilaFe/agda-spa

2024-03-09 23:50:14 -08:00

fdc40632bf Add a way to retrieve the code for a particular state

f84a1c923c Prove that the 'join' transformation is monotonic

Compare 2 commits »

DanilaFe pushed to main at DanilaFe/agda-spa

2024-03-09 21:47:19 -08:00

1b1b80465c Use named modules to avoid having to pass redundant parameters

DanilaFe pushed to main at DanilaFe/agda-spa

2024-03-09 14:10:48 -08:00

56c72e1388 Delete unused homomorphism proof that was broken by an Agda update.

0c30f8be48 Start on sign analysis (mostly just imports)

75f981cb75 Define simple sequential-only programs

ca99e18184 Tweak exports from finite value bundle to avoid (some) redundant arguments

702cf2c298 Expose more functionaity from the set lattice

Compare 9 commits »

DanilaFe pushed to main at DanilaFe/agda-spa

2024-03-07 21:54:32 -08:00

332b7616cf Prove that foldr is monotonic when input lists are pairwise monotonic

7905d106e2 Tweak signature of 'forget' to simplify proofs

34203840c8 Use the new provenance function to clean up some proofs

Compare 3 commits »

DanilaFe pushed to main at DanilaFe/agda-spa

2024-03-06 00:36:09 -08:00

48983c55b1 Prove exercise 4.26 from the textbook

fa0282ff6f Prove that the identity function is monotonic

Compare 2 commits »