by Pavel Panchekha with Ian Briggs and Yash Lad on Jun 3, 2024 | Tags: accuracy, approximation, awards, correctness, optimization, type systems
Numerical code needs to carefully balance accuracy and performance. A new DSL, MegaLibm, makes this easier by checking for numerical correctness and offering flexible compilation to efficient code. By reconceptualizing classic numerical techniques like polynomial approximation and range reduction as type-theoric operations like casts and binding operators, MegaLibm makes numerical code composable, and its ability to plug in mathematical an numerical tools (like Sollya) makes it easier and safer to write such code.
Read more...
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...
