APLAS 2024
Tue 22 - Fri 25 October 2024 Kyoto

News

Introduction

The 22nd Asian Symposium on Programming Languages and Systems (APLAS) aims to bring together programming language researchers, practitioners and implementors worldwide, to present and discuss the latest results and exchange ideas in all areas of programming languages and systems. This year’s conference is co-located with the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA)

APLAS 2024 will be held in Kyoto, Japan from Tuesday 22nd to Thursday 24th October 2024. The conference includes the student research competition and the associated poster session. Following the main conference, the New Ideas and Emerging Results (NIER) workshop will be held on Friday 25th October 2024.

APLAS is organized by the Asian Association for Foundation of Software (AAFS), founded by Asian researchers in cooperation with many researchers from Europe and the USA. Past APLAS symposiums were held in Taipei (’23), Auckland (’22), Chicago (’21), Fukuoka (’20), Bali (’19), Wellington (’18), Suzhou (’17), Hanoi (’16), Pohang (’15), Singapore (’14), Melbourne (’13), Kyoto (’12), Kenting (’11), Shanghai (’10), Seoul (’09), Bangalore (’08), Singapore (’07), Sydney (’06), Tsukuba (’05), Taipei (’04) and Beijing (’03) after three informal workshops.

Keynote Speakers

Albert Cohen, Google

Naoki Kobayashi, University of Tokyo (Joint keynote speaker with ATVA 2024)

Sukyoung Ryu, KAIST

Sponsors

Silver Sponsors

Organizational Sponsor

Award Sponsor

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

Tue 22 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

09:30 - 10:30
Keynote 1Keynote at Yamauchi Hall
Chair(s): Atsushi Igarashi Kyoto University, Oleg Kiselyov Tohoku University
09:30
60m
Talk
How to design, document, and implement programming languages
Keynote
10:30 - 11:00
11:00 - 12:30
Type theory and Semantic FrameworksResearch Papers at Yamauchi Hall
Chair(s): Oleg Kiselyov Tohoku University
11:00
30m
Talk
Comparing semantic frameworks of dependently-sorted algebraic theories
Research Papers
Benedikt Ahrens Delft University of Technology, Peter Lefanu Lumsdaine Stockholm University, Paige Randall North Utrecht University
11:30
30m
Talk
Random-access lists, from EE to FP
Research Papers
Pierre-Evariste Dagand IRIF / CNRS , Titouan Quennet Université Paris Cité, CNRS, IRIF
12:00
30m
Talk
Generic Reasoning of the Locally Nameless Representation
Research Papers
Yicheng Ni Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University
12:30 - 14:00
14:00 - 15:30
QuantumResearch Papers at Yamauchi Hall
Chair(s): Jacques Garrigue Nagoya University
14:00
30m
Talk
Quantum Programming Without the Quantum Physics
Research Papers
Jun Inoue National Institute of Advanced Industrial Science and Technology, Japan
14:30
30m
Talk
Quantum Bisimilarity is a Congruence under Physically Admissible Schedulers
Research Papers
Lorenzo Ceragioli IMT Lucca, Italy, Fabio Gadducci University of Pisa, Giuseppe Lomurno University of Pisa, Italy, Gabriele Tedeschi University of Pisa, Italy
15:00
30m
Talk
Type-Based Verification of Connectivity Constraints in Lattice Surgery
Research Papers
Ryo Wakizaka Kyoto University, Atsushi Igarashi Kyoto University, Yasunari Suzuki NTT Computer and Data Science Laboratories
15:30 - 16:00

Wed 23 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

09:00 - 10:00
Keynote 2Keynote at Yamauchi Hall
Chair(s): Oleg Kiselyov Tohoku University
09:00
60m
Talk
K-Pop the Ultimate Compilation: No Kernel Left Behind
Keynote
Albert Cohen Google DeepMind
File Attached
10:00 - 10:30
10:30 - 12:00
Type theory and Semantic Frameworks IIResearch Papers at Yamauchi Hall
Chair(s): Pierre-Evariste Dagand IRIF / CNRS
10:30
30m
Talk
Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language
Research Papers
Bohdan Liesnikov Delft University of Technology, Jesper Cockx Delft University of Technology
11:00
30m
Talk
Extending the Quantitative Pattern-Matching Paradigm
Research Papers
Sandra Alves University of Porto, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France, Miguel Ramos Universidade do Porto, LIACC; Université Paris Cité, IRIF, CNRS
11:30
30m
Talk
On Computational Indistinguishability and Logical Relations
Research Papers
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Zeinab Galal University of Bologna, Giulia Giusti ENS Lyon
12:00 - 14:00
15:40 - 16:00
16:00 - 17:00
Probabilistic and Declarative ProgrammingResearch Papers at Yamauchi Hall
Chair(s): Oleg Kiselyov Tohoku University
16:00
30m
Talk
Hybrid Verification of Declarative Programs with Arithmetic Non-Fail Conditions
Research Papers
Michael Hanus Kiel University
16:30
30m
Talk
Explaining Explanations in Probabilistic Logic Programming
Research Papers
German Vidal Universitat Politecnica de Valencia

Thu 24 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

09:00 - 10:00
Keynote 3Keynote at Inamori Hall
09:00
60m
Talk
High-Order Fixpoint Logic for Automated Program Verification
Keynote
Naoki Kobayashi University of Tokyo
10:30 - 11:00
10:30 - 12:00
LogicResearch Papers at Yamauchi Hall
Chair(s): Daan Leijen Microsoft Research
10:30
30m
Talk
Effective Search Space Pruning for Testing Deep Neural Networks
Research Papers
Bala Rangaya Singapore University of Technology and Design, Eugene Sng Ministry of Defence of Singapore, Minh-Thai Trinh Illinois Advanced Research Center at Singapore Ltd.
11:00
30m
Talk
Non-deterministic, probabilistic, and quantum effects through the lens of event structures
Research Papers
Vitor Fernandes University of Minho, Marc de Visme Université Paris-Saclay, CNRS, INRIA-SIF, LMF, Benoît Valiron Université Paris-Saclay, CNRS, CentraleSupélec, LMF
11:30
30m
Talk
Relative Completeness of Incorrectness Separation Logic
Research Papers
Yeonseok Lee Nagoya University, Koji Nakazawa Graduate School of Informatics, Nagoya University
File Attached
12:00 - 14:30
14:30 - 15:30
VerificationResearch Papers at Yamauchi Hall
Chair(s): Yuting Wang Shanghai Jiao Tong University
14:30
30m
Talk
A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution
Research Papers
Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany
15:00
30m
Talk
Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem
Research Papers
Hiroyuki Katsura The University of Tokyo, Naoki Kobayashi University of Tokyo, Ken Sakayori University of Tokyo, Ryosuke Sato Tokyo University of Agriculture and Technology
15:30 - 16:00
16:00 - 17:00
Verification (remote)Research Papers at Yamauchi Hall
Chair(s): Jacques Garrigue Nagoya University
16:00
30m
Talk
Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses
Research Papers
Shigeyuki Sato The University of Electro-Communications, Taiyo Mizuhashi The University of Tokyo, Genki Kimura The University of Tokyo, Kenjiro Taura The University of Tokyo
16:30
30m
Talk
OBRA: Oracle-based, relational, algorithmic type verification
Research Papers
Lisa Vasilenko IMDEA Software Institute and HSE University, Gilles Barthe MPI-SP; IMDEA Software Institute, Niki Vazou IMDEA Software Institute

Accepted Papers

Title
A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution
Research Papers
Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language
Research Papers
Comparing semantic frameworks of dependently-sorted algebraic theories
Research Papers
Effective Search Space Pruning for Testing Deep Neural Networks
Research Papers
Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses
Research Papers
Explaining Explanations in Probabilistic Logic Programming
Research Papers
Extending the Quantitative Pattern-Matching Paradigm
Research Papers
Generic Reasoning of the Locally Nameless Representation
Research Papers
Hybrid Verification of Declarative Programs with Arithmetic Non-Fail Conditions
Research Papers
Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem
Research Papers
Non-deterministic, probabilistic, and quantum effects through the lens of event structures
Research Papers
OBRA: Oracle-based, relational, algorithmic type verification
Research Papers
On Computational Indistinguishability and Logical Relations
Research Papers
Quantum Bisimilarity is a Congruence under Physically Admissible Schedulers
Research Papers
Quantum Programming Without the Quantum Physics
Research Papers
Random-access lists, from EE to FP
Research Papers
Relative Completeness of Incorrectness Separation Logic
Research Papers
File Attached
Type-Based Verification of Connectivity Constraints in Lattice Surgery
Research Papers

Call for Submissions

Scope

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:

  • programming paradigms and styles: functional, object-oriented, probabilistic, logic, constraint programming; extensible programming languages; programming languages for systems code; novel programming paradigms;
  • methods and tools to specify and reason about programs and languages: programming techniques; meta-programming; domain-specific languages; proof assistants; type systems; dependent types; program logics, static and dynamic program analysis; language-based security; model checking; testing;
  • programming language foundations: formal semantics; type theory; logical foundations; category theory; automata; effects; monads and comonads; recursion and corecursion; continuations and effect handlers; program verification; memory models; abstract interpretation;
  • methods and tools for implementation: compilers; program transformations; rewriting systems; partial evaluation; virtual machines; refactoring; intermediate languages; run-time environments; garbage collection and memory management; tracing; profiling; build systems; program synthesis;
  • concurrency and distribution: process algebras; concurrency theory; session types; parallel programming; service-oriented computing; distributed and mobile computing; actor-based languages; verification and testing of concurrent and distributed systems;
  • applications and emerging topics: programming languages and PL methods in education, security, privacy, database systems, computational biology, signal processing, graphics, human-computer interaction, computer-aided design, artificial intelligence and machine learning; case studies in program analysis and verification.

Submission Information

Submissions should not exceed 17 pages, excluding bibliography, in the Springer LNCS format. LaTeX template is available at Springer’s Information for Authors. The accepted papers will be allowed one extra page to accommodate reviewers’ feedback.

Additional material intended for reviewers but not for publication in the final version -– for example, details of proofs -– may be placed in a clearly marked appendix that is not included in the page limit. The paper must be understandable without the appendix, however. Reviewers are not obligated to review it.

Submitted papers must be unpublished and not submitted for publication elsewhere. Papers must be written in English. Accepted papers must be presented at the conference. For further details, please consult Springer Nature Code of Conduct for Authors.

Papers should be submitted via HotCRP: https://aplas24.hotcrp.com/

Reviewing process

As before, APLAS 2024 uses light double-blind reviewing process, with a rebuttal phase to address factual errors and minor misunderstandings. Reviewers will not see author names until they submit a review. Therefore, the authors must adhere to the following rules:

  • omit your names and institutions;
  • refer to your prior work in the third person, just as you refer to prior work by others;
  • omit the acknowledgments.

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 or makes the job of reviewing the paper more difficult (e.g., important background references should not be omitted or anonymized). In addition, 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. For more details, see the FAQ (on the OOPSLA submission site) https://2023.splashcon.org/track/splash-2023-oopsla#double-blinding-submissions-authors

The proceedings will be published as a volume in Springer’s LNCS series. Previous APLAS proceedings https://link.springer.com/conference/aplas can be found on SpringerLink. Authors interested in making their contributions Open Access please refer to Springer’s webpage https://www.springer.com/gp/computer-science/lncs/open-access-publishing-in-computer-proceedings for additional information, or contact the organizers.

Best Paper Award

APLAS 2024 continues the tradition of the best paper award. The award will be announced on this website, and printed certificates will be issued to the authors in the conference.