APLAS 2024 (series) /
APLAS 2024 Program
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Tue 22 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
Tue 22 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change
09:00 - 09:30 | |||
09:30 - 10:30 | Keynote 1Keynote at Yamauchi Hall Chair(s): Atsushi Igarashi Kyoto University, Oleg Kiselyov Tohoku University | ||
09:30 60mTalk | How to design, document, and implement programming languages Keynote Sukyoung Ryu KAIST | ||
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 30mTalk | 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 30mTalk | Random-access lists, from EE to FP Research Papers | ||
12:00 30mTalk | Generic Reasoning of the Locally Nameless Representation Research Papers | ||
12:30 - 14:00 | |||
14:00 - 15:30 | |||
14:00 30mTalk | Quantum Programming Without the Quantum Physics Research Papers Jun Inoue National Institute of Advanced Industrial Science and Technology, Japan | ||
14:30 30mTalk | 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 30mTalk | 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 | |||
18:00 - 19:30 | |||
Wed 23 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
Wed 23 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change
09:00 - 10:00 | |||
09:00 60mTalk | 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 30mTalk | Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language Research Papers | ||
11:00 30mTalk | 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 30mTalk | 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 | ||
14:00 20mPoster | [SRC] (Bi-)^3 directional Typing for Answer Type Modification SRC & Posters Takuma Yoshioka Kyoto University File Attached | ||
14:20 20mPoster | [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 20mPoster | [SRC] Refined^2 Environment Classifiers SRC & Posters Yuito Murase Kyoto University, Japan | ||
15:00 20mPoster | [SRC] Testing and Finding Bugs in Homomorphic Encryption Libraries with Equivalence Partitioning SRC & Posters Hyerin Park KAIST File Attached | ||
15:20 20mPoster | [SRC] Verified Exact Inference for Testing Quantum Circuit Transformers and Simulators SRC & Posters Kanguk Lee KAIST File Attached | ||
15:40 - 16:00 | |||
16:00 - 17:00 | Probabilistic and Declarative ProgrammingResearch Papers at Yamauchi Hall Chair(s): Oleg Kiselyov Tohoku University | ||
16:00 30mTalk | Hybrid Verification of Declarative Programs with Arithmetic Non-Fail Conditions Research Papers Michael Hanus Kiel University | ||
16:30 30mTalk | Explaining Explanations in Probabilistic Logic Programming Research Papers German Vidal Universitat Politecnica de Valencia | ||
19:00 - 21:00 | |||
19:00 2hDinner | Dinner Catering | ||
Thu 24 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
Thu 24 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change
09:00 - 10:00 | |||
09:00 60mTalk | High-Order Fixpoint Logic for Automated Program Verification Keynote Naoki Kobayashi University of Tokyo | ||
10:30 - 11:00 | |||
10:30 - 12:00 | |||
10:30 30mTalk | 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 30mTalk | 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 30mTalk | Relative Completeness of Incorrectness Separation Logic Research Papers File Attached | ||
12:00 - 14:30 | |||
14:30 - 15:30 | |||
14:30 30mTalk | A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution Research Papers | ||
15:00 30mTalk | 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 | |||
16:00 30mTalk | 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 30mTalk | 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 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
Fri 25 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change
09:00 - 10:30 | |||
09:00 30mTalk | Automata-based approach for quantum circuit/program verification APLAS NIER Yu-Fang Chen Academia Sinica Authorizer link Media Attached File Attached | ||
09:30 30mTalk | Hyper parametric timed CTL APLAS NIER DOI Pre-print File Attached | ||
10:00 30mTalk | Compositional Probabilistic Model Checking with String Diagrams of MDPs APLAS NIER Ichiro Hasuo National Institute of Informatics, Japan | ||
10:30 - 11:00 | |||
11:00 - 12:00 | |||
11:00 30mTalk | Grammar-based Pattern Matching and Type Checking for Difference Data Structures APLAS NIER Link to publication | ||
11:30 30mTalk | Climbing up a ladder: a new approach to contextual refinement APLAS NIER Koko Muroya NII File Attached | ||
12:00 - 13:30 | |||
12:00 90mLunch | Lunch Catering | ||
13:30 - 15:00 | |||
13:30 30mTalk | Verified and Verifying Compositional Compilation for Program Correctness and Safety APLAS NIER Yuting Wang Shanghai Jiao Tong University File Attached | ||
14:00 30mTalk | Specification and Verification for Higher-Order Imperative Programs APLAS NIER Wei-Ngan Chin National University of Singapore | ||
14:30 30mTalk | Deterministic Suffix-reading Automata APLAS NIER B Srivathsan Chennai Mathematical Institute | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Break Catering | ||