Danila Fedorin DanilaFe
0 Followers · 0 Following
Repositories
11
 Projects Packages Code Public Activity Starred Repositories
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2024-04-20 14:08:33 -07:00
6a952f8a15 Reduce gas for proof search
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-13 23:44:33 -07:00
2f91ca113e Make 'MonotonicPredicate' into another typeclass
7571cb7451 Extract 'monotonic state' into its own module
fc27b045d3 Remove nested module from Graphs
Compare 3 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-13 18:43:00 -07:00
de956cdc6a Split the Language file into modules
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-13 15:30:32 -07:00
7ed7f20227 Add missing edge
163108b9b3 Add precedence to some language constructs
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-04-13 14:13:53 -07:00
8dc5c40eae Get everything compiling
44f04e4020 Get forward analysis working again
4fe0d147fa Adjust 'Program' to have a graph and basic blocks
ba1c9b3ec8 Remove sketch if proof since the proof is done
b6e357787f Add proof about 'both' and pairing
Compare 10 commits »
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 »