Add commits and reformat index

janpaulpl · Jan 29, 2024 · 8693bc2 · 8693bc2
1 parent c3268fa
commit 8693bc2
Show file tree

Hide file tree

Showing 11 changed files with 125 additions and 27 deletions.
diff --git a/_data/navigation.yml b/_data/navigation.yml
@@ -1,4 +1,6 @@
 - name: About Me
   link: /
 - name: Publications
-  link: /pubs.html
+  link: /pubs.html
+- name: Commits
+  link: /commits.html
diff --git a/_site/404.html b/_site/404.html
@@ -27,6 +27,8 @@ <h1><a href="/">Jan-Paul Vincent Ramos-Dávila</a></h1>
 
 
 
+
+
           </div>
         </div>
         <div class="contact-toggle-wrapper">
@@ -53,6 +55,13 @@ <h1><a href="/">Jan-Paul Vincent Ramos-Dávila</a></h1>
                   </a>
                 </li>
 
+                <li>
+                  <a href="/commits.html" 
+                    class="nav-item" >
+                    Commits
+                  </a>
+                </li>
+
                 <li>
                   <a href="http://localhost:4000/assets/pdfs/cv.pdf" class="nav-item" target=”_blank”>
                     Curriculum Vitae

diff --git a/_site/assets/pdfs/cv.pdf b/_site/assets/pdfs/cv.pdf
diff --git a/_site/assets/pdfs/popl_src24.pdf b/_site/assets/pdfs/popl_src24.pdf
diff --git a/_site/assets/posters/popl_src24_poster.pdf b/_site/assets/posters/popl_src24_poster.pdf
diff --git a/_site/blog.html → _site/commits.html b/_site/blog.html → _site/commits.html
@@ -27,6 +27,10 @@ <h1><a href="/">Jan-Paul Vincent Ramos-Dávila</a></h1>
 
 
 
+
+            <h2>Commits</h2>
+
+
           </div>
         </div>
         <div class="contact-toggle-wrapper">
@@ -53,6 +57,12 @@ <h1><a href="/">Jan-Paul Vincent Ramos-Dávila</a></h1>
                   </a>
                 </li>
 
+                <li>
+                  <a href="/commits.html"  class="nav-item nav-item-current" >
+                    Commits
+                  </a>
+                </li>
+
                 <li>
                   <a href="http://localhost:4000/assets/pdfs/cv.pdf" class="nav-item" target=”_blank”>
                     Curriculum Vitae
@@ -87,7 +97,31 @@ <h1><a href="/">Jan-Paul Vincent Ramos-Dávila</a></h1>
       <div class="flex-body">
         <div class="flex-content">
           <div class="flex-rendered">
-
+  <h1 id="my-commit-history">My commit history</h1>
+
+<p><i class="ri-git-commit-fill">
+<em>
+01.29.24. After a nice chat with Dr. Alwyn Goodloe, I’m going to start working with the Langley Formal Methods research program at NASA to formally verify network protocols!
+</em>
+</i></p>
+
+<p><i class="ri-git-commit-fill">
+<em>
+01.20.24. Just finished providing AV support for POPL’24. We put in a lot of effort into this one, you can checkout the talks <a href="https://www.youtube.com/@acmsigplan">here</a>. 
+</em>
+</i></p>
+
+<p><i class="ri-git-commit-fill">
+<em>
+01.18.24. I’m TAing Cornell’s undergrad PL course, my first time ever TAing a course ☺.
+</em>
+</i></p>
+
+<p><i class="ri-git-commit-fill">
+<em>
+01.01.24. Push my first commit.
+</em>
+</i></p>
 
 </div>
         </div>

diff --git a/_site/index.html b/_site/index.html
@@ -29,6 +29,8 @@ <h2>About Me</h2>
 
 
 
+
+
           </div>
         </div>
         <div class="contact-toggle-wrapper">
@@ -54,6 +56,13 @@ <h2>About Me</h2>
                   </a>
                 </li>
 
+                <li>
+                  <a href="/commits.html" 
+                    class="nav-item" >
+                    Commits
+                  </a>
+                </li>
+
                 <li>
                   <a href="http://localhost:4000/assets/pdfs/cv.pdf" class="nav-item" target=”_blank”>
                     Curriculum Vitae
@@ -114,15 +123,24 @@ <h2>About Me</h2>
   </div>
 </div>
 <div class="flex-rendered">
-  <h1 id="hi">Hi!</h1>
-<p>I’m a Junior at <a href="https://www.cornell.edu/">Cornell University</a> working towards degrees in <a href="https://cis.cornell.edu/">Computer Science</a> &amp; <a href="https://philosophy.cornell.edu/">Philosophy</a>. I started doing Computer Science research under <a href="https://www.cs.cornell.edu/~asampson/">Dr. Adrian Sampson</a> in the <a href="https://calyxir.org/">Calyx project</a>. We studied optimizations and extensions towards a compiler infrastructure to simplify encoding of high-level program semantics to lower-level synthesizable hardware designs.</p>
+  <h1 id="about">About</h1>
+<p>I’m a Junior at <a href="https://www.cornell.edu/">Cornell University</a> working towards degrees in <a href="https://cis.cornell.edu/">Computer Science</a> with a concentration in <a href="https://pl.cs.cornell.edu/">Programming Languages</a> &amp; <a href="https://philosophy.cornell.edu/">Philosophy</a> with a concentration in <a href="https://philosophy.cornell.edu/harold-theodore-hodes">Logic advised by Harold Hodes</a>.</p>
+
+<p>My main research interests involve developing practical tools for program and theorem verification using both formal &amp; lightweight methods.</p>
+
+<p>Recreationally, I’m an avid <em>cinephile</em> (I’m sorry) and <em>audiophile</em> (I’m sorry again), for which you can judge my tastes all you like by following the socials at the top right corner of this page.</p>
+
+<h2 id="research">Research</h2>
+
+<p>This summer, I’m excited to work with <a href="https://shemesh.larc.nasa.gov/people/aeg/">Dr. Alwyn Goodloe</a> in the <a href="https://shemesh.larc.nasa.gov/fm/index.html">Langley Formal Methods research program at NASA</a>. We’ll be using Coq to formally verify theorems proving the soundness of network protocols.</p>
+
+<p>Since before that, I’ve been working under <a href="https://www.cs.cmu.edu/~aldrich/">Dr. Jonathan Aldrich</a> at CMU thanks to the <a href="https://www.cmu.edu/scs/s3d/reuse/Research/index.html">REUSE</a> program. We are developing a <a href="http://www.cs.cmu.edu/~aldrich/papers/vmcai2018-gradual-verification.pdf">Gradual Verifier</a> which serves to bridge the gap between static and dynamic verification, by allowing incremental verification of a program. I’ve worked on the first ever gradual verification tool – <a href="https://arxiv.org/abs/2210.02428">Gradual C0</a> – and gradual verification in <a href="https://popl24.sigplan.org/details/prisc-2024-papers/2/Gradual-Verification-for-Smart-Contracts">blockchain programming languages</a>.</p>
 
-<p>My main research interests involve developing <strong>practical tools</strong> for software verification using both formal &amp; lightweight methods.</p>
+<p>Before that, I started doing Computer Science research under <a href="https://www.cs.cornell.edu/~asampson/">Dr. Adrian Sampson</a> in the <a href="https://calyxir.org/">Calyx project</a>. We studied optimizations and extensions towards a compiler infrastructure to simplify encoding of high-level program semantics to lower-level synthesizable hardware designs.</p>
 
-<h1 id="current-research">Current Research</h1>
-<p>Since the summer of 2022, I’ve been working under CMU’s <a href="https://www.cmu.edu/scs/s3d/reuse/Research/index.html">REUSE</a> program with <a href="https://www.cs.cmu.edu/~aldrich/">Dr. Jonathan Aldrich</a>. We’ve been working on a <a href="http://www.cs.cmu.edu/~aldrich/papers/vmcai2018-gradual-verification.pdf">Gradual Verifier</a> which serves to bridge the gap between static and dynamic verification, by allowing incremental verification of a program.</p>
+<h2 id="community">Community</h2>
 
-<p>My work under the Gradual Verification framework involves optimizing and <a href="https://www.youtube.com/watch?v=sIIwmw0z2Yg">verifying the soundness</a> of the first ever gradual verification tool – <a href="https://arxiv.org/abs/2210.02428">Gradual C0</a> – and bringing gradual verification to the domain of <a href="https://github.com/gradual-verification/gradual-TEAL">blockchain programming languages</a>.</p>
+<p>Outside of Cornell, I’m part of the Audio/Visual team for <a href="https://www.sigplan.org/Conferences/">SIGPLAN conferences</a>. While this is just volunteering work, I’ve come to put a considerable amount of time into it, so checkout the <a href="https://www.youtube.com/@acmsigplan">SIGPLAN YouTube Channel</a> if you’re interested in some cool PL videos!</p>
 
 <center>
 <img width="25%" src="assets/img/Tokuhiro_Kawai.jpg" />

diff --git a/_site/pubs.html b/_site/pubs.html
@@ -29,6 +29,8 @@ <h1><a href="/">Jan-Paul Vincent Ramos-Dávila</a></h1>
             <h2>Publications</h2>
 
 
+
+
           </div>
         </div>
         <div class="contact-toggle-wrapper">
@@ -54,6 +56,13 @@ <h2>Publications</h2>
                   </a>
                 </li>
 
+                <li>
+                  <a href="/commits.html" 
+                    class="nav-item" >
+                    Commits
+                  </a>
+                </li>
+
                 <li>
                   <a href="http://localhost:4000/assets/pdfs/cv.pdf" class="nav-item" target=”_blank”>
                     Curriculum Vitae
@@ -251,17 +260,8 @@ <h3 class="pub-title">Optimization of a Gradual Verifier: Lazy evaluation of Iso
 
 
 
-<a href="/assets/pdfs/popl_src24.pdf" class="pub-link-box">
-<i class="pub-link ri-article-line"></i>
-<p>PDF</p>
-</a>
-
 
 
-<a href="/assets/posters/popl_src24_poster.pdf" class="pub-link-box">
-<i class="ri-table-line"></i>
-<p>Poster</p>
-</a>
 
 
 

diff --git a/blog.md b/blog.md
diff --git a/commits.md b/commits.md
@@ -0,0 +1,30 @@
+---
+layout: default
+post: ./_includes/publication.html
+---
+
+# My commit history 
+
+<i class="ri-git-commit-fill">
+<em>
+01.29.24. After a nice chat with Dr. Alwyn Goodloe, I'm going to start working with the Langley Formal Methods research program at NASA to formally verify network protocols!
+</em>
+</i>
+
+<i class="ri-git-commit-fill">
+<em>
+01.20.24. Just finished providing AV support for POPL'24. We put in a lot of effort into this one, you can checkout the talks [here](https://www.youtube.com/@acmsigplan). 
+</em>
+</i>
+
+<i class="ri-git-commit-fill">
+<em>
+01.18.24. I'm TAing Cornell's undergrad PL course, my first time ever TAing a course ☺.
+</em>
+</i>
+
+<i class="ri-git-commit-fill">
+<em>
+01.01.24. Push my first commit.
+</em>
+</i>
diff --git a/index.md b/index.md
@@ -3,15 +3,24 @@ layout: about
 post: ./_includes/publication.html
 ---
 
-# Hi!
-I'm a Junior at [Cornell University](https://www.cornell.edu/) working towards degrees in [Computer Science](https://cis.cornell.edu/) & [Philosophy](https://philosophy.cornell.edu/). I started doing Computer Science research under [Dr. Adrian Sampson](https://www.cs.cornell.edu/~asampson/) in the [Calyx project](https://calyxir.org/). We studied optimizations and extensions towards a compiler infrastructure to simplify encoding of high-level program semantics to lower-level synthesizable hardware designs.
+# About
+I'm a Junior at [Cornell University](https://www.cornell.edu/) working towards degrees in [Computer Science](https://cis.cornell.edu/) with a concentration in [Programming Languages](https://pl.cs.cornell.edu/) & [Philosophy](https://philosophy.cornell.edu/) with a concentration in [Logic advised by Harold Hodes](https://philosophy.cornell.edu/harold-theodore-hodes).
 
-My main research interests involve developing **practical tools** for software verification using both formal & lightweight methods. 
+My main research interests involve developing practical tools for program and theorem verification using both formal & lightweight methods.
 
-# Current Research
-Since the summer of 2022, I've been working under CMU's [REUSE](https://www.cmu.edu/scs/s3d/reuse/Research/index.html) program with [Dr. Jonathan Aldrich](https://www.cs.cmu.edu/~aldrich/). We've been working on a [Gradual Verifier](http://www.cs.cmu.edu/~aldrich/papers/vmcai2018-gradual-verification.pdf) which serves to bridge the gap between static and dynamic verification, by allowing incremental verification of a program. 
+Recreationally, I'm an avid *cinephile* (I'm sorry) and *audiophile* (I'm sorry again), for which you can judge my tastes all you like by following the socials at the top right corner of this page.
 
-My work under the Gradual Verification framework involves optimizing and [verifying the soundness](https://www.youtube.com/watch?v=sIIwmw0z2Yg) of the first ever gradual verification tool -- [Gradual C0](https://arxiv.org/abs/2210.02428) -- and bringing gradual verification to the domain of [blockchain programming languages](https://github.com/gradual-verification/gradual-TEAL).
+## Research 
+
+This summer, I'm excited to work with [Dr. Alwyn Goodloe](https://shemesh.larc.nasa.gov/people/aeg/) in the [Langley Formal Methods research program at NASA](https://shemesh.larc.nasa.gov/fm/index.html). We'll be using Coq to formally verify theorems proving the soundness of network protocols.
+
+Since before that, I've been working under [Dr. Jonathan Aldrich](https://www.cs.cmu.edu/~aldrich/) at CMU thanks to the [REUSE](https://www.cmu.edu/scs/s3d/reuse/Research/index.html) program. We are developing a [Gradual Verifier](http://www.cs.cmu.edu/~aldrich/papers/vmcai2018-gradual-verification.pdf) which serves to bridge the gap between static and dynamic verification, by allowing incremental verification of a program. I've worked on the first ever gradual verification tool -- [Gradual C0](https://arxiv.org/abs/2210.02428) -- and gradual verification in [blockchain programming languages](https://popl24.sigplan.org/details/prisc-2024-papers/2/Gradual-Verification-for-Smart-Contracts).
+
+Before that, I started doing Computer Science research under [Dr. Adrian Sampson](https://www.cs.cornell.edu/~asampson/) in the [Calyx project](https://calyxir.org/). We studied optimizations and extensions towards a compiler infrastructure to simplify encoding of high-level program semantics to lower-level synthesizable hardware designs.
+
+## Community
+
+Outside of Cornell, I'm part of the Audio/Visual team for [SIGPLAN conferences](https://www.sigplan.org/Conferences/). While this is just volunteering work, I've come to put a considerable amount of time into it, so checkout the [SIGPLAN YouTube Channel](https://www.youtube.com/@acmsigplan) if you're interested in some cool PL videos!
 
 <center>
 <img width="25%" src="assets/img/Tokuhiro_Kawai.jpg">