APLAS 2017 Program

Monday, November 27, 2017

Registration

8:00 AM	8:30 AM
8:00 AM	8:30 AM	Registration

Session: Invited Talk

8:30 AM	9:35 AM	Chair: Bor-Yuh Evan Chang
8:30 AM	8:35 AM	Xinyu Feng and Bor-Yuh Evan Chang. Welcome to APLAS 2017
8:35 AM	9:35 AM	Gilles Barthe. Relational Verification of Higher-Order Probabilistic Programs

Break

9:35 AM	10:10 AM
9:35 AM	10:10 AM	Tea Break

Session: Security

10:10 AM	11:50 PM	Chair: Atsushi Igarashi
10:10 AM	10:35 AM	Ximeng Li, Heiko Mantel and Markus Tasch. Taming Message-passing Communication in Compositional Reasoning about Confidentiality
10:35 AM	11:00 AM	Ian J. Hayes, Xi Wu and Larissa Meinicke. Capabilities for Java: Secure Access to Resources
11:00 AM	11:25 AM	Serdar Erbatur, Martin Hofmann and Eugen Zalinescu. Enforcing Programming Guidelines with Region Types and Effects
11:25 AM	11:50 PM	Neline van Ginkel, Raoul Strackx and Frank Piessens. Automatically generating secure wrappers for SGX enclaves from separation logic specifications

Lunch

11:50 AM	1:30 PM
11:50 AM	1:30 PM	Lunch

Session: Heap and Equivalence Reasoning

1:30 PM	3:10 PM	Chair: Zhenjiang Hu
1:30 PM	1:55 PM	Manjeet Dahiya and Sorav Bansal. Black-box equivalence checking across compiler optimizations
1:55 PM	2:20 PM	Yoonseok Ko, Xavier Rival and Sukyoung Ryu. Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects
2:20 PM	2:45 PM	Daisuke Kimura and Makoto Tatsuta. Decision Procedure for Entailment of Symbolic Heaps with Arrays
2:45 PM	3:10 PM	Qinxiang Cao, Santiago Cuellar and Andrew Appel. Putting order to the separation logic jungle

Break

3:10 PM	3:40 PM
3:10 PM	3:40 PM	Tea Break

Session: Concurrency and Verification

3:40 PM	5:20 PM	Chair: Makoto Tatsuta
3:40 PM	4:05 PM	Cristina Matache, Victor B. F. Gomes and Dominic Mulligan. Programming and proving with classical types
4:05 PM	4:30 PM	Adrien Pommellet and Tayssir Touili. Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-vous
4:30 PM	4:55 PM	Tobias Nipkow. Verified Root-Balanced Trees
4:55 PM	5:20 PM	Jieung Kim, Vilhelm Sjöberg, Zhong Shao and Ronghui Gu. Safety and Liveness of MCS Lock—Layer by Layer

Reception

6:00 PM	8:00 PM
6:00 PM	8:00 PM	Reception and Poster Session

Tuesday, November 28, 2017

Session: Invited Talk

8:30 AM	9:30 AM	Chair: Xinyu Feng
8:30 AM	9:30 AM	Naijun Zhan. Synthesizing SystemC Code from Delay Hybrid CSP

Break

9:30 AM	10:00 AM
9:30 AM	10:00 AM	Tea Break

Session: Numerical

10:00 AM	11:40 PM	Chair: Kazunori Ueda
10:00 AM	10:25 AM	Aziem Chawdhary and Andy King. Compact Difference Bound Matrices
10:25 AM	10:50 AM	Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido and Ichiro Hasuo. Sharper and Simpler Nonlinear Interpolants for Program Verification
10:50 AM	11:15 AM	Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga and Atsushi Igarashi. A Nonstandard Functional Programming Language
11:15 AM	11:40 PM	Shaobo He and Zvonimir Rakamaric. Counterexample-Guided Bit-Precision Selection

Lunch

11:40 AM	1:30 PM
11:40 AM	1:30 PM	Lunch

Session: Invited Talk

1:30 PM	2:30 PM	Chair: Bor-Yuh Evan Chang
1:30 PM	2:30 PM	Ron Garcia. Gradual Enforcement of Program Invariants

Break

2:30 PM	3:00 PM
2:30 PM	3:00 PM	Tea Break

Session: Semantics

3:00 PM	4:40 PM	Chair: Oleg Kiselyov
3:00 PM	3:25 PM	Martin Sulzmann and Peter Thiemann. A Computational Interpretation of Context-Free Expressions
3:25 PM	3:50 PM	Niccolò Veltri and Tarmo Uustalu. Partiality and container monads
3:50 PM	4:15 PM	Beniamino Accattoli and Bruno Barras. The Negligible and Yet Subtle Cost of Pattern Matching
4:15 PM	4:40 PM	Alejandro Díaz-Caro. A lambda calculus for density matrices wth classical and probabilistic controls

Short Break

4:40 PM	5:00 PM
4:40 PM	5:00 PM	Short Break

Session: Reports and Student Research Competition

5:00 PM	6:00 PM	Chair: Yu Zhang
5:00 PM	5:10 PM	Bor-Yuh Evan Chang. Chair’s Report
5:10 PM	5:15 PM	APLAS 2018 Announcement
5:15 PM	6:00 PM	Student Research Competition Finalist Presentations

Banquet

6:30 PM
6:30 PM		Banquet

Wednesday, November 29, 2017

Session: Invited Talk

8:30 AM	9:30 AM	Chair: Andy King
8:30 AM	9:30 AM	Sumit Gulwani. Programming by Examples: PL meets ML

Break

9:30 AM	10:00 AM
9:30 AM	10:00 AM	Tea Break

Session: Domain-Specific Languages

10:00 AM	11:40 PM	Chair: Wei Ngan Chin
10:00 AM	10:25 AM	Yongzhe Zhang, Hsiang-Shang Ko and Zhenjiang Hu. Palgol: A High-Level DSL for Vertex-Centric Graph Processing with Remote Data Access
10:25 AM	10:50 AM	Bob Reynders and Dominique Devriese. Efficient Functional Reactive Programming through Incremental Behaviors
10:50 AM	11:15 AM	Daan Leijen. Implementing Algebraic Effects in C (or “Monads for Free in C”)
11:15 AM	11:40 PM	Oleg Kiselyov and Tatsuya Katsushima. Sound and Efficient Language-Integrated Query: Maintaining the ORDER

Lunch

11:40 AM	1:00 PM
11:40 AM	1:00 PM	Lunch

Excursion

1:00 PM	5:30 PM
1:00 PM	5:30 PM	Excursion

Hosted on GitHub Pages using the Dinky theme