ACM DL

Proceedings of the ACM on

Programming Languages (PACMPL)

Menu
Latest Articles

Higher inductive types in cubical computational type theory

Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with... (more)

Constructing quotient inductive-inductive types

Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher... (more)

Definitional proof-irrelevance without K

Definitional equality—or conversion—for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that... (more)

Bisimulation as path type for guarded recursive types

In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive... (more)

Abstraction-safe effect handlers via tunneling

Algebraic effect handlers offer a unified approach to expressing control-flow transfer idioms such as exceptions, iteration, and async/await. Unfortunately, previous attempts to make these handlers type-safe have failed to support the fundamental principle of modular reasoning for higher-order abstractions. We demonstrate that abstraction-safe... (more)

Abstracting algebraic effects

Proposed originally by Plotkin and Pretnar, algebraic effects and their handlers are a leading-edge approach to computational effects: exceptions, mutable state, nondeterminism, and such. Appreciated for their elegance and expressiveness, they are now progressing into mainstream functional programming languages. In this paper, we introduce and... (more)

Intersection types and runtime errors in the pi-calculus

We introduce a type system for the π-calculus which is designed to guarantee that typable processes are well-behaved, namely they never produce a... (more)

Principality and approximation under dimensional bound

We develop an algebraic and algorithmic theory of principality for the recently introduced framework of intersection type calculi with dimensional... (more)

Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known... (more)

Fully abstract module compilation

We give a translation suitable for compilation of modern module calculi supporting sealing, generativity, translucent signatures, applicative functors, higher-order functors and/or first-class modules. Ours is the first module-compilation translation with a dynamic correctness theorem. The theorem states that the translation produces target terms... (more)

Polymorphic symmetric multiple dispatch with variance

Many object-oriented languages provide method overloading, which allows multiple method declarations with the same name. For a given method... (more)

Abstracting extensible data types: or, rows by any other name

We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism.... (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