All Publications
-
-
SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation
-
The Memorist Tale: Every Thunk Every Cost All At Once
-
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
-
Freer Arrows and Why You Need Them in Haskell
-
Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
-
Mechanized Reasoning about "how" Using Functional Programs and Embeddings
-
Program Adverbs and Tlön Embeddings
-
Reasoning about the Garden of Forking Paths
-
Verifying an HTTP Key-Value Server with Interaction Trees and VST
-
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
-
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
-
A Scala based Framework for Developing Acceleration Systems with FPGAs
-
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
-
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code (Experience Report)
-
Scala Based FPGA Design Flow (Abstract Only)
-
AutoBench: Finding Workloads That You Need Using Pluggable Hybrid Analyses
-
ScalaHDL: Express and Test Hardware Designs in a Scala DSL