APLAS 2021
as the organisers put it
Welcome to the website of The 19th 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 2021 will be co-located with SPLASH 2021. Due to the COVID-19 situation, all authors will be given the chance to present remotely regardless of whether the conference is held as a physical, virtual, or h ...
who it's for
programming languages researchers, formal methods and verification engineers, compiler writers, program analysis developers, language designers, tool implementers and maintainers, software package manager engineers, quantum computing researchers
topics
OCaml Tezos contract interface; fully abstract compilation; relation-based choice in Soufflé; dynamic typing for ML via type tags; dictionary-passing translation for Go; LTL verification of bitvector programs; ZX-calculus circuit simplification; function pointer elimination for C; flat-abstraction string solving; network block summarization for neural nets; server-side package dependency computation; pi-calculus to C termination reduction
| title | author | length |
|---|---|---|
| A Typed Programmatic Interface to Contracts on the Blockchain | Thi Thu Ha Doan, Peter Thiemann | 15m |
Defines a concrete, type-safe interaction between OCaml programs and Tezos contracts and proves preservation and progress for that execution model. Provides a… | ||
| Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly | Carmine Abate, Matteo Busi, Stelios Tsampas | 12m |
Shows that a fully abstract compiler only robustly preserves a precisely characterized set of hyperproperties which can be trivial or meaningless in some… | ||
| The Choice Construct in the Soufflé Language | Xiaowen Hu, Joshua Karp, David Zhao, Abdul Zreika, Xi Wu, Bernhard Scholz | 15m |
Implements a relation-based choice extension to the Soufflé Datalog engine that enforces functional dependencies on relations, emitting an existence-check… | ||
| A compilation method for dynamic typing in ML | Atsushi Ohori, Katsuhiro Ueno | 15m |
Presents a systematic compilation method that adds first-class dynamic typing to ML and ships in SML# 4.0.0. Uses type-directed compilation with type-tag… | ||
| A Dictionary-Passing Translation of Featherweight Go | Martin Sulzmann, Stefan Wehr | 13m |
Paper gives a dictionary-passing translation from Featherweight Go to a simple untyped functional target and claims it preserves dynamic behavior of programs… | ||
| Proving LTL Properties of Bitvector Programs and Decompiled Binaries | Cyrus Liu, Chengbin Pang, Daniel Dietsch, Eric Koskinen, Ton Chanh Le, Georgios Portokalidis, Jun Xu | 15m |
Introduces a source transformation that replaces bitvector operators with extra linear-case splits and uses integer interpolation to let SMT-backed tools… | ||
| Hybrid quantum-classical circuit simplification with the ZX-calculus | Agustín Borgna, Simon Perdrix, Benoît Valiron | 14m |
A complete optimization procedure targets hybrid quantum-classical circuits with classical parity logic (NOT and XOR), translating them into ZX⏚ (ZX-ground)… | ||
| Function Pointer Eliminator for C Programs | Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa | 10m |
Tool converts C to LLVM via Clang, runs SVF pointer analysis, extracts possible targets into JSON, then rewrites the original C to replace each indirect call… | ||
| Solving Not-Substring with Flat Abstraction | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, Di-De Yen | 13m |
Proposes a concrete CEGAR-based method using flat abstraction that encodes non-substring into linear integer (Presburger) constraints and implements it in a… | ||
| Scalable and Modular Robustness Analysis of Deep Neural Networks | Yuyi Zhong, Quang-Trung Ta, Tianzuo Luo, Fanlong ZHANG, Siau-Cheng Khoo | 14m |
BBPoly implements network block summarization on top of the DeepPoly abstract domain to speed robustness verification using only CPU. It segments networks… | ||
| Server-Side Computation of Package Dependencies in Package-Management Systems | Nobuhiro Kasai, Isao Sasano | 13m |
Server computes full dependency graphs for npm packages in advance and serves them so clients fetch each package graph with one request. Implementation… | ||
| Termination Analysis for the \$\pi\$-Calculus by Reduction to Sequential Program Termination | Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada | 14m |
Proposes an automated reduction that translates π-calculus to C so termination of the sequential program implies termination of the original process, and… | ||
| PyCT: A Python Concolic Tester | Wei-Lun Tsai, Wei-Cheng Wu, Di-De Yen, Fang Yu, Yu-Fang Chen | 10m |
PyCT is a Python concolic tester that implements many more integer, string and range type member functions, adds automatic handling for exceptions (inserting a… | ||
| Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications | Wonhyuk Choi, Michel Vazirani, Mark Santolucito | 09m |
Builds a browser-based tool, The SynthSynthesizer, that parses dropdown or written temporal-stream-logic specs into logical formulas, runs reactive synthesis… | ||
| Preprocessing of Alternating Automata for Language Emptiness Testing | Pavol Vargovčík, Lukáš Holík | 15m |
Preprocessing implements boolean simplifications plus two novel rewrites: basic simplification (structural hashing, absorption, removal of empty-state… | ||
| Adaptable Traces for Program Explanations | Divya Bajaj, Martin Erwig, Danila Fedorin, Kai Gay | 15m |
Claim: program execution proof trees become readable explanations after systematic trace transformations that preserve proof content while drastically… | ||
| Latent Effects for Reusable Language Components | Birthe van den Berg, Casper Bach Poulsen, Tom Schrijvers, Nicolas Wu | 15m |
Claims a new class called latent effects that strictly generalizes algebraic and scoped effects and adds a modular latent monad plus a latent functor L to let… | ||
| nothing matches | ||