Danila Fedorin DanilaFe
0 Followers · 0 Following
Repositories
11
 Projects Packages Code Public Activity Starred Repositories
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 »
DanilaFe created branch pynchon in Web-Projects/blog-static 2026-05-31 05:43:20 +00:00
DanilaFe pushed to main at Web-Projects/blog-versions 2026-05-20 01:33:53 +00:00
9af115e403 Update to latest blog and update image for fixed code in SPA part 6
DanilaFe pushed to master at Nix-Configs/blog-static-flake 2026-05-20 00:57:00 +00:00
4481c38cf3 Update blog
DanilaFe pushed to master at Web-Projects/blog-static 2026-05-20 00:56:11 +00:00
98e2e7da6c Update theme with i18n stuff
DanilaFe pushed to master at Web-Projects/vanilla-hugo 2026-05-20 00:55:35 +00:00
b1b5408301 Pull more text into translation
DanilaFe pushed to master at Web-Projects/blog-static 2026-05-20 00:07:04 +00:00
f57e3d370b Bump theme version
8795003ce7 Fix submodule links in SPA part 6 which got out of sync with the code
Compare 2 commits »
DanilaFe pushed to master at Web-Projects/vanilla-hugo 2026-05-20 00:06:47 +00:00
d206ed9f3e Bump Hugo version