Write a Blog >>
APLAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021

We solicit contributions in the forms of regular research papers, and tool papers. Among others, solicited topics include:

  • Semantics, logics, foundational theory
  • Design of languages, type systems, and foundational calculi
  • Domain-specific languages
  • Compilers, interpreters, abstract machines
  • Program derivation, synthesis, and transformation
  • Program analysis, verification, model-checking
  • Logic, constraint, probabilistic, and quantum programming
  • Software security
  • Concurrency and parallelism
  • Tools and environments for programming and implementation
  • Applications of SAT/SMT to programming and implementation

Papers should be submitted electronically via the submission web page using HotCRP:

https://aplas2021.hotcrp.com

The acceptable format is PDF. Submitted papers must be unpublished and not submitted for publication elsewhere. Papers must be written in English. The proceedings will be published as a volume in Springer’s LNCS series. Accepted papers must be presented at the conference.

REVIEW PROCESS

APLAS 2021 will use a lightweight double-blind reviewing process. Following this process means that reviewers will not see the authors’ names or affiliations as they initially review a paper. The authors’ names will then be revealed to the reviewers only once their reviews have been submitted. To facilitate this process, submitted papers must adhere to the following: Author names and institutions must be omitted and References to the authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”). The purpose of this process is to help the reviewers come to an initial judgement about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission, makes the job of reviewing the paper more difficult, or interferes with the process of disseminating new ideas. For example, important background references should not be omitted or anonymised, even if they are written by the same authors and share common ideas, techniques, or infrastructure. Authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas.

AUTHOR RESPONSE PERIOD

During the author response period, authors will be able to read reviews and respond to them as appropriate.

PROCEEDINGS

The proceedings will be published in the Lecture Notes in Computer Science Series. Authors should consult Springer’s authors’ instructions and use their proceedings templates, either for LaTeX or for Word, for the preparation of their papers. Springer encourages authors to include their ORCIDs in their papers. In addition, the corresponding author of each paper, acting on behalf of all of the authors of that paper, must complete and sign a Consent-to-Publish form. The corresponding author signing the copyright form should match the corresponding author marked on the paper. Once the files have been sent to Springer, changes relating to the authorship of the papers cannot be made.

RESEARCH INTEGRITY

The Program Committee reserves the right, up until the time of publication, to reverse a decision of paper acceptance. Reversal is possible if fatal flaws are discovered in the paper, or research integrity is found to have been seriously breached.

Dates
Tracks
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sun 17 Oct

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
Invited talk 1Keynote Talks at Zurich D +8h
Chair(s): Hakjoo Oh Korea University
09:00
60m
Keynote
Solidifying and Advancing the Software FoundationsVirtual
Keynote Talks
Zhendong Su ETH Zurich
10:50 - 12:10
Analysis / Synthesis Research Papers at Zurich D +8h
Chair(s): Jiasi Shen Massachusetts Institute of Technology
10:50
15m
Talk
Scalable and Modular Robustness Analysis of Deep Neural NetworksVirtual
Research Papers
Yuyi Zhong School of Computing, National University of Singapore, Quang-Trung Ta National University of Singapore, Tianzuo Luo School of Computing, National University of Singapore, Fanlong ZHANG School of Computer, Guangdong University of Technology, Siau-Cheng Khoo National University of Singapore
11:05
15m
Talk
Server-Side Computation of Package Dependencies in Package-Management SystemsVirtual
Research Papers
Nobuhiro Kasai Shibaura Institute of Technology, Isao Sasano Shibaura Institute of Technology
11:20
10m
Talk
PyCT: A Python Concolic TesterVirtual
Research Papers
Wei-Lun Tsai Academia Sinica, Wei-Cheng Wu University of Southern California, USA, Di-De Yen Academia Sinica, Fang Yu National Chengchi University, Yu-Fang Chen Academia Sinica, Taiwan
11:30
10m
Talk
Program Synthesis for Musicians: A Usability Testbed for Temporal Logic SpecificationsVirtual
Research Papers
Wonhyuk Choi Columbia University, Michel Vazirani Columbia University, Mark Santolucito Barnard College, Columbia University, USA
11:40
10m
Talk
Function Pointer Eliminator for C ProgramsVirtual
Research Papers
Daisuke Kimura Toho University , Mahmudul Faisal Al Ameen University of Tokyo, Makoto Tatsuta National Institute of Informatics, Koji Nakazawa Nagoya University
11:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

13:50 - 15:10
Compilation / TransformationResearch Papers at Zurich D +8h
Chair(s): Sam Lindley The University of Edinburgh, UK
13:50
15m
Talk
A Dictionary-Passing Translation of Featherweight GoVirtual
Research Papers
Martin Sulzmann Karlsruhe University of Applied Sciences, Germany, Stefan Wehr Offenburg University of Applied Sciences
14:05
15m
Talk
A compilation method for dynamic typing in MLVirtual
Research Papers
Atsushi Ohori Tohoku University, Japan, Katsuhiro Ueno Tohoku University
14:20
15m
Talk
Fully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyVirtual
Research Papers
Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università di Pisa - Dipartimento di Informatica, Stelios Tsampas FAU Erlangen-Nuremberg, INF 8
14:35
15m
Talk
Hybrid quantum-classical circuit simplification with the ZX-calculusVirtual
Research Papers
Agustín Borgna Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France and Université Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 91405, Orsay, France, Simon Perdrix Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay
14:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

17:00 - 18:20
Invited talk 1Keynote Talks at Zurich D
Chair(s): Xinyu Wang University of Michigan
17:00
60m
Keynote
Solidifying and Advancing the Software FoundationsVirtual
Keynote Talks
Zhendong Su ETH Zurich
18:50 - 20:10
Analysis / Synthesis (mirror)Research Papers at Zurich D
Chair(s): Kihong Heo KAIST
18:50
15m
Talk
Scalable and Modular Robustness Analysis of Deep Neural NetworksVirtual
Research Papers
Yuyi Zhong School of Computing, National University of Singapore, Quang-Trung Ta National University of Singapore, Tianzuo Luo School of Computing, National University of Singapore, Fanlong ZHANG School of Computer, Guangdong University of Technology, Siau-Cheng Khoo National University of Singapore
19:05
15m
Talk
Server-Side Computation of Package Dependencies in Package-Management SystemsVirtual
Research Papers
Nobuhiro Kasai Shibaura Institute of Technology, Isao Sasano Shibaura Institute of Technology
19:20
10m
Talk
PyCT: A Python Concolic TesterVirtual
Research Papers
Wei-Lun Tsai Academia Sinica, Wei-Cheng Wu University of Southern California, USA, Di-De Yen Academia Sinica, Fang Yu National Chengchi University, Yu-Fang Chen Academia Sinica, Taiwan
19:30
10m
Talk
Program Synthesis for Musicians: A Usability Testbed for Temporal Logic SpecificationsVirtual
Research Papers
Wonhyuk Choi Columbia University, Michel Vazirani Columbia University, Mark Santolucito Barnard College, Columbia University, USA
19:40
10m
Talk
Function Pointer Eliminator for C ProgramsVirtual
Research Papers
Daisuke Kimura Toho University , Mahmudul Faisal Al Ameen University of Tokyo, Makoto Tatsuta National Institute of Informatics, Koji Nakazawa Nagoya University
19:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

21:50 - 23:10
Compilation / Transformation (mirror)Research Papers at Zurich D
Chair(s): Xin Zhang Peking University
21:50
15m
Talk
A Dictionary-Passing Translation of Featherweight GoVirtual
Research Papers
Martin Sulzmann Karlsruhe University of Applied Sciences, Germany, Stefan Wehr Offenburg University of Applied Sciences
22:05
15m
Talk
A compilation method for dynamic typing in MLVirtual
Research Papers
Atsushi Ohori Tohoku University, Japan, Katsuhiro Ueno Tohoku University
22:20
15m
Talk
Fully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyVirtual
Research Papers
Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università di Pisa - Dipartimento di Informatica, Stelios Tsampas FAU Erlangen-Nuremberg, INF 8
22:35
15m
Talk
Hybrid quantum-classical circuit simplification with the ZX-calculusVirtual
Research Papers
Agustín Borgna Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France and Université Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 91405, Orsay, France, Simon Perdrix Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay
22:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

Mon 18 Oct

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
Invited talk 2Keynote Talks at Zurich D +8h
Chair(s): Atsushi Igarashi Kyoto University, Japan
09:00
60m
Keynote
A Separation Logic for Probabilistic IndependenceVirtual
Keynote Talks
Justin Hsu University of Wisconsin-Madison, USA
10:50 - 12:10
Language DesignResearch Papers at Zurich D +8h
Chair(s): Sergio Mover Ecole Polytechnique
10:50
15m
Talk
A Typed Programmatic Interface to Contracts on the BlockchainVirtual
Research Papers
Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany
11:05
15m
Talk
Adaptable Traces for Program ExplanationsVirtual
Research Papers
Divya Bajaj Oregon State University, Martin Erwig Oregon State University, Danila Fedorin Oregon State University, Kai Gay Oregon State University
11:20
15m
Talk
Latent Effects for Reusable Language ComponentsVirtual
Research Papers
Birthe van den Berg KU Leuven, Casper Bach Poulsen Delft University of Technology, Tom Schrijvers KU Leuven, Nicolas Wu Imperial College London, UK
11:35
15m
Talk
The Choice Construct in the Soufflé LanguageVirtual
Research Papers
Xiaowen Hu The University of Sydney, Joshua Karp The University of Sydney, David Zhao The University of Sydney, Abdul Zreika The University of Sydney, Xi Wu The University of Sydney, Bernhard Scholz University of Sydney
11:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

13:50 - 15:10
Verification / TheoryResearch Papers at Zurich D +8h
Chair(s): Xiaokang Qiu Purdue University, USA
13:50
15m
Talk
Preprocessing of Alternating Automata for Language Emptiness TestingVirtual
Research Papers
Pavol Vargovčík Brno University of Technology, Czech Republic, Lukáš Holík Brno University of Technology
14:05
15m
Talk
Proving LTL Properties of Bitvector Programs and Decompiled BinariesVirtual
Research Papers
Cyrus Liu Stevens Institute of Technology, Chengbin Pang Stevens Institute of Technology, Daniel Dietsch University of Freiburg, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Georgios Portokalidis Stevens Institute of Technology, Jun Xu Stevens Institute of Technology
14:20
15m
Talk
Solving Not-Substring with Flat AbstractionVirtual
Research Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Lukáš Holík Brno University of Technology, Denghang Hu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Wei-Lun Tsai Academia Sinica, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Di-De Yen Academia Sinica
14:35
15m
Talk
Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program TerminationVirtual
Research Papers
Tsubasa Shoshi The University of Tokyo, Takuma Ishikawa The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan
14:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

17:00 - 18:20
Invited talk 2Keynote Talks at Zurich D
Chair(s): Xujie Si McGill University, Canada
17:00
60m
Keynote
A Separation Logic for Probabilistic IndependenceVirtual
Keynote Talks
Justin Hsu University of Wisconsin-Madison, USA
18:50 - 20:10
Language Design (mirror)Research Papers at Zurich D
Chair(s): Andreea Costea School of Computing, National University Of Singapore
18:50
15m
Talk
A Typed Programmatic Interface to Contracts on the BlockchainVirtual
Research Papers
Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany
19:05
15m
Talk
Adaptable Traces for Program ExplanationsVirtual
Research Papers
Divya Bajaj Oregon State University, Martin Erwig Oregon State University, Danila Fedorin Oregon State University, Kai Gay Oregon State University
19:20
15m
Talk
Latent Effects for Reusable Language ComponentsVirtual
Research Papers
Birthe van den Berg KU Leuven, Casper Bach Poulsen Delft University of Technology, Tom Schrijvers KU Leuven, Nicolas Wu Imperial College London, UK
19:35
15m
Talk
The Choice Construct in the Soufflé LanguageVirtual
Research Papers
Xiaowen Hu The University of Sydney, Joshua Karp The University of Sydney, David Zhao The University of Sydney, Abdul Zreika The University of Sydney, Xi Wu The University of Sydney, Bernhard Scholz University of Sydney
19:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

21:50 - 23:10
Verification / Theory (mirror)Research Papers at Zurich D
Chair(s): Yue Li Nanjing University
21:50
15m
Talk
Preprocessing of Alternating Automata for Language Emptiness TestingVirtual
Research Papers
Pavol Vargovčík Brno University of Technology, Czech Republic, Lukáš Holík Brno University of Technology
22:05
15m
Talk
Proving LTL Properties of Bitvector Programs and Decompiled BinariesVirtual
Research Papers
Cyrus Liu Stevens Institute of Technology, Chengbin Pang Stevens Institute of Technology, Daniel Dietsch University of Freiburg, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Georgios Portokalidis Stevens Institute of Technology, Jun Xu Stevens Institute of Technology
22:20
15m
Talk
Solving Not-Substring with Flat AbstractionVirtual
Research Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Yu-Fang Chen Academia Sinica, Taiwan, Bui Phi Diep Uppsala University, Sweden, Lukáš Holík Brno University of Technology, Denghang Hu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Wei-Lun Tsai Academia Sinica, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Di-De Yen Academia Sinica
22:35
15m
Talk
Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program TerminationVirtual
Research Papers
Tsubasa Shoshi The University of Tokyo, Takuma Ishikawa The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ken Sakayori The University of Tokyo, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan
22:50
20m
Live Q&A
Q&A and discussionVirtual
Research Papers

Call for Tool Papers

We solicit submissions in the form of tool papers describing a demonstration of a tool or a system that support theory, program construction, reasoning, or program execution in the scope of APLAS. The main purpose of a tool paper is to display a completed, robust and well-documented tool-highlighting the overall functionality of the tool, the interfaces of the tool, interesting examples and applications of the tool, an assessment of the tool’s strengths and weaknesses, and a summary of documentation/support available with the tool. Authors of tool demonstration proposals are expected to present a live demonstration of the tool at the conference. It is highly desirable that the tools are available on the web. System and Tool papers should not exceed 8 pages in the Springer LNCS format, including bibliography and figures. They may include an additional appendix of up to 6 extra pages giving the outline, screenshots, examples, etc. to indicate the content of the proposed live demo.

Call for Regular Research Papers

We solicit submissions in the form of regular research papers describing original scientific research results, including system development and case studies. Among others, solicited topics include:

  • Semantics, logics, foundational theory
  • Design of languages, type systems, and foundational calculi
  • Domain-specific languages
  • Compilers, interpreters, abstract machines
  • Program derivation, synthesis, and transformation
  • Program analysis, verification, model-checking
  • Logic, constraint, probabilistic, and quantum programming
  • Software security
  • Concurrency and parallelism
  • Tools and environments for programming and implementation
  • Applications of SAT/SMT to programming and implementation

Regular research papers should not exceed 18 pages in the Springer LNCS format(LaTeX template), including bibliography and figures. Authors may attach anonymous supplementary material to a submission, on the understanding that reviewers are not obliged to read it. This category encompasses both theoretical and implementation (also known as system descriptions) papers. In either case, submissions should clearly identify what has been accomplished and why it is significant. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. System descriptions papers should contain a link to a working system and will be judged on originality, usefulness, and design. In case of lack of space, proofs, experimental results, or any information supporting the technical results of the paper could be provided as an appendix or a link to a web page, but reviewers are not obliged to read them.

Accepted Papers

Title
A Dictionary-Passing Translation of Featherweight GoVirtual
Research Papers
A Typed Programmatic Interface to Contracts on the BlockchainVirtual
Research Papers
A compilation method for dynamic typing in MLVirtual
Research Papers
Adaptable Traces for Program ExplanationsVirtual
Research Papers
Fully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyVirtual
Research Papers
Function Pointer Eliminator for C ProgramsVirtual
Research Papers
Hybrid quantum-classical circuit simplification with the ZX-calculusVirtual
Research Papers
Latent Effects for Reusable Language ComponentsVirtual
Research Papers
Preprocessing of Alternating Automata for Language Emptiness TestingVirtual
Research Papers
Program Synthesis for Musicians: A Usability Testbed for Temporal Logic SpecificationsVirtual
Research Papers
Proving LTL Properties of Bitvector Programs and Decompiled BinariesVirtual
Research Papers
PyCT: A Python Concolic TesterVirtual
Research Papers
Scalable and Modular Robustness Analysis of Deep Neural NetworksVirtual
Research Papers
Server-Side Computation of Package Dependencies in Package-Management SystemsVirtual
Research Papers
Solving Not-Substring with Flat AbstractionVirtual
Research Papers
Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program TerminationVirtual
Research Papers
The Choice Construct in the Soufflé LanguageVirtual
Research Papers