Relational database applications are notoriously difficult to test and debug. Concurrent execution of database transactions may violate complex... (more)
As machine learning systems are increasingly used to make real world legal and financial decisions, it is of paramount importance that we develop... (more)
We present Parallely, a programming language and a system for verification of approximations in... (more)
In 2016, the first quantum processors have been made available to the general public. The possibility of programming an actual quantum device has elicited much enthusiasm. Yet, such possibility also brought challenges. One challenge is the so called Qubit Allocation problem: the mapping of a virtual quantum circuit into an actual quantum architecture. There exist solutions to this problem; however, in our opinion, they fail to capitalize on decades of improvements on graph theory. In contrast,... (more)
The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between... (more)
In the context of gradual typing, type soundness guarantees the safety of typed code. When untyped code fails to respect types, a runtime check finds the discrepancy. As for untyped code, type soundness makes no promises; it does not protect untyped code from mistakes in type specifications and unwarranted blame. To address the asymmetry, this... (more)
TLA+ is a language for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. TLA+ is extremely concise yet expressive: The language primitives include Booleans, integers, functions, tuples, records,... (more)
The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are... (more)
The scope and scale of biological data are increasing at an exponential rate, as technologies like next-generation sequencing are becoming radically... (more)
It is well known that a staged interpreter is a compiler: specializing an interpreter to a given program produces an equivalent executable that runs... (more)
We present a novel approach to context-free grammar parsing that is based on generating a sequence of grammars called derivative grammars from a given... (more)
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.
enter search term and/or author name