Welcome

Hello people of the Internet. You have managed to find the webpage of Lucas Silver, a PhD student at the University of Pennsylvania. I work with Steve Zdancewic on research in Programming Languages. In this role, I study how we can build better tools to give high assurances of program correctness. I work closely with other members of the discussion group PLClub to expand our understanding of the science of programming languages.

Publications

Dijkstra Monads Forever: Termination Sensitive Specifications for Interaction Trees - POPL 2021 - 5 min talk - 30 min talk

Projects

Dijkstra Monads for Interaction Trees
In this project we apply the techniques of Dijkstra Monads to program semantics build with the Interaction Trees library. This allows us to verify specifications about effectful, interactive programs.

Research Interests

Rich Program Logics
Software engineers write mountains of important code. Code upon which lives and livelihoods depend on being correct. And this code is very often wrong, and very often wrong in meaningful and even dangerous ways. Writing and verifying formal specifications about code can give us high degrees of confidence that our code is correct. However, the technology of formal specifications lags beyond the rich array of capabilities modern programming languages have. In order to realize the promise of formal specifications, we need program logics that can keep up with these capabilities.
Interaction of Specifications with Semantics
When you have simple programming languages, you can afford to have simple semantics and for the language of your specifications be very simple. However, anything that approaches the complexity of real, modern programming languages is going to need massively complicated semantics and a massively complicated language of specifications. Both of these tasks are difficult on their own, and after you have both, you want to know that your specifications actually properly restrict the behavior of your semantics. Can we reduce the difficulty of these tasks by systematically deriving extensions to specifications from extensions to semantics?
CoInduction
Real programs often diverge. And this divergence is not simply the result of bugs or other failures. Some real programs are designed to run forever. Servers and operating systems are a key example. This means we need to consider infinite behavior in order to write provably correct programs. The makes traditional inductive approaches insufficient. In order to make writing coinductive proofs doable, we need better tools and techniques.