Projects
A description of my ongoing and past projects can be found below
Pint: A small trusted kernel with dependent intersections, unions, and index erasure
A compact, syntax-directed calculus equipped with a bidirectional type checker supporting dependent intersection and union types, subtyping, and explicit coercions. The system incorporates index and coercion erasure to ensure that program equivalence is preserved at runtime, while maintaining soundness and compatibility with an implicit, bidirectional checking discipline. Finally, we generalize the framework to a quantitative resource setting, following McBride’s graded type theory, allowing Pint’s irrelevance and erasure mechanisms to be expressed via graded quantities. This subsumes ad-hoc erasure techniques and enables principled, resource-aware typing within the calculus
Pint on the Rocqs
Aims to mechanize the complete Pint calculus in Rocq, including dependent intersection and union types, subtyping, and coercions. The project formalizes Pint within a small, verifiable kernel, quantifying proof size, isolating axioms, and ensuring that the trusted computing base remains minimal. In addition, we develop a domain-specific language (DSL) for embedding imperative and object-oriented programs into the mechanization, enabling practical program verification within the formalized system.
Composition of Sigma Protocols
TBD
Interactive Zero Knowledge Proofs for Quadratic Residues in EasyCrypt
Zero knowledge proofs (ZKP) have gained popularity recently due to their ability to protect data while also being efficient. Interractive ZKP's allow a prover to convince a verifier about the validy of some statement without revealing any meaningful information beyond the truth of the statement itself. In this project, we studied a Sigma-protocol for quadratic residues and formalized its security properties in the EasyCrypt proof assistant. We provided machine-checked proofs of completeness, soundness, and honest-verifier zero-knowledge within a game-based framework. A more detailed report can be found here
Row Level Security in Databases
This project implements Row-Level Security (RLS) for a SQLite database using Haskell and the LIO (Labeled IO) library for information-flow control. We model database tables as Haskell data types and associate each row with dynamically constructed DCLabels encoding secrecy and integrity policies. Security is implemented in a secure database layer that extends basic database operations with label-based checks, ensuring that data flows only when permitted by the canFlowTo relation. The system supports secure insertion, querying, and deletion of customer records, with multiple versions exploring role-based access control through labels representing administrators and regular users. Serialization and deserialization of labels enable persistent storage in SQLite, and prepared statements are used to safely interface between Haskell and SQL. This work demonstrates how fine-grained information-flow control using Haskell LIO can be used to enforce security policies in databases. Slides can be found 🎞 here