VMCAI
Sun 17 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
POPL 2016 (series) / VMCAI (series) / Hilton St. Petersburg Bayfront /

Room information: Grand Bay South

VenueHilton St. Petersburg Bayfront
Room nameGrand Bay South
Floor0
Room InformationNo extra information available
Program

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 FoundationsPOPL 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 CompilationPOPL 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 complexityPOPL 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 analysisPOPL 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 GraduallyPOPL 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 processesPOPL 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 modelsPOPL 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 CheckingPOPL 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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
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

Room10:003011:003012:003013:003014:003015:0030
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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:00153045
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