- Portland, OR
- https://danilafe.com
- Joined on
2017-09-08
Block a user
7d2842fd64
Add article about the 'deeply embedded expression' pattern
cd4c121e07
Update the theme
d0570f876e
Add the SPA code as a submodule
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
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
fdc40632bf
Add a way to retrieve the code for a particular state
f84a1c923c
Prove that the 'join' transformation is monotonic
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
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
48983c55b1
Prove exercise 4.26 from the textbook
fa0282ff6f
Prove that the identity function is monotonic
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
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
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
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
b083561629
Add most of the proof of from distributivity.
3ad7db738a
Prove that 'to' preserves equality