| 9:35 - 9:45 | Opening | Session 1 (Chair: Eijiro Sumii) |
|---|---|
| 9:45 - 10:45 |
Liquid Types For Haskell (Invited Talk)
[slides] Ranjit Jhala |
| 10:45 - 11:00 | Break |
| Session 2 (Chair: Andy King) | 11:00 - 11:30 |
PrologCheck - property-based testing in Prolog
[slides] Cláudio Amaral, Mario Florido and Vítor Santos Costa |
| 11:30 - 12:00 |
Generating Constrained Random Data with Uniform Distribution
[slides] Koen Claessen, Jonas Duregård and Michał H. Pałka |
| 12:00 - 14:00 | Lunch Break |
| Session 3 (Chair: Ken-ichi Asai) | 14:00 - 14:30 |
Guided Type Debugging
[slides] Sheng Chen and Martin Erwig |
| 14:30 - 15:00 |
Using big-step and small-step semantics in Maude to perform declarative debugging
[slides] Adrian Riesco |
| 15:00 - 15:30 | Break |
| Session 4 (Chair: Akimasa Morihata) | 15:30 - 16:00 |
Faustine: a Vector Faust Interpreter Test Bed for Multimedia Signal Processing - System Description - Karim Barkati, Haisheng Wang and Pierre Jouvelot |
| 16:00 - 16:30 |
The Design and Implementation of BER MetaOCaml: System Description
[Web page] Oleg Kiselyov |
| 16:30 - 17:00 |
On Cross-Stage Persistence in Multi-Stage Programming
[slides] Yuichiro Hanada and Atsushi Igarashi |
| Session 5 (Chair: Michael Codish) | 9:45 - 10:45 |
Programming Language Methodologies for Systems Verification (Invited Talk) Gabriele Keller |
|---|---|
| 10:45 - 11:00 | Break |
| Session 6 (Chair: Oleg Kiselyov) | 11:00 - 11:30 |
Lightweight higher-kinded polymorphism
[slides] Jeremy Yallop and Leo White |
| 11:30 - 12:00 |
Generic Programming with Multiple Parameters
[slides] José Pedro Magalhães |
| 12:00 - 14:00 | Lunch Break |
| Session 7 (Chair: Tachio Terauchi) | 14:00 - 14:30 |
Type-Based Amortized Resource Analysis with Integers and Arrays
[slides] Jan Hoffmann and Zhong Shao |
| 14:30 - 15:00 |
Linear Sized Types in the Calculus of Constructions
[slides] Jorge Luis Sacchini |
| 15:00 - 15:30 | Break |
| Session 8 (Chair: Jacques Garrigue) | 15:30 - 16:00 |
Dynamic Programming via Thinning and Incrementalization
[slides] Akimasa Morihata, Masato Koishi and Atsushi Ohori |
| 16:00 - 16:30 |
POSIX Regular Expression Parsing with Derivatives
[slides] Martin Sulzmann and Kenny Zhuo Ming Lu |
| 16:30 - 17:00 |
Semantics for Prolog with Cut - Revisited
[slides] Jael Kriener and Andy King |
| 18:30- | Banquet (Kanazawa Excel Hotel Tokyu) |
| Session 9 (Chair: Naoyuki Tamura) | 9:45 - 10:45 |
Relating Computational Effects by TT-Lifting (Invited Talk) Shin-ya Katsumata |
|---|---|
| 10:45 - 11:00 | Break |
| Session 10 (Chair: Atsushi Igarashi) | 11:00 - 11:30 |
A New Formalization of Subtyping to Match Subclasses to Subtypes
[slides] Hyunik Na and Sukyoung Ryu |
| 11:30 - 12:00 |
Type Soundness and Race Freedom for Mezzo
[slides] Thibaut Balabonski, Francois Pottier and Jonathan Protzenko |
| 12:00 - 14:00 | Lunch Break |
| Session 11 (Chair: Michael Codish) | 14:00 - 14:30 |
Proving Correctness of Compilers using Structured Graphs
[slides] Patrick Bahr |
| 14:30 - 15:00 |
Constraint Logic Programming for Hedges: a Semantic Reconstruction
[slides] Besik Dundua, Mario Florido, Temur Kutsia and Mircea Marin |
| 15:00 - 15:30 | Break |
| Session 12 (Chair: Naoki Kobayashi) | 15:30 - 16:00 |
How many numbers contains a lambda-term?
[slides] Pawel Parys |
| 16:00 - 16:30 |
AC-KBO Revisited
[slides] Akihisa Yamada, Sarah Winkler, Nao Hirokawa and Aart Middeldorp |
| 16:30 - 17:00 |
Well-structured pushdown system: Case of Dense Timed Pushdown Automata
[slides] Xiaojuan Cai and Mizuhito Ogawa |
| 17:00 - 17:15 | Closing |