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:
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.
Sun 17 OctDisplayed time zone: Central Time (US & Canada) change
09:00 - 10:20 | |||
09:00 60mKeynote | 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 15mTalk | 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 15mTalk | Server-Side Computation of Package Dependencies in Package-Management SystemsVirtual Research Papers | ||
11:20 10mTalk | 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 10mTalk | 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 10mTalk | 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 20mLive 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 15mTalk | 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 15mTalk | A compilation method for dynamic typing in MLVirtual Research Papers | ||
14:20 15mTalk | 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 15mTalk | 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 20mLive Q&A | Q&A and discussionVirtual Research Papers |
17:00 - 18:20 | |||
17:00 60mKeynote | Solidifying and Advancing the Software FoundationsVirtual Keynote Talks Zhendong Su ETH Zurich |
18:50 - 20:10 | |||
18:50 15mTalk | 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 15mTalk | Server-Side Computation of Package Dependencies in Package-Management SystemsVirtual Research Papers | ||
19:20 10mTalk | 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 10mTalk | 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 10mTalk | 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 20mLive 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 15mTalk | 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 15mTalk | A compilation method for dynamic typing in MLVirtual Research Papers | ||
22:20 15mTalk | 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 15mTalk | 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 20mLive Q&A | Q&A and discussionVirtual Research Papers |
Mon 18 OctDisplayed time zone: Central Time (US & Canada) change
09:00 - 10:20 | |||
09:00 60mKeynote | A Separation Logic for Probabilistic IndependenceVirtual Keynote Talks Justin Hsu University of Wisconsin-Madison, USA |
10:50 - 12:10 | |||
10:50 15mTalk | A Typed Programmatic Interface to Contracts on the BlockchainVirtual Research Papers | ||
11:05 15mTalk | 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 15mTalk | 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 15mTalk | 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 20mLive Q&A | Q&A and discussionVirtual Research Papers |
13:50 - 15:10 | |||
13:50 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 20mLive Q&A | Q&A and discussionVirtual Research Papers |
17:00 - 18:20 | |||
17:00 60mKeynote | 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 15mTalk | A Typed Programmatic Interface to Contracts on the BlockchainVirtual Research Papers | ||
19:05 15mTalk | 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 15mTalk | 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 15mTalk | 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 20mLive Q&A | Q&A and discussionVirtual Research Papers |
21:50 - 23:10 | |||
21:50 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 20mLive Q&A | Q&A and discussionVirtual Research Papers |
Accepted 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 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 17 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.