All Publications
-
-
The Memorist Tale: Every Thunk Every Cost All At Once
-
SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation
-
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