APLAS 2024
Tue 22 - Fri 25 October 2024 Kyoto

This program is tentative and subject to change.

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
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
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
File Attached
16:55
6m
Poster
[SRC] Testing and Finding Bugs in Homomorphic Encryption Libraries with Equivalence Partitioning
SRC & Posters
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
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

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
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
14:00 - 15:40
Finalist PresentationSRC & Posters at Yamauchi Hall
Chair(s): Koko Muroya NII, Yudai Tanabe Institute of Science Tokyo
15:40 - 16:00
16:00 - 17:00
Probabilistic and Declarative ProgrammingResearch Papers at Yamauchi Hall
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
19:00
2h
Dinner
Dinner
Catering

Thu 24 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

09:00 - 10:00
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
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 Advanced Digital Sciences Center
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
12:00 - 14:30
14:30 - 15:30
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
17:00 - 17:30

Fri 25 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

09:00 - 10:30
09:00
30m
Talk
Automata-based approach for quantum circuit/program verification
APLAS NIER
Yu-Fang Chen Academia Sinica
09:30
30m
Talk
Hyper parametric timed CTL
APLAS NIER
Masaki Waga Kyoto University, Étienne André Université Sorbonne Paris Nord; LIPN; CNRS
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
13:30 - 15:00
13:30
30m
Talk
Verified and Verifying Compositional Compilation for Program Correctness and Safety
APLAS NIER
Yuting Wang Shanghai Jiao Tong University
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