#43 PL in the Industry and Summer Schools - Patrick and Eric
Type Theory Forall
Deep Dive
What is Eric Bond's current research focus at the University of Michigan?
Eric Bond is working on extending his advisor Max New's thesis on gradual typing, specifically focusing on polymorphism for gradually typed languages and developing denotational semantics for these models.
What is Patrick Lafontaine's research focus under his advisor Benjamin Delaware?
Patrick Lafontaine is leading his advisor's program synthesis effort, focusing on complex types like refinement types and coverage types. He uses these types to guide synthesis and works predominantly in OCaml, with some synthesizers written in Rust.
What challenges does Eric Bond face in his research on denotational semantics for gradual typing?
Eric Bond is exploring models of state, particularly the dynamic state monad, which supports allocating new cells and setting/getting values. The categorical semantics of dynamic state are more complex than the regular state monad due to the need to account for varying heap configurations and address availability.
What motivated Eric Bond to return to academia after working in industry?
Eric Bond returned to academia to dive deeper into categorical logic and type theory, seeking the academic freedom to explore abstract research. He felt that industry work, while rewarding, was more constrained by deliverables and less focused on theoretical exploration.
What is the NSF CS Grad for US fellowship program, and how did it help Eric Bond?
The NSF CS Grad for US fellowship program supports non-traditional students, particularly those returning from industry to academia. Eric Bond received this fellowship, which provided three years of funding, mentorship, and a community of individuals transitioning back into academia.
What was Patrick Lafontaine's experience during his internship at AWS?
Patrick Lafontaine interned at AWS in the automated reasoning team, where he worked on anomaly detection using complex type systems and abstract interpretation. He appreciated the flexibility to explore ideas and the opportunity to work on impactful problems in a large-scale industry setting.
How does Amazon's investment in formal methods compare to traditional industries?
Amazon heavily invests in formal methods, particularly through its automated reasoning group, to ensure software correctness and reliability. This is a shift from traditional industries like defense and aerospace, where formal methods have historically been more prevalent.
What is the Oregon PL Summer School, and why is it valuable?
The Oregon PL Summer School is a resource for learning about programming languages, featuring world-class researchers and lectures on advanced topics. It is valuable for both students and industry professionals looking to gain insights into academic research and theoretical aspects of PL.
What are the career prospects in programming languages and formal methods?
Career prospects in programming languages and formal methods are strong, with opportunities in both academia and industry. Companies like Amazon are heavily investing in formal methods, and there is a growing demand for expertise in areas like security, verification, and type systems.
- Eric's research extends Max New's work on gradual typing, focusing on polymorphism and denotational semantics.
- Patrick's research involves program synthesis using refinement types and coverage types in OCaml, with some work in Rust.
- Both discuss their preferences for Rust and OCaml, highlighting the advantages and disadvantages of each.