Commit Graph

Select branches

Hide Pull Requests

main

Mono Color

• f0da9a9020 Move more code out of Sign and into Main Danila Fedorin 2024-03-11 13:07:42 -0700
• 040c13caba Use instances to simplify printing code Danila Fedorin 2024-03-11 12:50:05 -0700
• 56da61b339 Delete the bundles since they did not turn out all that useful Danila Fedorin 2024-03-11 12:14:53 -0700
• 3e88a64ed9 Add some debugging code to sign analysis to print the results Danila Fedorin 2024-03-10 22:23:45 -0700
• 8a85c4497c Prove that evaluation is monotonic and complete sign analysis Danila Fedorin 2024-03-10 21:25:46 -0700
• 8964ba59a1 Prove monotonicity of eval Danila Fedorin 2024-03-10 20:29:05 -0700
• 96f3ceaeb2 Use the previous join function directly in GeneralizedUpdate Danila Fedorin 2024-03-10 19:41:02 -0700
• 237250cf72 Stop using modules in 'Sign' analysis Danila Fedorin 2024-03-10 19:23:48 -0700
• 8515491327 Simplify AboveBelow a bit to avoid nested modules Danila Fedorin 2024-03-10 18:43:10 -0700
• 3305de4710 Remove need for explicit arguments in map derivatives Danila Fedorin 2024-03-10 18:35:29 -0700
• f21ebdcf46 Start working on the evaluation operation. Danila Fedorin 2024-03-10 18:13:01 -0700
• 0705df708e Prove that variables in a program all come from the program's code Danila Fedorin 2024-03-10 16:41:21 -0700
• 51accb6438 Define 'minus', too -- with no monotonicity proof. Danila Fedorin 2024-03-10 16:40:49 -0700
• afe5bac2dc Commit result of (unsuccessfully) trying to prove monotonicity of plus. Danila Fedorin 2024-03-10 13:54:19 -0700
• fdc40632bf Add a way to retrieve the code for a particular state Danila Fedorin 2024-03-09 23:09:50 -0800
• f84a1c923c Prove that the 'join' transformation is monotonic Danila Fedorin 2024-03-09 23:06:47 -0800
• 1b1b80465c Use named modules to avoid having to pass redundant parameters Danila Fedorin 2024-03-09 21:46:15 -0800
• 56c72e1388 Delete unused homomorphism proof that was broken by an Agda update. Danila Fedorin 2024-03-09 14:07:56 -0800
• 0c30f8be48 Start on sign analysis (mostly just imports) Danila Fedorin 2024-03-09 14:00:10 -0800
• 75f981cb75 Define simple sequential-only programs Danila Fedorin 2024-03-09 13:59:48 -0800
• ca99e18184 Tweak exports from finite value bundle to avoid (some) redundant arguments Danila Fedorin 2024-03-09 13:59:22 -0800
• 702cf2c298 Expose more functionaity from the set lattice Danila Fedorin 2024-03-09 13:58:40 -0800
• 0c088ca2ae Prove multi-key access monotonicity in finite maps Danila Fedorin 2024-03-09 13:58:07 -0800
• bc138d87f0 Prove things about key-based access in map Danila Fedorin 2024-03-09 13:57:29 -0800
• 311ed75186 Expose more helpers from 'Map' Danila Fedorin 2024-03-09 13:57:02 -0800
• 1ccc6f08e5 Add more properties of uniqueness Danila Fedorin 2024-03-09 13:54:01 -0800
• 332b7616cf Prove that foldr is monotonic when input lists are pairwise monotonic Danila Fedorin 2024-03-07 21:53:45 -0800
• 7905d106e2 Tweak signature of 'forget' to simplify proofs Danila Fedorin 2024-03-07 20:04:33 -0800
• 34203840c8 Use the new provenance function to clean up some proofs Danila Fedorin 2024-03-07 19:59:14 -0800
• 48983c55b1 Prove exercise 4.26 from the textbook Danila Fedorin 2024-03-06 00:35:29 -0800
• fa0282ff6f Prove that the identity function is monotonic Danila Fedorin 2024-03-06 00:35:06 -0800
• 164fc3636f Prove that constant functions are monotonic Danila Fedorin 2024-03-03 17:23:57 -0800
• c932210d37 Re-expert monotonicity from Lattice Danila Fedorin 2024-03-03 17:04:18 -0800
• a8d26b1c48 Prove that join is monotonic in both arguments Danila Fedorin 2024-03-03 16:51:57 -0800
• 2ddac38c3f Update with new changes to Agda Danila Fedorin 2024-03-03 16:44:10 -0800
• f00dabfc93 More cleanup to FiniteValueMap Danila Fedorin 2024-03-02 16:15:20 -0800
• 01f4e02026 More cleanup to FiniteValueMap Danila Fedorin 2024-03-02 16:05:42 -0800
• fbbcd72037 Some early refactors of FiniteValueMap Danila Fedorin 2024-03-02 15:18:10 -0800
• 03cdc65a7b Format AboveBelow a bit better (round two) Danila Fedorin 2024-03-02 14:56:04 -0800
• ec2b1ec3ba Format FiniteMap a little bit better Danila Fedorin 2024-03-02 14:54:44 -0800
• 112dcb2208 Clean up AboveBelow slightly Danila Fedorin 2024-03-02 14:34:15 -0800
• 8516f58b1d Remove helper comment. Danila Fedorin 2024-03-02 14:13:02 -0800
• 6cb6281bc2 Make main run the fixed point algorithm Danila Fedorin 2024-03-01 23:42:10 -0800
• 0774946211 Expose decidability from Map modules Danila Fedorin 2024-03-01 23:27:49 -0800
• 65d1590358 Prove monotonicity of lub in one argument Danila Fedorin 2024-03-01 23:26:25 -0800
• ae3e2c28b0 Create bundles and add a program to evaluate some code with finite maps Danila Fedorin 2024-03-01 21:58:58 -0800
• 97a4165b58 Expose bundles from FiniteValueMap Danila Fedorin 2024-03-01 21:35:40 -0800
• 754714d770 Restore bundles in IterProd Danila Fedorin 2024-03-01 21:12:22 -0800
• ae09a27f64 Prove that finite value-maps are finite height Danila Fedorin 2024-03-01 21:03:23 -0800
• ca90f6509c Re-write the IterProd proofs to couple lattice and finite height lattice Danila Fedorin 2024-03-01 21:02:56 -0800
• 29898e738b Clean up a bit Danila Fedorin 2024-03-01 19:08:29 -0800
• 3a537f54ba Add a helpful utility function Danila Fedorin 2024-03-01 19:08:11 -0800
• 52e7a7a208 Prove distributivity in the other direction, too Danila Fedorin 2024-03-01 19:07:59 -0800
• 8715d6d89c Finish proof of from distributivity Danila Fedorin 2024-02-26 00:00:18 -0800
• b083561629 Add most of the proof of from distributivity. Danila Fedorin 2024-02-25 20:28:07 -0800
• 3ad7db738a Prove that 'to' preserves equality Danila Fedorin 2024-02-25 18:43:54 -0800
• 53a08b8f79 Prove that 'first' presrves equality Danila Fedorin 2024-02-25 18:08:03 -0800
• d6064ff752 Expose 'locate' and 'forget' from Map Danila Fedorin 2024-02-25 18:07:50 -0800
• d280f5afdf Make auxillary definitions private Danila Fedorin 2024-02-25 14:06:45 -0800
• b96bac5518 Prove the other direction for inverses. Danila Fedorin 2024-02-25 13:57:45 -0800
• 99fc21cef2 Expose 'subset-impl' from Map Danila Fedorin 2024-02-25 13:57:28 -0800
• 2a06e6ae2d Adjust 'to' to make it easier to reason about Danila Fedorin 2024-02-25 12:17:19 -0800
• 671ffc82df Define to-and-from functions from finite maps to tuples and prove one inverse direction Danila Fedorin 2024-02-19 14:50:29 -0800
• 486b552b59 Try to generalize universe levels where possible Danila Fedorin 2024-02-19 12:36:46 -0800
• aafcb2683d Prove the transport of 'height lattice' property given an isomorphism Danila Fedorin 2024-02-18 23:26:41 -0800
• 8c9f39ac35 Add some additional 'equivalence' definitions to Equivalence Danila Fedorin 2024-02-18 21:46:42 -0800
• 6384f7006e Make 'lattice' public Danila Fedorin 2024-02-18 20:18:38 -0800
• b1c6b4c99a Expose bundles from Unit Danila Fedorin 2024-02-11 21:20:05 -0800
• 5420bb808e Expose bundles from 'Prod' Danila Fedorin 2024-02-11 21:16:41 -0800
• 4c0860f4c7 Expose bundle form MapSet Danila Fedorin 2024-02-11 21:14:49 -0800
• e89418d600 Expose bundle form 'Map' Danila Fedorin 2024-02-11 21:12:49 -0800
• bfb32092c2 Expose bundles and apply so renames to IterProd Danila Fedorin 2024-02-11 21:10:51 -0800
• 6e26aa1580 Add a bundle to FiniteMap Danila Fedorin 2024-02-11 21:02:43 -0800
• 27f40bd42e Add bundles to 'AboveBelow' Danila Fedorin 2024-02-11 21:00:28 -0800
• 08f3f49640 Rename some definitions in Nat and expose bundle Danila Fedorin 2024-02-11 20:56:21 -0800
• a920608bef Tweak IterProd to expose more (including a bundle) Danila Fedorin 2024-02-11 20:45:14 -0800
• 45f2babfa3 Fix typo in FixedHeightLattice definition Danila Fedorin 2024-02-11 15:37:00 -0800
• 16c4d13242 Prove that iterated products are finite height Danila Fedorin 2024-02-11 15:36:12 -0800
• 0ba4b46e16 Add proof of decidable equivalence for products Danila Fedorin 2024-02-11 15:35:50 -0800
• 7e5cc1b316 Add an 'iterated product' lattice for A x A ... x A x B. Danila Fedorin 2024-02-11 14:18:58 -0800
• 33b7bc37f0 Add a 'FiniteHeightLattice' bundle Danila Fedorin 2024-02-11 14:17:49 -0800
• 6fe8dc2a02 Add an 'iterate' function to Utils Danila Fedorin 2024-02-11 14:16:42 -0800
• ec31333e9a Add a 'Finite Map' lattice Danila Fedorin 2024-02-11 13:19:46 -0800
• ad26d20274 Add facts about equal-key maps Danila Fedorin 2024-02-11 12:45:43 -0800
• 2b27e397b6 Add another utility proof Danila Fedorin 2024-02-11 12:45:33 -0800
• d718338759 Clean up 'Map' to hide implementation details, extract code Danila Fedorin 2024-02-10 16:51:43 -0800
• 1b8c88b1a2 Expose only a 'public' "keys" function from Map Danila Fedorin 2024-02-10 16:35:21 -0800
• a55c786a51 Tentatively start working on a language to analyze Danila Fedorin 2024-02-07 22:51:08 -0800
• 512cd22be5 Fix definition of 'less than' to not involve a third variable. Danila Fedorin 2024-02-07 21:04:13 -0800
• 9646096c75 Fix uses of 'absurd' in Fixedpoint.agda Danila Fedorin 2023-11-23 14:15:40 -0800
• bf74b35c14 Add proof of Lattice preservation Danila Fedorin 2023-09-29 21:19:48 -0700
• 7b24bae29a Start on the homomorphism / isomorphism proofs Danila Fedorin 2023-09-29 20:45:13 -0700
• 3c346dcd15 Add a 'set' lattice backed by maps Danila Fedorin 2023-09-23 17:12:12 -0700
• 4a90a57388 Clean up imports a bit Danila Fedorin 2023-09-23 16:39:11 -0700
• 6cd37a212f Move the product instances into its own file Danila Fedorin 2023-09-23 16:34:30 -0700
• 8eaec3facd Provide a 'fixed height' predicate from Lattice for convenience Danila Fedorin 2023-09-23 16:20:58 -0700
• dce21b3696 Moved the Nat lattice instance into an actual file Danila Fedorin 2023-09-23 15:34:59 -0700
• 5d54e62c3a Move the lattice etc. instances into Lattice.Map Danila Fedorin 2023-09-23 15:08:04 -0700
• 845a8a2236 Move the Map into Lattice/Map Danila Fedorin 2023-09-23 15:06:43 -0700
• f27dec8904 Add proof of fixed-height chain Danila Fedorin 2023-09-23 12:33:48 -0700