Add Agda SPA to resume

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

resume.html

@@ -45,6 +45,13 @@
             <section>
                 <h1>Projects</h1>
                 <div class="section-content">
+                    <div class="project-container">
+                        <a class="project-link" href="https://dev.danilafe.com/DanilaFe/agda-spa">
+                            <h2>agda-spa</h2>
+                            <i data-feather="link" class="project-link-icon"></i>
+                        </a> &mdash;
+                        Framework for formally-verified lattice-based program analysis in Agda, explained in-depth in <a href="https://danilafe.com/series/static-program-analysis-in-agda/">a series of posts</a>.
+                    </div>
                     <!--
                     <div class="project-container">
                         <a class="project-link" href="https://github.com/DanilaFe/abcs">
@@ -85,6 +92,7 @@
                         Compiler from a small imperative language into CHIP-8 bytecode.
                     </div>
                     -->
+                    <!--
                     <div class="project-container">
                         <a class="project-link" href="https://github.com/DanilaFe/pegasus">
                             <h2>pegasus</h2>
@@ -92,6 +100,7 @@
                         </a> &mdash;
                         LALR parser generator currently supporting the C and Crystal languages.
                     </div>
+                    -->
                     <!--
                     <div class="project-container">
                         <a class="project-link" href="https://github.com/DanilaFe/Scylla">
@@ -131,7 +140,8 @@
                         <ul>
                             <li>Added support for compile-time reflection, various language features, and full scope resolution to compiler written in <em class="bold">C++</em>.</li>
                             <li>Led development of <em class="bold">Python</em> bindings for compiler, accelerating development of a linter and a language server by over 10x.</li>
-                            <li>Designed and implemented <em class="bold">a type-safe error reporting API</em>, improving developer experience and compiler error messages.</li>
+                            <li>Leveraged profiling information to improve performance of scope resolution compiler pass by 30%.</li>
+                            <li>Designed <em class="bold">a type-safe error reporting API</em>, improving developer experience and enabling 100+ custom error messages.</li>
                             <li>Supported community growth by designing, launching, and authoring articles for the <a href="https://chapel-lang.org/blog/posts/welcome">Chapel language technical blog.</a></li>
                             <li>Laid groundwork for compatibility with leading-edge supercomputers by implementing initial <em class="bold">AMD GPU
                                 programming support</em> using <em class="bold">Clang</em> and <em class="bold">ROCm</em> tooling.</li>
@@ -147,7 +157,7 @@
                             <li>Developed tooling in <em class="bold">Haskell</em> to interpret, verify, generate, and debug programming languages.</li>
                             <li>Contributed to <em class="bold">research papers</em> published to the GPCE and VL/HCC.</li>
                             <li>Proctored <em class="bold">quizzes and exams</em> for over 200 students.</li>
-                            <li>Aided students in implementing a final project in the form of a <em class="bold">custom programming language</em>.</li>
+                            <!-- <li>Aided students in implementing a final project in the form of a <em class="bold">custom programming language</em>.</li> -->
                             <li>Suggested and organized <em class="bold">independent review sessions</em> attended by over 70 students, with
                                 50% attendance growth between sessions.</li>
                         </ul>