diff --git a/resume.html b/resume.html
index 1927b94..bb7a7e4 100644
--- a/resume.html
+++ b/resume.html
@@ -160,6 +160,33 @@
                     </div>
                 </div>
             </section>
+            <!--
+            <section>
+                <h1>Programming Languages & Formal Methods</h1>
+                <div class="section-content">
+                    <div class="position">
+                        <h2><a class="project-link" href="https://dev.danilafe.com/DanilaFe/agda-spa">agda-spa<i data-feather="link" class="project-link-icon"></i></a></h2>
+                        <ul>
+                            <li>Designed and implemented a lattice-based static analysis framework in <em class="bold">Agda</em> using monotone transfer functions.</li>
+                            <li>Built reusable architecture for constructing <em class="bold">dataflow analyses</em> over arbitrary finite-height lattices.</li>
+                            <li>Devised mechanism for verifying analyses via a correspondence between <em class="bold">control-flow graphs</em> and <em class="bold">program semantics</em>.</li>
+                            <li>Compositionally proved lattice constructions for types such as maps, sets, and tuples.</li>
+                            <li>Documented the framework in depth in <a href="https://danilafe.com/series/static-program-analysis-in-agda/">a series of posts</a> on personal blog.</li>
+                        </ul>
+                    </div>
+
+                    <div class="position">
+                        <h2><a class="project-link" href="https://github.com/DanilaFe/maypop">maypop<i data-feather="link" class="project-link-icon"></i></a></h2>
+                        <ul>
+                            <li>Implemented a dependently typed functional programming language supporting inductive types and formal proofs.</li>
+                            <li>Built typechecker, evaluator, and module system, integrated with documentation using Literate <em class="bold">Haskell</em></li>
+                            <li>Developed logic-programming-style proof search and unification for dependently-typed terms.</li>
+                            <li>Leveraged a monad-transformer-based architecture for extensible effects and testable components.</li>
+                        </ul>
+                    </div>
+                </div>
+            </section>
+            -->
             <section>
                 <h1>Publications</h1>