Jan-Paul 😎

POPL

Gradual C0: Symbolic Execution for Gradual Verification (TOPLAS)

Jenna DiVincenzo, Ian McCormack, Hemant Gouni, Jacob Gorenburg, Jan-Paul Ramos-Dávila, Mona Zhang, Conrad Zimmerman, Joshua Sunshine, Éric Tanter, Jonathan Aldrich

In 52nd ACM SIGPLAN Symposium on Principles of Programming Languages, 2025.

TOPLAS

Gradual C0: Symbolic Execution for Gradual Verification

Jenna DiVincenzo, Ian McCormack, Hemant Gouni, Jacob Gorenburg, Jan-Paul Ramos-Dávila, Mona Zhang, Conrad Zimmerman, Joshua Sunshine, Éric Tanter, Jonathan Aldrich

In ACM Transactions on Programming Languages and Systems, 2024, Article No.: 14, 1–57, https://doi.org/10.1145/3704808.

CORNELL

Evaluating Soundness of a Gradual Verifier with Property Based Testing

Jan-Paul Ramos-Dávila

In Cornell Undergraduate Research Journal, 2(1), 17–27, 10.37513/curj.v2i1.696.

Scheme

Sound Default-Typed Scheme (Position Paper)

Jan-Paul Ramos-Dávila

In Scheme and Functional Programming Workshop, co-located with ICFP/SPLASH, 2025.

CoqPL

Formal Verification of a Software Defined Delay-Tolerant Network (Extended Abstract)

Jan-Paul Ramos-Dávila, Alwyn E. Goodloe

In The Eleventh International Workshop on Coq for Programming Languages, co-located with POPL, 2025.

NASA / IEEE

Formal Verification of a Software Defined Delay-Tolerant Network

Jan-Paul Ramos-Dávila

In IEEE Workshop on Optimizing Interplanetary Communication Through Network Autonomy, 2024.

PriSC

Gradual Verification of Smart Contracts

Haojia Sun, Kunal Singh, Jan-Paul Ramos-Dávila, Jonathan Aldrich, Jenna Wise (DiVincenzo)

In Workshop on Principles of Secure Compilation, co-located with POPL, 2024.

POPV

Sound Default-Typed Scheme

Jan-Paul Ramos-Dávila

In Principles of Programming and Verification Seminar at Boston University, 2025.

MWPLS

Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime

Jan-Paul Ramos-Dávila

In Midwest Programming Languages Summit, 2023.

POPL SRC

Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime

Jan-Paul Ramos-Dávila

In ACM SIGPLAN Symposium on Principles of Programming Languages, 2024.

POPL SRC

Evaluating Soundness of a Gradual Verifier with Property Based Testing

Jan-Paul Ramos-Dávila

In ACM SIGPLAN Symposium on Principles of Programming Languages, 2023.

Jan-Paul Vincent Ramos-Dávila

Publications

Conferences

Gradual C0: Symbolic Execution for Gradual Verification (TOPLAS)

Journals

Gradual C0: Symbolic Execution for Gradual Verification

Evaluating Soundness of a Gradual Verifier with Property Based Testing

Workshops

Sound Default-Typed Scheme (Position Paper)

Formal Verification of a Software Defined Delay-Tolerant Network (Extended Abstract)

Formal Verification of a Software Defined Delay-Tolerant Network

Gradual Verification of Smart Contracts

Presentations

Sound Default-Typed Scheme

Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime

Research Competitions

Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime

Evaluating Soundness of a Gradual Verifier with Property Based Testing