APLAS 2024
Tue 22 - Fri 25 October 2024
Kyoto
Toggle navigation
Attending
Venue: Shirankaikan (Kyoto University medical school area)
Registration
Social Events
Program
APLAS Program
Your Program
Tue 22 Oct
Wed 23 Oct
Thu 24 Oct
Fri 25 Oct
Tracks
APLAS 2024
Events
Keynote
- How to design, document, and implement programming languages
- K-Pop the Ultimate Compilation: No Kernel Left Behind
- High-Order Fixpoint Logic for Automated Program Verification
SRC & Posters
Research Papers
APLAS NIER
Organization
APLAS 2024 Committees
Organizing Committee
Track Committees
SRC & Posters
Organizer
SRC & Posters
Judges
SRC & Posters
Selection Committee
Research Papers
Organizing Committee
Research Papers
Program Committee
Research Papers
Steering Committee
Contributors
People Index
Search
Series
Series
APLAS 2025
APLAS 2024
APLAS 2023
APLAS 2022
APLAS 2021
APLAS 2020
APLAS 2019
Sign in
Sign up
APLAS 2024 (
series
) /
Shirankaikan (Kyoto University medical school area)
/
Room information: Yamauchi Hall
Venue
Shirankaikan (Kyoto University medical school area)
Room name
Yamauchi Hall
Floor
2
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+09:00) Osaka, Sapporo, Tokyo
.
Use conference time zone: (GMT+09:00) Osaka, Sapporo, Tokyo
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
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 program
Specify 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 Opening
Events
at
Yamauchi Hall
09:30 - 10:30
Keynote 1
Keynote
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
11:00 - 12:30
Type theory and Semantic Frameworks
Research 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
14:00 - 15:30
Quantum
Research 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
18:00 - 19:30
Reception
Catering
at
Yamauchi Hall
Wed 23 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
09:00 - 10:00
Keynote 2
Keynote
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:30 - 12:00
Type theory and Semantic Frameworks II
Research 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
14:00 - 15:40
Finalist Presentation
SRC & 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
16:00 - 17:00
Probabilistic and Declarative Programming
Research 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
10:30 - 12:00
Logic
Research 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
14:30 - 15:30
Verification
Research 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
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
Closing
Events
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 1
APLAS 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
11:00 - 12:00
Session 2
APLAS 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
13:30 - 15:00
Session 3
APLAS 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
Tue 22 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
Yamauchi Hall
Events
Registration and Opening
Keynote
Keynote 1
Research Papers
Type theory and Semantic Frameworks
Research Papers
Quantum
Catering
Reception
Wed 23 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
Yamauchi Hall
Keynote
Keynote 2
Research Papers
Type theory and Semantic Frameworks II
SRC & Posters
Finalist Presentation
Research Papers
Probabilistic and Declarative Programming
Thu 24 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Yamauchi Hall
Research Papers
Logic
Research Papers
Verification
Research Papers
Verification (remote)
Events
Closing
Fri 25 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
Yamauchi Hall
APLAS NIER
Session 1
APLAS NIER
Session 2
APLAS NIER
Session 3
Tue 22 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
Yamauchi Hall
APLAS Keynote
How to design, document, and implement programming languages
09:30 - 10:30
APLAS Research Papers
Comparing semantic frameworks of dependently-sorted algebraic theories
11:00 - 11:30
APLAS Research Papers
Random-access lists, from EE to FP
11:30 - 12:00
APLAS Research Papers
Generic Reasoning of the Locally Nameless Representation
12:00 - 12:30
APLAS Research Papers
Quantum Programming Without the Quantum Physics
14:00 - 14:30
APLAS Research Papers
Quantum Bisimilarity is a Congruence under Physically Admissible Schedulers
14:30 - 15:00
APLAS Research Papers
Type-Based Verification of Connectivity Constraints in Lattice Surgery
15:00 - 15:30
Wed 23 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
Yamauchi Hall
APLAS Keynote
K-Pop the Ultimate Compilation: No Kernel Left Behind
09:00 - 10:00
APLAS Research Papers
Building A Correct-By-Construction Type Checker for a Dependently Typed ...
10:30 - 11:00
APLAS Research Papers
Extending the Quantitative Pattern-Matching Paradigm
11:00 - 11:30
APLAS Research Papers
On Computational Indistinguishability and Logical Relations
11:30 - 12:00
APLAS SRC & Posters
[SRC] (Bi-)^3 directional Typing for Answer Type Modification
14:00 - 14:20
APLAS SRC & Posters
[SRC] Lightweight Dependent Types via Staging: Compile-Time Manifest Co ...
14:20 - 14:40
APLAS SRC & Posters
[SRC] Refined^2 Environment Classifiers
14:40 - 15:00
APLAS SRC & Posters
[SRC] Testing and Finding Bugs in Homomorphic Encryption Libraries with ...
15:00 - 15:20
APLAS SRC & Posters
[SRC] Verified Exact Inference for Testing Quantum Circuit Transformers ...
15:20 - 15:40
APLAS Research Papers
Hybrid Verification of Declarative Programs with Arithmetic Non-Fail Co ...
16:00 - 16:30
APLAS Research Papers
Explaining Explanations in Probabilistic Logic Programming
16:30 - 17:00
Thu 24 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
Yamauchi Hall
APLAS Research Papers
Effective Search Space Pruning for Testing Deep Neural Networks
10:30 - 11:00
APLAS Research Papers
Non-deterministic, probabilistic, and quantum effects through the lens ...
11:00 - 11:30
APLAS Research Papers
Relative Completeness of Incorrectness Separation Logic
11:30 - 12:00
APLAS Research Papers
A Formal Verification Framework for Tezos Smart Contracts Based on Symb ...
14:30 - 15:00
APLAS Research Papers
Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas ...
15:00 - 15:30
APLAS Research Papers
Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Si ...
16:00 - 16:30
APLAS Research Papers
OBRA: Oracle-based, relational, algorithmic type verification
16:30 - 17:00
Fri 25 Oct
Displayed time zone:
Osaka, Sapporo, Tokyo
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
Yamauchi Hall
APLAS NIER
Automata-based approach for quantum circuit/program verification
09:00 - 09:30
APLAS NIER
Hyper parametric timed CTL
09:30 - 10:00
APLAS NIER
Compositional Probabilistic Model Checking with String Diagrams of MDPs
10:00 - 10:30
APLAS NIER
Grammar-based Pattern Matching and Type Checking for Difference Data St ...
11:00 - 11:30
APLAS NIER
Climbing up a ladder: a new approach to contextual refinement
11:30 - 12:00
APLAS NIER
Verified and Verifying Compositional Compilation for Program Correctnes ...
13:30 - 14:00
APLAS NIER
Specification and Verification for Higher-Order Imperative Programs
14:00 - 14:30
APLAS NIER
Deterministic Suffix-reading Automata
14:30 - 15:00
x
Wed 18 Dec 16:48