Select Page

PL Perspectives

Perspectives on computing and technology from and for those with an interest in programming languages.
A DSL for Implementing Math Functions

A DSL for Implementing Math Functions

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...

AI Software Should be More Like Plain Old Software

AI Software Should be More Like Plain Old Software

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...

One Polynomial Approximation to Produce Correctly Rounded Results for Multiple Representations and Rounding Modes

One Polynomial Approximation to Produce Correctly Rounded Results for Multiple Representations and Rounding Modes

To create a single polynomial approximation that produces correct results for multiple representations and rounding modes,  we propose to generate a polynomial that generates the correctly rounded result of f(x) using the non-standard round-to-odd rounding mode with 2 additional precision bits compared to the largest floating point representation that we wish to support.  We provide a proof that this method produces correctly rounded results for multiple representations and for all the standard rounding modes. More detailed explanation of our approach can be found in our POPL 2022 distinguished paper.

Read more...

Bad Reasons to Reject Good Papers, and vice versa

Bad Reasons to Reject Good Papers, and vice versa

Peer review is an essential aspect of academic research, giving a feedback loop that stimulates and rewards high-quality work – but as we all know, it doesn’t always function well. To help maintain a consensus of what constitutes good reviewing, this note spells out some bad and good reasons to reject and accept papers.

Read more...

Neural network verification: Where are we and where do we go from here?

Neural network verification: Where are we and where do we go from here?

Deep learning has transformed the way we think of software and what it can do. But deep neural networks are fragile and their behaviors are often surprising. In many settings, we need to provide formal guarantees on the safety, security, correctness, or robustness of neural networks. In this post, I will talk about the verification problem for neural networks and some of the prominent verification techniques that are being developed. I will also discuss the great challenges that our community is well positioned to address and some of the ideas that we can port from the machine-learning community.

Read more...