Add Agda SPA to resume
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
aa46087fe2
commit
c08aba8c92
@ -45,6 +45,13 @@
|
|||||||
<section>
|
<section>
|
||||||
<h1>Projects</h1>
|
<h1>Projects</h1>
|
||||||
<div class="section-content">
|
<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> —
|
||||||
|
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">
|
<div class="project-container">
|
||||||
<a class="project-link" href="https://github.com/DanilaFe/abcs">
|
<a class="project-link" href="https://github.com/DanilaFe/abcs">
|
||||||
@ -85,6 +92,7 @@
|
|||||||
Compiler from a small imperative language into CHIP-8 bytecode.
|
Compiler from a small imperative language into CHIP-8 bytecode.
|
||||||
</div>
|
</div>
|
||||||
-->
|
-->
|
||||||
|
<!--
|
||||||
<div class="project-container">
|
<div class="project-container">
|
||||||
<a class="project-link" href="https://github.com/DanilaFe/pegasus">
|
<a class="project-link" href="https://github.com/DanilaFe/pegasus">
|
||||||
<h2>pegasus</h2>
|
<h2>pegasus</h2>
|
||||||
@ -92,6 +100,7 @@
|
|||||||
</a> —
|
</a> —
|
||||||
LALR parser generator currently supporting the C and Crystal languages.
|
LALR parser generator currently supporting the C and Crystal languages.
|
||||||
</div>
|
</div>
|
||||||
|
-->
|
||||||
<!--
|
<!--
|
||||||
<div class="project-container">
|
<div class="project-container">
|
||||||
<a class="project-link" href="https://github.com/DanilaFe/Scylla">
|
<a class="project-link" href="https://github.com/DanilaFe/Scylla">
|
||||||
|
Loading…
Reference in New Issue
Block a user