Danila Fedorin

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"

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 »