Danila Fedorin DanilaFe
0 Followers · 0 Following
Repositories
11
 Projects Packages Code Public Activity Starred Repositories
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 »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-03-03 17:38:29 -08:00
164fc3636f Prove that constant functions are monotonic
c932210d37 Re-expert monotonicity from Lattice
a8d26b1c48 Prove that join is monotonic in both arguments
2ddac38c3f Update with new changes to Agda
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-03-02 16:24:14 -08:00
f00dabfc93 More cleanup to FiniteValueMap
01f4e02026 More cleanup to FiniteValueMap
fbbcd72037 Some early refactors of FiniteValueMap
03cdc65a7b Format AboveBelow a bit better (round two)
ec2b1ec3ba Format FiniteMap a little bit better
Compare 7 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-03-01 23:46:27 -08:00
6cb6281bc2 Make main run the fixed point algorithm
0774946211 Expose decidability from Map modules
65d1590358 Prove monotonicity of lub in one argument
ae3e2c28b0 Create bundles and add a program to evaluate some code with finite maps
97a4165b58 Expose bundles from FiniteValueMap
Compare 5 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-03-01 21:14:52 -08:00
754714d770 Restore bundles in IterProd
DanilaFe pushed to main at DanilaFe/agda-spa 2024-03-01 21:04:04 -08:00
ae09a27f64 Prove that finite value-maps are finite height
ca90f6509c Re-write the IterProd proofs to couple lattice and finite height lattice
29898e738b Clean up a bit
3a537f54ba Add a helpful utility function
52e7a7a208 Prove distributivity in the other direction, too
Compare 5 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-26 00:00:31 -08:00
8715d6d89c Finish proof of from distributivity
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-25 20:29:10 -08:00
b083561629 Add most of the proof of from distributivity.
3ad7db738a Prove that 'to' preserves equality
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-25 18:08:33 -08:00
53a08b8f79 Prove that 'first' presrves equality
d6064ff752 Expose 'locate' and 'forget' from Map
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-25 14:13:24 -08:00
d280f5afdf Make auxillary definitions private
b96bac5518 Prove the other direction for inverses.
99fc21cef2 Expose 'subset-impl' from Map
2a06e6ae2d Adjust 'to' to make it easier to reason about
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-19 22:58:11 -08:00
671ffc82df Define to-and-from functions from finite maps to tuples and prove one inverse direction
486b552b59 Try to generalize universe levels where possible
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-18 23:27:05 -08:00
aafcb2683d Prove the transport of 'height lattice' property given an isomorphism
8c9f39ac35 Add some additional 'equivalence' definitions to Equivalence
6384f7006e Make 'lattice' public
Compare 3 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-11 21:21:27 -08:00
b1c6b4c99a Expose bundles from Unit
5420bb808e Expose bundles from 'Prod'
4c0860f4c7 Expose bundle form MapSet
e89418d600 Expose bundle form 'Map'
bfb32092c2 Expose bundles and apply so renames to IterProd
Compare 9 commits »