Danila Fedorin DanilaFe
0 Followers · 0 Following
Repositories
11
 Projects Packages Code Public Activity Starred Repositories
DanilaFe pushed to master at Nix-Configs/server-config 2026-09-15 04:00:52 +00:00
43c0837a86 Update config with new blog versions
DanilaFe pushed to master at Nix-Configs/blog-static-flake 2026-09-15 03:54:57 +00:00
32a8e86c92 Update blog with new article
DanilaFe pushed to master at Web-Projects/blog-static 2026-09-15 03:54:02 +00:00
f4eb812572 Add another sidenote
87c7536f49 publish
ebd8073520 Add new article
Compare 3 commits »
DanilaFe pushed to master at Nix-Configs/server-config 2026-09-12 01:33:33 +00:00
8492e00680 Add, but don't enable, whatdo host
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-08-10 03:08:51 +00:00
53f8bd47dc Add function back in to Embedding
fd371ba175 Remove trace suffix from Reaching type
Compare 2 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-08-09 23:37:26 +00:00
df4d072f22 Clean up comments in Graphs.lean and Program.lean
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-08-09 23:00:22 +00:00
c0542d0811 Allow negative numbers in expressions
a19f9fa148 Get rid of Tagged
269906871f Update LICM/Reaching to node use NodeId
1eecf45c0f Add more machinery to use embeddings as "proofs of child-ship"
827d55c6b6 Switch embeddings to index-offset.
Compare 5 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-07-03 00:42:48 +00:00
904f6375be Consolidate per-operator trace lifting into GGraph.Embed + Trace.embed
8cd053a242 Migrate Reaching.lean to projections via a generic Trace.steps
Compare 2 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-07-02 03:58:46 +00:00
0e6976f9b4 Migrate most of the codebase (sans Reaching.lean / LICM left) to projections
10b8fa97ca Add left-and-right open traces to help formalization
8ed48cf444 Add non-state parameterized 'Reaches' relation
Compare 3 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-07-01 04:23:50 +00:00
37d88f070a Remove 'prog.code s = some bs' argument to eval
6c05e401c1 Document Program.lean
fe5098095a Reorganize proofs to make 'Program' accessible to files in Language/
59afbdaf71 Rename StateInterp to match the style of the rest of the codebase
490c472d22 Start documenting FiniteMap.lean
Compare 12 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-06-28 01:04:48 +00:00
86bc33ee26 Register cases rules on lattice carriers for aesop automation
9e0702b5f5 Replace AboveBelow lattice-axiom case bashes with aesop
445187837c Add Trace.concat notation and apply at call sites
1a49689edc Apply aesop to reduce proofs
b1b3b0d2fe Add more documentation
Compare 13 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-06-26 17:16:27 +00:00
a5f533d67a Use a direct N-way unzip instead of induction over product size
c281d78d1d Add documentation for IterProd
1a843747bf Delete unused code and moved some lemmas into Lattice.lean
352e0bb8cc Fold Isomorphism module into Lattice.lean
a12b6c0c3c Write more documentation
Compare 5 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-06-25 23:55:36 +00:00
cbad43efdc Make FiniteHeightLattice extend Lattice and derive Top/Bot
acef0f202b Add titles to documented modules
c2ad0db668 Update comments in Graph and make map be a Functor instance
a5235f6fbc Add documentation to some modules.
e2df847139 Adopt lemma as the default keyword
Compare 14 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-06-24 19:33:40 +00:00
9ab43b34ef Use mathlib definition of inverses for Isomorphism.lean
97a9150bf3 Simplify the strict-step extraction in LTSeries.exists_unzip
93f913a699 Clean up namespaces in the analysis framework
7fb9d9aa19 Clean up Lattice.lean's namespaces
Compare 4 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-06-23 20:12:09 +00:00
f23705a93e Add scoped quotation syntax for object-language programs
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-06-23 20:10:10 +00:00
30d2960fca Add scoped quotation syntax for object-language programs
b1dc725ced Apply some cleanups to Graphs.lean
ed88f4ce94 Use 'interp' to add [[ bla ]] notation for analysis
8ce6e5e4e4 Have LatticeInterpretation extend Interp
6afa7df444 Remove unused plus/minus mono_left/mono_right projections
Compare 10 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-06-23 01:36:29 +00:00
8c37a4c049 Lean: inline BoundedChains.no_longer into FixedHeight.bot_le
2ee32580a2 Lean migration cleanup: collapse FixedHeight struct into FiniteHeightLattice typeclass
Compare 2 commits »
DanilaFe pushed to fable-lean-migration at DanilaFe/agda-spa 2026-06-10 06:37:59 +00:00
b16f14fdfd Lean migration: typeclass-based parameter passing, as in the Agda original
b26d6b5acd Lean migration: final notes — Lean output verified identical to Agda
a82d54666a Lean migration: Phase 7 (Sign + Constant analyses, executable)
739fbb503c Lean migration: Phase 6 (forward analysis framework)
2cfd0a2fb7 Lean migration: Phase 5 (language, CFGs, traces, Program)
Compare 8 commits »
DanilaFe created branch fable-lean-migration in DanilaFe/agda-spa 2026-06-10 06:37:59 +00:00
DanilaFe pushed to pynchon at Web-Projects/blog-static 2026-05-31 05:43:21 +00:00
4918558893 Tweak styles to make things work nicely with "page-looking things"
25f8e31fd3 Finish draft
f92b8bcab1 Add initial draft of Pynchon before repurposing
Compare 3 commits »