Program - APLAS 2024

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

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:00 - 09:30	Registration and OpeningEvents at Yamauchi Hall

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 Sukyoung Ryu KAIST

	10:30 - 11:00	Coffee BreakCatering at The 2nd floor corridor

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	LunchCatering at Open space (2nd floor)

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	Coffee BreakCatering at The 2nd floor corridor

16:00 - 17:30	Poster SessionSRC & Posters at The 2nd floor corridor Chair(s): Koko Muroya NII, Yudai Tanabe Institute of Science Tokyo

16:00 6m Poster		[SRC] (Bi-)^3 directional Typing for Answer Type Modification SRC & Posters Takuma Yoshioka Kyoto University File Attached
16:06 6m Poster		[non-SRC] Disproving Termination of O-like Combinators by Tree Automata SRC & Posters Munehiro Iwami Iwate Prefectural University, Keisuke Nakano Tohoku University File Attached
16:13 6m Poster		[SRC / Not under award selection] GPU Code Generation for Dynamic Graph Algorithms SRC & Posters Ashwina Kumar IIT Madras, India File Attached
16:20 6m Poster		[SRC] Implementing a control flow obfuscation tool for Java SRC & Posters Ching Hian Singapore University of Technology and Design, Singapore File Attached
16:27 6m Poster		[SRC] Improving the WebAssembly Specification Framework for Future Proposals SRC & Posters Yusung Sim Korea Advanced Institute of Science and Technology (KAIST) File Attached
16:34 6m Poster		[SRC] Lightweight Dependent Types via Staging: Compile-Time Manifest Contracts SRC & Posters Takashi Suwa Kyoto University and National Institute of Informatics File Attached
16:41 6m Poster		[SRC] On the Equivalence Between Binary and Intermediate Representation Through Filtered-Simulation SRC & Posters Jihee Park Korea Advanced Institute of Science and Technology (KAIST) File Attached
16:48 6m Poster		[SRC] Refined^2 Environment Classifiers SRC & Posters Yuito Murase Kyoto University, Japan
16:55 6m Poster		[SRC] Testing and Finding Bugs in Homomorphic Encryption Libraries with Equivalence Partitioning SRC & Posters Hyerin Park KAIST File Attached
17:02 6m Poster		[non-SRC] Toward a Formalization of Secure-Multiparty Computation Stack SRC & Posters Cheng-Hui Weng Nagoya University, Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan, Jacques Garrigue Nagoya University, Takafumi Saikawa Nagoya University File Attached
17:09 6m Poster		[non-SRC] Towards Ownership Refinement Type Inference with Nested Arrays SRC & Posters Yusuke Fujiwara Kyoto University, Yusuke Matsushita The University of Tokyo, Kohei Suenaga Graduate School of Informatics, Kyoto University, Atsushi Igarashi Kyoto University File Attached
17:16 6m Poster		[SRC] Verified Exact Inference for Testing Quantum Circuit Transformers and Simulators SRC & Posters Kanguk Lee KAIST File Attached
17:23 6m Poster		[SRC] Vython: a Language with Dynamic Version Checking for Gradual Updating SRC & Posters Satsuki Kasuya Institute of Science Tokyo File Attached

	18:00 - 19:30	ReceptionCatering at Yamauchi Hall

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	Coffee BreakCatering at The 2nd floor corridor

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	LunchCatering at Open space (2nd floor)

14:00 - 15:40	Finalist PresentationSRC & Posters at Yamauchi Hall Chair(s): Koko Muroya NII, Yudai Tanabe Institute of Science Tokyo

14:00 20m Poster		[SRC] (Bi-)^3 directional Typing for Answer Type Modification SRC & Posters Takuma Yoshioka Kyoto University File Attached
14:20 20m Poster		[SRC] Lightweight Dependent Types via Staging: Compile-Time Manifest Contracts SRC & Posters Takashi Suwa Kyoto University and National Institute of Informatics File Attached
14:40 20m Poster		[SRC] Refined^2 Environment Classifiers SRC & Posters Yuito Murase Kyoto University, Japan
15:00 20m Poster		[SRC] Testing and Finding Bugs in Homomorphic Encryption Libraries with Equivalence Partitioning SRC & Posters Hyerin Park KAIST File Attached
15:20 20m Poster		[SRC] Verified Exact Inference for Testing Quantum Circuit Transformers and Simulators SRC & Posters Kanguk Lee KAIST File Attached

	15:40 - 16:00	Coffee BreakCatering at The 2nd floor corridor

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

19:00 - 21:00	BanquetCatering at The Sodoh Higashiyama Kyoto

19:00 2h Dinner		Dinner Catering

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	Coffee BreakCatering at The 2nd floor corridor

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	LunchCatering at Open space (2nd floor)

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	Coffee BreakCatering at The 2nd floor corridor

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

	17:00 - 17:30	ClosingEvents at Yamauchi Hall Chair(s): Jacques Garrigue Nagoya University, Koko Muroya NII, Yudai Tanabe Institute of Science Tokyo

Fri 25 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change

09:00 - 10:30	Session 1APLAS NIER at Yamauchi Hall Chair(s): Wei-Ngan Chin National University of Singapore

09:00 30m Talk		Automata-based approach for quantum circuit/program verification APLAS NIER Yu-Fang Chen Academia Sinica Authorizer link Media Attached File Attached
09:30 30m Talk		Hyper parametric timed CTL APLAS NIER Masaki Waga Kyoto University, Étienne André Université Sorbonne Paris Nord; LIPN; CNRS DOI Pre-print File Attached
10:00 30m Talk		Compositional Probabilistic Model Checking with String Diagrams of MDPs APLAS NIER Ichiro Hasuo National Institute of Informatics, Japan

	10:30 - 11:00	Coffee BreakCatering at The 2nd floor corridor

11:00 - 12:00	Session 2APLAS NIER at Yamauchi Hall Chair(s): Jacques Garrigue Nagoya University

11:00 30m Talk		Grammar-based Pattern Matching and Type Checking for Difference Data Structures APLAS NIER Naoki Yamamoto Waseda University, Kazunori Ueda Waseda University Link to publication
11:30 30m Talk		Climbing up a ladder: a new approach to contextual refinement APLAS NIER Koko Muroya NII File Attached

12:00 - 13:30	LunchCatering at Open space (2nd floor)

12:00 90m Lunch		Lunch Catering

13:30 - 15:00	Session 3APLAS NIER at Yamauchi Hall Chair(s): Kazunori Ueda Waseda University

13:30 30m Talk		Verified and Verifying Compositional Compilation for Program Correctness and Safety APLAS NIER Yuting Wang Shanghai Jiao Tong University File Attached
14:00 30m Talk		Specification and Verification for Higher-Order Imperative Programs APLAS NIER Wei-Ngan Chin National University of Singapore
14:30 30m Talk		Deterministic Suffix-reading Automata APLAS NIER B Srivathsan Chennai Mathematical Institute

15:00 - 15:30	BreakCatering at The 2nd floor corridor

15:00 30m Coffee break		Break Catering

APLAS 2024 Program

Tue 22 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change

Wed 23 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change

Thu 24 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change

Fri 25 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change

Tracks

APLAS 2024 Program

Switch Program View

Program Display Configuration

Tue 22 OctDisplayed time zone: Osaka, Sapporo, Tokyo change

Wed 23 OctDisplayed time zone: Osaka, Sapporo, Tokyo change

Thu 24 OctDisplayed time zone: Osaka, Sapporo, Tokyo change

Fri 25 OctDisplayed time zone: Osaka, Sapporo, Tokyo change

Get Calendar (iCal)

Tue 22 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change

Wed 23 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change

Thu 24 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change

Fri 25 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change