Add more explicit 'formal methods' section

This commit is contained in:
2026-04-16 18:21:02 -07:00
parent f22cb5b795
commit 656e4411b2

View File

@@ -160,6 +160,33 @@
</div> </div>
</div> </div>
</section> </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> <section>
<h1>Publications</h1> <h1>Publications</h1>