Schedule

Sunday (2nd December)

Workshop on New Ideas and Emerging Results (NIER’18)
11am: Session 1 : Decidaility and Synthesis
On The Decidability of PDA by Yuxi Fu
Transplanting Syntax-Guided Synthesis to Computer Networks by Xiaokang Qiu
12pm: Lunch
1:30pm: Session 2 : Programmability
Bidirectional Programming in Datalog by Zhenjiang Hu
Task-Oriented Software Development with iTasks by Jurriën Stutterhei
Callability Control by Isaac Oscar Gariano and Marco Servetto
3pm: Afternoon Tea/Coffee
Temporal Properties of Smart Contracts by Ilya Sergey, Amrit Kumar and Aquinas Hobor
On Cut-elimination in Cyclic Proof Systems by Daisuke Kimura, Koji Nakazawa, Tachio Terauchi and Hiroshi Unno
Metaprogramming Statically verified code by Hrshikesh Arora and Marco Servetto

Monday (3rd December)

8:30am: Welcome
9am: Technical Track — Types (Session Chair: Tachio Terauchi, Waseda University, Japan)
Non-linear Pattern Matching with Backtracking for Non-free Data Types by Satoshi Egi (Rakuten Institute of Technology, Japan) and Yuichi Nishiwaki (University of Tokyo, Japan)Types of Fireballs by Beniamino Accattoli (INRIA, France) and Giulio Guerrieri (University of Bologna, Italy)

Factoring Derivation Spaces via Intersection Types by Pablo Barenbaum (University of Buenos Aires, Argentina) and Gonzalo Ciruelos (Universidad de Buenos Aires, Argentina)

10:30am: Morning Tea/Coffee
11am: (Keynote) Amal Ahmed, “Compositional Compiler Verification for a Multi-Language World”
1:30pm Technical Track — Program Analysis (Session Chair: Sukyoung Ryu, KAIST, South Korea)
On the Soundness of Call Graph Construction in the Presence of Dynamic Language Features – A Benchmark and Tool Evaluation by Li Sui (Massey University, New Zealand), Jens Dietrich (Massey University, New Zealand), Amjed Tahir (Massey University, New Zealand), Shawn Rasheed (Massey University, New Zealand), and Michael Emery (Massey University, New Zealand)

Complexity Analysis of Tree Share Structure by Xuan Bach Le (National University of Singapore, Singapore), Aquinas Hobor (National University of Singapore, Singapore), and Anthony Widjaja Lin (University of Oxford, UK)

Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Model by Thibault Suzanne (École Normale Supérieure, France) and Antoine Miné (LIP6, UPMC, France)

3pm: Afternoon Tea/Coffee
3:30pm Tool Papers (Session Chair: Aquinas Hobor, National University of Singapore, Singapore)

Scallina: Translating Verified Programs from Coq to Scala by Youssef El Bakouny (Saint-Joseph University of Beirut, Lebanon) and Dani Mezher (Saint-Joseph University of Beirut, Lebanon)

HoIce: A ICE-based Non-Linear Horn Clause Solver by Adrien Champion (University of Tokyo, Japan), Naoki Kobayashi (University of Tokyo, Japan), and Ryosuke Sato (Kyushu University, Japan)

Traf: a Graphical Proof Tree Viewer Cooperating with Coq through Proof General by Hideyuki Kawabata (Hiroshima City University, Japan), Yuta Tanaka (Hiroshima City University, Japan), Mai Kimura (Hiroshima City University, Japan), and Tetsuo Hironaka (Hiroshima City University, Japan)

The Practice of a Compositional Functional Programming Language by Timothy Jones (Montoux, New Zealand) and Michael Homer (Victoria University of Wellington, New Zealand)

6pm Poster Session

Tuesday (4th December)

9am: Technical Track — Functional Programs and Probabilistic Programs (Session Chair: Sukyoung Ryu, KAIST, South Korea)

New Approaches for Almost-Sure Termination of Probabilistic Programs by Mingzhang Huang (Shanghai Jiao Tong University, China), Hongfei Fu (Shanghai Jiao Tong University, China), and Krishnendu Chatterjee (IST Austria, Austria)

Particle-Style Geometry of Interaction as a Module System by Ulrich Schöpp (Ludwig Maximilian Universität München, Germany)

Automated Synthesis of Functional Programs with Auxiliary Functions by Shingo Eguchi (University of Tokyo, Japan), Naoki Kobayashi (University of Tokyo, Japan), and Takeshi Tsukada (University of Tokyo, Japan)

10:30am: Morning Tea/Coffee
11am: (Keynote) Azalea Raad, “Correctness in a weakly consistent setting”
1:30pm Pickup for excursion to Weta Digitial.
5pm Drop off at Te Papa, time to explore!
6:30pm Evening Banquet at Te Papa

Wednesday (5th December)

9am: Technical Track — Verification (Chung-Kil Hur, Seoul National University, South Korea)

Modular Verification of SPARCv8 Code by Junpeng Zha (University of Science and Technology of China, China), Xinyu Feng (Nanjing University, China), and Lei Qiao (Beijing Institute of Control Engineering, China)

Formal Verification of a Call-by-value Lambda Calculus Machine by Fabian Kunze (Saarland University, Germany), Gert Smolka (Saarland University, Germany), and Yannick Forster (Saarland University, Germany)

Automated Modular Verification for Relaxed Communication Protocols by Andreea Costea (National University of Singapore, Singapore), Wei-Ngan Chin (National University of Singapore, Singapore), Shengchao Qin (Teesside University, UK), and Florin Craciun (Babes-Bolyai University, Romania)

10:30am: Morning Tea/Coffee
11am: (Keynote) Bernhard Scholz, Soufflé: A Datalog Engine for Static Analysis
1:30pm Technical Track — Logic (Session Chair: Wei Ngan Chin, National University of Singapore, Singapore)

Automated proof synthesis for the minimal propositional logic with deep neural networks by Taro Sekiyama (National Institute of Informatics, Japan) and Kohei Suenaga (Kyoto University, Japan)

On the Complexity of Pointer Arithmetic in Separation Logic by James Brotherston (University College London, UK) and Max Kanovich (University College London, UK)

A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints by Quang Loc Le (Teesside University, UK) and Mengda He (Teesside University, UK)

3pm: Afternoon Tea/Coffee
3:30pm Technical Track — Continuation and Model Checking (Session Chair: Atsushi Igarashi, Kyoto University, Japan)

Certifying CPS Transformation of Let-polymorphic Calculus Using PHOAS by Urara Yamada (Ochanomizu University, Japan) and Kenichi Asai (Ochanomizu University, Japan)

Model Checking Differentially Private Properties by Depeng Liu (Chinese Academy of Science, China), Bow-Yaw Wang (Academia Sinica, Taiwan), and Lijun Zhang (Chinese Academy of Science, China)

Shallow Effect Handlers by Daniel Hillerström (University of Edinburgh, UK) and Sam Lindley (University of Edinburgh, UK)

5pm Closing

Thursday (6th December)

9am: Sydney Area Programming Languages Interest Group (SAPLING’18)

Friday (7th December)

9am: Software Innovation NZ Meeting