This website requires JavaScript.
Explore
Help
Sign In
Danila Fedorin
DanilaFe
0 Followers
·
0 Following
Portland, OR
https://danilafe.com
Joined on
2017-09-08
Block a user
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.
User to block:
Optional note:
The note is not visible to the blocked user.
Cancel
Block
Repositories
11
Projects
Packages
Code
Public Activity
Starred Repositories
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 »
DanilaFe
pushed to
main
at
DanilaFe/agda-spa
2024-02-11 15:39:47 -08:00
45f2babfa3
Fix typo in FixedHeightLattice definition
16c4d13242
Prove that iterated products are finite height
0ba4b46e16
Add proof of decidable equivalence for products
7e5cc1b316
Add an 'iterated product' lattice for A x A ... x A x B.
33b7bc37f0
Add a 'FiniteHeightLattice' bundle
Compare 11 commits »
DanilaFe
pushed to
master
at
DanilaFe/dotfiles
2024-02-10 14:33:52 -08:00
e6eb69e31b
Merge remote-tracking branch 'origin/master'
4bf96b1296
Add more vim config changes
Compare 2 commits »
DanilaFe
pushed to
master
at
DanilaFe/dotfiles
2024-02-10 14:31:00 -08:00
3e6a62b798
Configure CLS and chplcheck
First
Previous
...
14
15
16
17
18
...
Next
Last