Danila Fedorin

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 »

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 »