(Tentative) Technical Program

Andrzej Murawski (University of Leicester)

Title: Algorithmic game semantics (75 min)

Nikos Tzevelekos (University of Oxford)

Title: Games with names (45 min)

Matthew Might (University of Utah)

Title: A tutorial on the small-step approach to CFA (75 min)

Jan Midtgaard (Aarhus University)

Title: Flow-Sensitive Type Recovery in Linear-Log Time (45 min)

Friday Afternoon II: 16:00-18:00

Thomas Jensen (INRIA)

Title: Deriving control-flow analyses with abstract interpretation (45 min)

Dimitrios Vardoulakis (Northeastern University)

Title: CFA2: Pushdown Flow Analysis for Higher-Order Languages (60 min)

Luke Ong (University of Oxford)

Title: Recursion Schemes, Collapsible Pushdown Automata, and the Model Checking of Higher-Order Computation (45 min)

Naoki Kobayashi (Tohoku University)

Title: Algorithms and applications of higher-order model checking (45 min)

Saturday Morning: 11:00-12:00

Luca Paolini (Università di Torino)

Title: Higher-order call-by-value software Verification (30 min)

Steven Ramsay (University of Oxford)

Title: Pattern Matching Recursion Schemes for the Verification of Functional Programs (30 min)

Ranjit Jhala (University of California)

Title: Higher-Order Program Verification with Liquid Types (80 min)

Saturday Afternoon II: 15:20-16:35

Suresh Jagannathan (Purdue University)

Title: Using Proofs-from-Tests to Verify Higher-Order Programs (45 min)

Tachio Terauchi (Nagoya University)

Title: Relatively Complete Refinement Types from Counterexamples (30 min)

Saturday Afternoon III: 17:00-18:00

Hiroshi Unno (Tohoku University)

Title: Predicate Abstraction and CEGAR for Higher-Order Model Checking (30 min)

David Van Horn (Northeastern University)

Title: Abstract Reduction Semantics for Modular Higher-Order Contract Verification (30 min)

Neil D. Jones (University of Cophenhagen)

Title: Termination Analysis of the Untyped lambda-Calculus (45 min)

Jean-Pierre Jouannaud (LIX, Ecole Polytechnique)

Title: Higher-order rules: termination and confluence (45 min)

Sunday Morning II: 11:00-12:00

Fritz Henglein (DIKU)

Title: Soundness is not sufficient (60 min)

Keisuke Nakano (University of Electro-Communications)

Title: View updatablity checking for graph queries (30 min)

Kazuhiro Inaba (Google)

Title: Decomposition of Higher-Order Programs to Garbage-Free First-Order Programs (45 min)

Monday Morning II: 10:45-12:00

Yasuhiko Minamide (University of Tsukuba)

Title: Static Approximation of Dynamically Generated Web Pages with Context-Free Grammars (45 min)

Martin Lester (University of Oxford)

Title: Verifying Liveness Properties of ML Programs (30 min)

Robin Neatherway (University of Oxford)

Title: A syntax-directed approach to model checking higher-order recursion schemes (30min)

Takeshi Tsukada (Tohoku University)

Title: Linear Intersection Types and Game Semantics (30 min)

Akihiko Tozawa (IBM Research, Tokyo)

Title: HORS model checking and logical relation (30 min)

Monday Afternoon II: 15:30-17:00

(session chair: Luke Ong)

Matthew Might (University of Utah)

Title: A family of abstract interpretation for static analysis of concurrent higher-order programs (30 min)

Nikos Tzevelekos (University of Oxford)

Title: Functional Reachability (30 min)

David Van Horn (Northeastern University)

Title: The Complexity of kCFA (30 min)