diff --git a/_data/navigation.yml b/_data/navigation.yml index 089b67d4..8957e431 100644 --- a/_data/navigation.yml +++ b/_data/navigation.yml @@ -1,4 +1,6 @@ - name: About Me link: / - name: Publications - link: /pubs.html \ No newline at end of file + link: /pubs.html +- name: Commits + link: /commits.html \ No newline at end of file diff --git a/_site/404.html b/_site/404.html index e6f595a2..a8516b13 100644 --- a/_site/404.html +++ b/_site/404.html @@ -27,6 +27,8 @@

Jan-Paul Vincent Ramos-Dávila

+ +
@@ -53,6 +55,13 @@

Jan-Paul Vincent Ramos-Dávila

+
  • + + Commits + +
    • +
  • Curriculum Vitae diff --git a/_site/assets/pdfs/cv.pdf b/_site/assets/pdfs/cv.pdf index 98a6ba9c..5b8612c1 100644 Binary files a/_site/assets/pdfs/cv.pdf and b/_site/assets/pdfs/cv.pdf differ diff --git a/_site/assets/pdfs/popl_src24.pdf b/_site/assets/pdfs/popl_src24.pdf deleted file mode 100644 index d96b470a..00000000 Binary files a/_site/assets/pdfs/popl_src24.pdf and /dev/null differ diff --git a/_site/assets/posters/popl_src24_poster.pdf b/_site/assets/posters/popl_src24_poster.pdf deleted file mode 100644 index 8d305da8..00000000 Binary files a/_site/assets/posters/popl_src24_poster.pdf and /dev/null differ diff --git a/_site/blog.html b/_site/commits.html similarity index 79% rename from _site/blog.html rename to _site/commits.html index a78986dd..46b2a907 100644 --- a/_site/blog.html +++ b/_site/commits.html @@ -27,6 +27,10 @@

    Jan-Paul Vincent Ramos-Dávila

    + +

    Commits

    + +
    • @@ -53,6 +57,12 @@

    Jan-Paul Vincent Ramos-Dávila

    +
  • + + Commits + +
    • +
  • Curriculum Vitae @@ -87,7 +97,31 @@

    Jan-Paul Vincent Ramos-Dávila

    - +

    My commit history

    + +

    + +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! + +

    + +

    + +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. + +

    + +

    + +01.18.24. I’m TAing Cornell’s undergrad PL course, my first time ever TAing a course ☺. + +

    + +

    + +01.01.24. Push my first commit. + +

    diff --git a/_site/index.html b/_site/index.html index d1988c27..697f19b4 100644 --- a/_site/index.html +++ b/_site/index.html @@ -29,6 +29,8 @@

    About Me

    + +
    • @@ -54,6 +56,13 @@

    About Me

    +
  • + + Commits + +
    • +
  • Curriculum Vitae @@ -114,15 +123,24 @@

    About Me

    • -

    Hi!

    -

    I’m a Junior at Cornell University working towards degrees in Computer Science & Philosophy. I started doing Computer Science research under Dr. Adrian Sampson in the Calyx project. 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 working towards degrees in Computer Science with a concentration in Programming Languages & Philosophy with a concentration in Logic advised by Harold Hodes.

    + +

    My main research interests involve developing practical tools for program and theorem verification using both formal & lightweight methods.

    + +

    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.

    + +

    Research

    + +

    This summer, I’m excited to work with Dr. Alwyn Goodloe in the Langley Formal Methods research program at NASA. 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 at CMU thanks to the REUSE program. We are developing a Gradual Verifier 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 – and gradual verification in blockchain programming languages.

    -

    My main research interests involve developing practical tools for software verification using both formal & lightweight methods.

    +

    Before that, I started doing Computer Science research under Dr. Adrian Sampson in the Calyx project. We studied optimizations and extensions towards a compiler infrastructure to simplify encoding of high-level program semantics to lower-level synthesizable hardware designs.

    -

    Current Research

    -

    Since the summer of 2022, I’ve been working under CMU’s REUSE program with Dr. Jonathan Aldrich. We’ve been working on a Gradual Verifier which serves to bridge the gap between static and dynamic verification, by allowing incremental verification of a program.

    +

    Community

    -

    My work under the Gradual Verification framework involves optimizing and verifying the soundness of the first ever gradual verification tool – Gradual C0 – and bringing gradual verification to the domain of blockchain programming languages.

    +

    Outside of Cornell, I’m part of the Audio/Visual team for SIGPLAN 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 if you’re interested in some cool PL videos!

    diff --git a/_site/pubs.html b/_site/pubs.html index f9ebd2b9..3f1a6f1f 100644 --- a/_site/pubs.html +++ b/_site/pubs.html @@ -29,6 +29,8 @@

    Jan-Paul Vincent Ramos-Dávila

    Publications

    + +
    @@ -54,6 +56,13 @@

    Publications

    +
  • + + Commits + +
    • +
  • Curriculum Vitae @@ -251,17 +260,8 @@

    Optimization of a Gradual Verifier: Lazy evaluation of Iso - - -

    PDF

    -     - - - -

    Poster

    -     diff --git a/blog.md b/blog.md deleted file mode 100644 index 75a235c5..00000000 --- a/blog.md +++ /dev/null @@ -1,4 +0,0 @@ ---- -layout: default -post: ./_includes/publication.html ---- \ No newline at end of file diff --git a/commits.md b/commits.md new file mode 100644 index 00000000..601c8b89 --- /dev/null +++ b/commits.md @@ -0,0 +1,30 @@ +--- +layout: default +post: ./_includes/publication.html +--- + +# My commit history + + + +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! + + + + + +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). + + + + + +01.18.24. I'm TAing Cornell's undergrad PL course, my first time ever TAing a course ☺. + + + + + +01.01.24. Push my first commit. + + \ No newline at end of file diff --git a/index.md b/index.md index abaae5d5..0b4899ba 100644 --- 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!