VMCAI
Sun 17 - Tue 19 January 2016
St. Petersburg, Florida, United States
co-located with
POPL 2016
Toggle navigation
Attending
Venue: Hilton St. Petersburg Bayfront
VMCAI 2016 Proceedings
Registration
Invited Speakers
Student Travel Funding
Program
Complete Program
Your Program
Online Access to Conference Proceedings
Sun 17 Jan
Mon 18 Jan
Tue 19 Jan
Track/Call
Organization
VMCAI Committees
Program Chairs
Program Committee
Organizing Committee
Steering Committee
Contributors
People Index
Search
Series
Series
VMCAI 2025
VMCAI 2024
VMCAI 2023
VMCAI 2022
VMCAI 2021
VMCAI 2020
VMCAI 2019
VMCAI 2018
VMCAI 2017
VMCAI
Sign in
Sign up
POPL 2016
(
series
) /
VMCAI
(
series
) /
Hilton St. Petersburg Bayfront
/
Room information: Grand Bay South
Venue
Hilton St. Petersburg Bayfront
Room name
Grand Bay South
Floor
0
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-05:00) Guadalajara, Mexico City, Monterrey
.
Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07: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-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:30) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-03:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-02:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02: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+06: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+10:00) Magadan
(GMT+11: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
Wed 20 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
10:30 - 12:10
Track 2: Types and Foundations
POPL Research Papers
at
Grand Bay South
Chair(s):
Robert Atkey
University of Strathclyde
10:30
25m
Talk
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
POPL Research Papers
Matt Brown
UCLA
,
Jens Palsberg
University of California, Los Angeles
Media Attached
File Attached
10:55
25m
Talk
Type Theory in Type Theory using Quotient Inductive Types
POPL Research Papers
Thorsten Altenkirch
University of Nottingham
,
Ambrus Kaposi
University of Nottingham
Media Attached
File Attached
11:20
25m
Talk
System Fω with Equirecursive Types for Datatype-generic Programming
POPL Research Papers
Yufei Cai
University of Tübingen, Germany
,
Paolo G. Giarrusso
University of Tübingen, Germany
,
Klaus Ostermann
University of Tübingen, Germany
Media Attached
11:45
25m
Talk
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
POPL Research Papers
Pierre-Louis Curien
Univ. Paris Diderot and INRIA Paris-Rocquencourt
,
Marcelo Fiore
Computer Laboratory, University of Cambridge
,
Guillaume Munch-Maccagnoni
Computer Laboratory, University of Cambridge
14:20 - 16:00
Track 2: Correct Compilation
POPL Research Papers
at
Grand Bay South
Chair(s):
Jens Palsberg
University of California, Los Angeles
14:20
25m
Talk
Fully-Abstract Compilation by Approximate Back-Translation
POPL Research Papers
Dominique Devriese
iMinds - Distrinet, KU Leuven
,
Marco Patrignani
KU Leuven
,
Frank Piessens
iMinds - Distrinet, KU Leuven
Pre-print
Media Attached
14:45
25m
Talk
Lightweight Verification of Separate Compilation
POPL Research Papers
Jeehoon Kang
Seoul National University
,
Yoonseung Kim
Seoul National University (South Korea)
,
Chung-Kil Hur
Seoul National University
,
Derek Dreyer
MPI-SWS
,
Viktor Vafeiadis
MPI-SWS, Germany
Media Attached
File Attached
15:10
25m
Talk
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
POPL Research Papers
Ed Robbins
Kent
,
Andy King
Kent
,
Tom Schrijvers
KU Leuven
Media Attached
15:35
25m
Talk
Sound Type-dependent Syntactic Language Extension
POPL Research Papers
Florian Lorenzen
TU Berlin
,
Sebastian Erdweg
TU Darmstadt, Germany
Pre-print
Media Attached
File Attached
16:30 - 17:45
Track 2: Decidability and complexity
POPL Research Papers
at
Grand Bay South
Chair(s):
C.-H. Luke Ong
University of Oxford, UK
16:30
25m
Talk
Decidability of Inferring Inductive Invariants
POPL Research Papers
Oded Padon
Tel Aviv University
,
Neil Immerman
University of Massachusetts, Amherst
,
Sharon Shoham
,
Aleksandr Karbyshev
Tel Aviv University
,
Mooly Sagiv
Tel Aviv University
Media Attached
16:55
25m
Talk
The Hardness of Data Packing
POPL Research Papers
Rahman Lavaee
,
Chen Ding
University of Rochester
Media Attached
17:20
25m
Talk
The Complexity of Interaction
POPL Research Papers
Stéphane Gimenez
University of Innsbruck
,
Georg Moser
University of Innsbruck
Media Attached
Thu 21 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
10:30 - 12:10
Track 2: Probabilistic and statistical analysis
POPL Research Papers
at
Grand Bay South
Chair(s):
Aditya Nori
Microsoft Research, UK
10:30
25m
Talk
Prophet: Automatic Patch Generation via Learning from Successful Patches
POPL Research Papers
Fan Long
MIT CSAIL
,
Martin C. Rinard
Massachusetts Institute of Technology, USA
Media Attached
10:55
25m
Talk
Estimating types in binaries using predictive modeling
POPL Research Papers
Omer Katz
Technion, Israel Institute of Technology
,
Ran El-Yaniv
Technion, Israel Institute of Technology
,
Eran Yahav
Technion
Media Attached
File Attached
11:20
25m
Talk
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
POPL Research Papers
Krishnendu Chatterjee
IST Austria
,
Hongfei Fu
IST Austria
,
Rouzbeh Hasheminezhad
Sharif University
,
Petr Novotný
IST Austria
Media Attached
11:45
25m
Talk
Transforming Spreadsheet Data Types using Examples
POPL Research Papers
Rishabh Singh
Microsoft Research
,
Sumit Gulwani
Microsoft Research
Media Attached
14:20 - 16:00
Track 2: Types, Generally or Gradually
POPL Research Papers
at
Grand Bay South
Chair(s):
Tiark Rompf
Purdue & Oracle Labs
14:20
25m
Talk
Principal Type Inference for GADTs
POPL Research Papers
Sheng Chen
University of louisiana at Lafayette
,
Martin Erwig
Oregon State University
Media Attached
14:45
25m
Talk
Abstracting Gradual Typing
POPL Research Papers
Ronald Garcia
University of British Columbia
,
Alison M. Clark
,
Éric Tanter
University of Chile, Chile
Link to publication
Media Attached
15:10
25m
Talk
The Gradualizer: a methodology and algorithm for generating gradual type systems
POPL Research Papers
Matteo Cimini
Indiana University
,
Jeremy G. Siek
Indiana University
Media Attached
15:35
25m
Talk
Is Sound Gradual Typing Dead?
POPL Research Papers
Asumu Takikawa
Northeastern University
,
Daniel Feltey
Northeastern University
,
Ben Greenman
Northeastern University
,
Max S. New
,
Jan Vitek
Northeastern University
,
Matthias Felleisen
Northeastern University
Pre-print
Media Attached
File Attached
16:30 - 17:45
Track 2: Sessions and processes
POPL Research Papers
at
Grand Bay South
Chair(s):
Matteo Maffei
Saarland University
16:30
25m
Talk
Effects as sessions, sessions as effects
POPL Research Papers
Dominic Orchard
Imperial College London
,
Nobuko Yoshida
Imperial College London, UK
Pre-print
Media Attached
16:55
25m
Talk
Monitors and Blame Assignment for Higher-Order Session Types
POPL Research Papers
Limin Jia
Carnegie Mellon University
,
Hannah Gommerstadt
Carnegie Mellon University
,
Frank Pfenning
Carnegie Mellon University
Media Attached
File Attached
17:20
25m
Talk
Environmental Bisimulations for Probabilistic Higher-Order Languages
POPL Research Papers
Davide Sangiorgi
University of Bologna
,
Valeria Vignudelli
University of Bologna/INRIA
Media Attached
Fri 22 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
10:30 - 12:10
Track 2: Semantics and memory models
POPL Research Papers
at
Grand Bay South
Chair(s):
Alexey Gotsman
IMDEA
10:30
25m
Talk
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
POPL Research Papers
Shaked Flur
University of Cambridge
,
Kathryn E. Gray
University of Cambridge
,
Christopher Pulte
University of Cambridge
,
Susmit Sarkar
University of St Andrews
,
Luc Maranget
INRIA Rocquencourt
,
Ali Sezgin
University of Cambridge
,
Will Deacon
ARM Ltd.
,
Peter Sewell
University of Cambridge
Media Attached
File Attached
10:55
25m
Talk
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
POPL Research Papers
Jean Pichon-Pharabod
University of Cambridge
,
Peter Sewell
University of Cambridge
File Attached
11:20
25m
Talk
Overhauling SC atomics in C11 and OpenCL
POPL Research Papers
John Wickerson
Imperial College London
,
Mark Batty
University of Cambridge
,
Alastair F. Donaldson
Imperial College London
Pre-print
File Attached
11:45
25m
Talk
Taming Release-Acquire Consistency
POPL Research Papers
Ori Lahav
MPI-SWS
,
Nick Giannarakis
MPI-SWS
,
Viktor Vafeiadis
MPI-SWS, Germany
Pre-print
Media Attached
File Attached
14:20 - 15:35
Track 2: Foundations of Model Checking
POPL Research Papers
at
Grand Bay South
Chair(s):
Alexandra Silva
Radboud University Nijmegen
14:20
25m
Talk
Lattice-Theoretic Progress Measures and Coalgebraic Model Checking
POPL Research Papers
Ichiro Hasuo
University of Tokyo
,
Shunsuke Shimizu
University of Tokyo
,
Corina Cirstea
University of Southampton
Media Attached
14:45
25m
Talk
Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components
POPL Research Papers
Krishnendu Chatterjee
IST Austria
,
Amir Kafshdar Goharshady
,
Rasmus Ibsen-Jensen
,
Andreas Pavlogiannis
Media Attached
15:10
25m
Talk
Memoryful Geometry of Interaction II: Recursion and Adequacy
POPL Research Papers
Koko Muroya
University of Tokyo
,
Naohiko Hoshino
Kyoto University
,
Ichiro Hasuo
University of Tokyo
Media Attached
Wed 20 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Grand Bay South
POPL Research Papers
Track 2: Types and Foundations
POPL Research Papers
Track 2: Correct Compilation
POPL Research Papers
Track 2: Decidability and complexity
Thu 21 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Grand Bay South
POPL Research Papers
Track 2: Probabilistic and statistical analysis
POPL Research Papers
Track 2: Types, Generally or Gradually
POPL Research Papers
Track 2: Sessions and processes
Fri 22 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
Grand Bay South
POPL Research Papers
Track 2: Semantics and memory models
POPL Research Papers
Track 2: Foundations of Model Checking
Wed 20 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
17:00
15
30
45
Grand Bay South
POPL Research Papers
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
10:30 - 10:55
POPL Research Papers
Type Theory in Type Theory using Quotient Inductive Types
10:55 - 11:20
POPL Research Papers
System Fω with Equirecursive Types for Datatype-generic Programming
11:20 - 11:45
POPL Research Papers
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
11:45 - 12:10
POPL Research Papers
Fully-Abstract Compilation by Approximate Back-Translation
14:20 - 14:45
POPL Research Papers
Lightweight Verification of Separate Compilation
14:45 - 15:10
POPL Research Papers
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
15:10 - 15:35
POPL Research Papers
Sound Type-dependent Syntactic Language Extension
15:35 - 16:00
POPL Research Papers
Decidability of Inferring Inductive Invariants
16:30 - 16:55
POPL Research Papers
The Hardness of Data Packing
16:55 - 17:20
POPL Research Papers
The Complexity of Interaction
17:20 - 17:45
Thu 21 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
17:00
15
30
45
Grand Bay South
POPL Research Papers
Prophet: Automatic Patch Generation via Learning from Successful Patches
10:30 - 10:55
POPL Research Papers
Estimating types in binaries using predictive modeling
10:55 - 11:20
POPL Research Papers
Algorithmic Analysis of Qualitative and Quantitative Termination Proble ...
11:20 - 11:45
POPL Research Papers
Transforming Spreadsheet Data Types using Examples
11:45 - 12:10
POPL Research Papers
Principal Type Inference for GADTs
14:20 - 14:45
POPL Research Papers
Abstracting Gradual Typing
14:45 - 15:10
POPL Research Papers
The Gradualizer: a methodology and algorithm for generating gradual typ ...
15:10 - 15:35
POPL Research Papers
Is Sound Gradual Typing Dead?
15:35 - 16:00
POPL Research Papers
Effects as sessions, sessions as effects
16:30 - 16:55
POPL Research Papers
Monitors and Blame Assignment for Higher-Order Session Types
16:55 - 17:20
POPL Research Papers
Environmental Bisimulations for Probabilistic Higher-Order Languages
17:20 - 17:45
Fri 22 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Grand Bay South
POPL Research Papers
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
10:30 - 10:55
POPL Research Papers
A concurrency semantics for relaxed atomics that permits optimisation a ...
10:55 - 11:20
POPL Research Papers
Overhauling SC atomics in C11 and OpenCL
11:20 - 11:45
POPL Research Papers
Taming Release-Acquire Consistency
11:45 - 12:10
POPL Research Papers
Lattice-Theoretic Progress Measures and Coalgebraic Model Checking
14:20 - 14:45
POPL Research Papers
Algorithms for Algebraic Path Properties in Concurrent Systems of Const ...
14:45 - 15:10
POPL Research Papers
Memoryful Geometry of Interaction II: Recursion and Adequacy
15:10 - 15:35
x
Fri 8 Nov 22:45