Posts by Collection

portfolio

Portfolio item number 1

Short description of portfolio item number 1

Portfolio item number 2

Short description of portfolio item number 2

publications

Formal verification of approximate-DP via the characteristic function

Published in , 1900

Undergraduate Honor Thesis

talks

Interactive proofs in higher order concurrent separation logic: iris proof mode demo

Published: May 24, 2024

There has been tremendous progress on program logics for increasingly sophisticated programming language that reason about challenging features. In this talk, I presented a paper that mechanizes reasoning in CSL by embedding it in the Coq proof assistant. The goal of this paper is to make reasoning in the object logic in the same style as reasoning in Coq proof assistant. When using a proof assistants to reason in an embedded logic one cannot benefit from the proof contexts and basic tactics of the proof assistants. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic. I will be talking about a so-called proof mode that extends the Coq proof assistant with named proof contexts for the object logic. I also gave a demo where we dived into emacs with examples of how proofs are done in both Coq and Iris proof modes.

The Ultimate Conditional Syntax

Published: November 26, 2024

Pattern matching on algebraic datatypes is the cornerstone of functional programming as it allows us to write code which is concise and type safe. But can it be more expressive and more readable compared to existing implementations in languages like OCaml and Haskell? I presented a paper that introduces the ultimate conditional syntax (UCS) — treating pattern matching as a generalization of if-then-else by adding destructing and binding capabilities to boolean expressions. This allows us to write nested multi-way if-expressions which can be split in arbitrary ways. I will first talk about these key features of UCS, followed by describing the source syntax. I will then talk about how UCS is compiled into a core language which is simpler, and how the compilation handles problems like backtracking, missing, and redundant cases. Finally, I will talk about how UCS compares to existing approaches in terms of expressiveness, type checking, and practicality of usage.

Aaryan Patel