APLAS 2022
as the organisers put it
Welcome to the website of The 20th Asian Symposium on Programming Languages and Systems (APLAS). APLAS aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia but is an international forum that serves the worldwide programming languages community. APLAS 2022 will be co-located with SPLASH 2022. APLAS’22 Proceedings can be downloaded free of charge before December 31, 2022.
| title | author | length |
|---|---|---|
| RHLE: Modular Deductive Verification of Relational ∀∃ Properties | Robert F. Dickerson | 25m |
RHLE defines a deductive logic and verifier for relational ∀∃ properties by turning implementation nondeterminism into choice variables in function… | ||
| Automated Temporal Verification for Algebraic Effects | Yahui Song, Darius Foo, Wei-Ngan Chin | 28m |
ContEffs provides a regular-expression–based logic to state precise temporal properties for algebraic effects and a forward verifier plus fixpoint calculator… | ||
| Verification of Concurrent Programs under Release-Acquire Concurrency | Krishna Shankaranarayanan | 01h 04m |
Shows that reachability under release‑acquire is undecidable for finite‑state programs by a PCP reduction using four threads that guess and verify sequences… | ||
| An Algebraic Theory for Shared-State Concurrency | Yotam Dvir, Ohad Kammar, Ori Lahav | 30m |
Presents a concrete monadic denotational model for a higher‑order language with shared‑state interleaving concurrency, proving a representation theorem that… | ||
| Applicative Intersection Types | Xu Xue, Ningning Xie | 30m |
Two calculi for intersection types with an explicit merge operator: the first admits an unrestricted merge, proves type soundness but yields non-deterministic… | ||
| Decoupling the Ascending and Descending Phases in Abstract Interpretation | Isabella mastrini, Vincent surgery | 29m |
Decouple the ascending (widening) and descending (narrowing) phases by transfer fixed point to D: compute a fast widening fixpoint on A, map that post‑widening… | ||
| Characterizing functions mappable over GADTs | Patricia Johann, Pierre Cagne | 32m |
An algorithm takes a term t and a type-formula specification Phi and returns constraints that exactly characterize which functions are mappable over t; it… | ||
| Novice Type Error Diagnosis with Natural Language Models | true kingal | 30m |
Uses pretrained Transformer language models (BERT/CodeBERT family) to predict token-level type error locations by treating code as token sequences with… | ||
| A Calculus with Recursive Types, Record Concatenation and Subtyping | yoga Jones, Me Bruno oliveris, Anton Farm | 25m |
Paper presents a new calculus that combines iso-recursive types with disjoint intersection types and a merge operator that generalizes symmetric record… | ||
| Inferring Region Types via an Abstract Notion of Environment Transformation | Chuangjie Xu | 29m |
Presents a region-type inference that summarizes each method as an abstract transformation so the method body is analyzed once even for many region-varied… | ||
| Model-based Fault Classification for Automotive Software | Mike Becker, Roland Meyer, Tobias Runge | 32m |
Model-based algorithm replays failing CAN traces symbolically to localize the exact divergence, computes minimal subsets of messages that suffice to cause the… | ||
| nothing matches | ||