Collabrative verification of information flow for high insurance app store
Seminar talk, Security and Privacy Seminar at UW-Madison, Madison, Wisconsin
Talks and Presentations
The Ultimate Conditional Syntax
Seminar talk, Programming languages seminar at UW-Madison,
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.
Attacks on open source software - hypocrite commit, SSH backdoor
Seminar talk, Security and Privacy Seminar at UW-Madison, Madison, Wisconsin
Interactive proofs in higher order concurrent separation logic: iris proof mode demo
Seminar talk, Programming languages seminar at UW-Madison,
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.