by Henry DeYoung, Andreia Mordido, Frank Pfenning, and Ankush Das on Jan 29, 2025 | Tags: parametric polymorphism, saturation-based algorithms, structural subtyping
Recursive types, generics (sometimes called parametric polymorphism), and subtyping are all essential features for modern programming languages across numerous paradigms. However, structural subtyping is undecidable in the presence of recursive types and generics. In our POPL 2024 paper and its accompanying implementation, we propose a reconstruction of the interaction between recursive types, generics, and structural subtyping from first principles. We present a notion of parametricity for type constructors that forms the basis of a suitable, decidable fragment of structural subtyping, which we call parametric subtyping.
Read more...
by Rachit Nigam and Alexa VanHattum on Jan 13, 2025 | The Missing Mentoring Pillar The programming languages (PL) community has developed a whole host of mentoring pillars to help new research become a part of our community The Programming Languages Mentoring Workshop (PLMW), our 1-2 day workshop before each of our four...
Read more...
by the PLDI Steering Committee on Jan 2, 2025 | [Note: Since PLDI joined the PACM-PL journal, what was previously called Program Committee is now called Review Committee. In the following, we use the term Program Committee (PC) because it is a better-known term.] Prior to PLDI 2021, the PLDI conference always held...
Read more...
by Will Crichton on Nov 21, 2024 | Tags: human factors, language design, Measurements
Software systems researchers want to make human-centered claims, but don’t have the proper tools to do so. That’s how we ended up with the ubiquitous lines-of-code comparison found in evaluation sections everywhere. In this post, I explore: what can we reasonably expect researchers to do that’s higher quality than LOC but less effort than a full-blown user study?
Read more...
by ASPLOS Steering Committee on Nov 4, 2024 | This article is cross-posted from the SIGARCH Blog. TL;DR The ASPLOS Steering Committee (SC) is soliciting feedback on the new review process introduced with ASPLOS 2023. The SC welcomes input on the impact of the new process and changes being contemplated for ASPLOS...
Read more...
by Tommy Guy, Peli de Halleux, Reshabh K Sharma, and Ben Zorn on Oct 22, 2024 |
Prompts are our way of communicating intent to AI foundation models and large language models. The PL and SE communities have great experience understanding how to build robust software that should now be applied to AI model prompts.
Read more...
by Wenhao Tang, Daniel Hillerström, Sam Lindley, and J. Garrett Morris on Aug 12, 2024 | Tags: control flow linearity, effect handlers, linear types, type-and-effect systems
Programming languages can statically ensure that certain resources are used exactly once through a linear type system based on Girard’s linear logic. Typical linear type systems track the number of times that variables are used under the assumption that continuations are always used linearly. Alas, this assumption is false in programming languages with powerful non-linear control flow features. For instance, in POSIX C the process duplication function `fork()` returns to its caller twice. More generally control operators such as Plotkin and Pretnar’s effect handlers, as in the web-programming language Links, enable the programmer to capture a continuation and then invoke it more than once or drop it altogether.
Read more...
by Stefan Marr on Jul 8, 2024 | Tags: academic writing, benchmarks, Measurements, performance, systems
When we start moving our programming language ideas from the world of proofs to the world of practical implementations, we start to encounter many different problems, one of which is performance. While the most important performance improvement is to go from a...
Read more...
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 Emery Berger and Ben Zorn on Apr 23, 2024 | Tags: AI software, correctness, programming, systems
A Tale of Two Softwares: In a world where AI is revolutionizing the way we interact with technology, a new type of software emerges: AI Software (AISW). But with great power comes great responsibility, and the systems research community must rise to the challenge of ensuring AISW is as robust, secure, and safe as its predecessor, Plain Old Software (POSW).
Read more...
