Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with... (more)
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 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)
In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive... (more)
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)
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)
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)
We develop an algebraic and algorithmic theory of principality for the recently introduced framework of intersection type calculi with dimensional... (more)
Bidirectional typechecking, in which terms either synthesize a type or are checked against a known... (more)
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)
Many object-oriented languages provide method overloading, which allows multiple method declarations with the same name. For a given method... (more)
We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism.... (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