projects

Research projects in Programming Languages, Formal Methods, and Neurosymbolic AI.

Our group is involved in several interesting projects across Programming Languages, Type systems, Program Verification and Synthesis, and Neurosymbolic programming/AI. Below, I list some of these:

Formal Methods Verification
Formal Methods Lean Refinement Types Coverage Types

Formal Methods for Verification and Synthesis

This umbrella project aims to make fundamental contributions to the use of Formal Methods (e.g., Refinement Types) to aid programmers in writing correct, safe and coverage complete programs.

  • Coverage Types: Under-approximate properties.
  • Morpheus: Higher-order parser combinators.
  • Hegel: Novel tree automata for synthesis.
  • Lean: Formal Verification.
Neurosymbolic AI
AI/ML Formal Logic

Neurosymbolic Programming / AI

Working at the intersection of Programming Languages and ML to address the limitations of both Neural and Symbolic approaches. We aim to synthesize efficient, robust, and verified programs for safety-critical tasks.

Check out these resources on Neurosymbolic Programming and Neurosymbolic AI.

Program Synthesis for X
Synthesis for Networking Synthesis for Data Transform

Neurosymbolic Program Synthesis for X

Solving challenging, error-prone programming tasks across various domains using verified program synthesis using a combination of PL and AI/ML techniques.

  • DUNE: NeuroSymbolic Synthesis for Automatic Data Transformation.
  • TANTRA: Correct low-level network configurations.
  • Review the Curated List of synthesis applications.
Trustworthy Concurrency
Parallelism Hardware

Trustworthy Concurrency

Programming and reasoning about concurrent programs is notoriously challenging. We develop scalable reasoning methods for hardware and compilers that support weaker memory models than sequential consistency.