by Shravan Narayan and Deian Stefan on Jul 27, 2021 | Tags: computer security, information flow control, sandboxing, type systems, WebAssembly
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. The idea of SFI is old. Its use in production, to sandbox third-party libraries in Firefox, is new. We describe the PL techniques—notably static information flow control—that were key to deploying SFI in practice and their use in tackling software security more generally.
Read more...
by Michael Coblenz, Chris Martens, and Luke Church on Jul 6, 2021 | Tags: formal reasoning, type systems, usability
How can types and formal reasoning tools improve the lives of people who write software? This is the focus of the HATRA (Human Aspects of Types and Reasoning Assistants) workshop. At the 2020 meeting, we discussed exciting opportunities for these key PL techniques to make developers more effective.
Read more...
by Justin Hsu on Jan 28, 2021 | Tags: functional programming, programming paradigms, static analysis, teaching, type systems
How can we refocus and modernize the undergraduate “programming paradigms” course?
Read more...
by John Wickerson on Aug 19, 2020 | Tags: formal verification, functional programming, rust language, separation logic, type systems
People of PL is a series of interviews with PL researchers. In today’s post, John Wickerson chats with Derek Dreyer, who is Faculty at the Max Planck Institute for Software Systems (MPI-SWS), and Honorarprofessor of Computer Science, Saarland University.
Read more...
by John Wickerson on Jun 18, 2020 | Tags: diversity, functional programming, gradual typing, type systems
People of PL is a series of interviews with PL researchers. In today’s post, John Wickerson chats with Ron Garcia, who is an Associate Professor at the University of British Columbia.
Read more...