ACM DL

Proceedings of the ACM on

Programming Languages (PACMPL)

Menu
Latest Articles

Versatile event correlation with algebraic effects

We present the first language design to uniformly express variants of n-way joins over asynchronous event streams from different domains, e.g.,... (more)

Parametric polymorphism and operational improvement

Parametricity, in both operational and denotational forms, has long been a useful tool for reasoning about program correctness. However, there is as... (more)

Handling delimited continuations with dependent types

Dependent types are a powerful tool for maintaining program invariants. To take advantage of this aspect in real-world programming, efforts have been... (more)

The simple essence of automatic differentiation

Automatic differentiation (AD) in reverse mode (RAD) is a central component of deep learning and other uses of large-scale optimization. Commonly used RAD algorithms such as backpropagation, however, are complex and stateful, hindering deep understanding, improvement, and parallel execution. This paper develops a simple, generalized AD algorithm... (more)

A spectrum of type soundness and performance

The literature on gradual typing presents three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. This paper presents a uniform semantic framework that explains all three approaches, illustrates how each approach affects a developer's work, and adds a systematic... (more)

Compositional soundness proofs of abstract interpreters

Abstract interpretation is a technique for developing static analyses. Yet, proving abstract interpreters sound is challenging for interesting... (more)

Graduality from embedding-projection pairs

Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about these mixed programs is Siek-Vitousek-Cimini-Boyland’s (dynamic) gradual guarantee, which says that giving components of a program more precise types only adds runtime type checking, and... (more)

Incremental relational lenses

Lenses are a popular approach to bidirectional transformations, a generalisation of the view update problem in databases, in which we wish to make changes to source tables to effect a desired change on a view. However, perhaps surprisingly, lenses have seldom actually been used to implement updatable views in databases. Bohannon, Pierce and Vaughan... (more)

Elaborating dependent (co)pattern matching

In a dependently typed language, we can guarantee correctness of our programs by providing formal proofs. To check them, the typechecker elaborates these programs and proofs into a low level core language. However, this core language is by nature hard to understand by mere humans, so how can we know we proved the right thing? This question occurs... (more)

Capturing the future by replaying the past (functional pearl)

Delimited continuations are the mother of all monads! So goes the slogan inspired by Filinski’s 1994 paper, which showed that delimited... (more)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic

A number of tools have been developed for carrying out separation-logic proofs mechanically using an... (more)

NEWS

About PACMPL

Proceedings of the ACM on Programming Languages (PACMPL) is a Gold Open Access journal publishing research on all aspects of programming languages, from design to implementation and from mathematical formalisms to empirical studies. Each issue of the journal is devoted to a particular subject area within programming languages and will be announced through publicized Calls for Papers. All accepted papers receive two rounds of reviewing and authors can expect initial decisions regarding submissions in under 3 months. The journal operates in close collaboration with the Special Interest Group on Programming Languages (SIGPLAN) and is committed to making high-quality peer-reviewed scientific research in programming languages free of restrictions on both access and use.

Read more about PACMPL in the inaugural editorial message.

All ACM Journals | See Full Journal Index

Search PACMPL
enter search term and/or author name