Write a Blog >>
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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 2: Types and FoundationsResearch Papers at Grand Bay South
Chair(s): Robert AtkeyUniversity of Strathclyde
10:30
25m
Talk
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
Research Papers
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles
Media Attached File Attached
10:55
25m
Talk
Type Theory in Type Theory using Quotient Inductive Types
Research Papers
Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham
Media Attached File Attached
11:20
25m
Talk
System Fω with Equirecursive Types for Datatype-generic Programming
Research Papers
Yufei CaiUniversity of Tübingen, Germany, Paolo G. GiarrussoUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
Media Attached
11:45
25m
Talk
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi
Research Papers
Pierre-Louis CurienUniv. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo FioreComputer Laboratory, University of Cambridge, Guillaume Munch-MaccagnoniComputer Laboratory, University of Cambridge
14:20 - 16:00
Track 2: Correct CompilationResearch Papers at Grand Bay South
Chair(s): Jens PalsbergUniversity of California, Los Angeles
14:20
25m
Talk
Fully-Abstract Compilation by Approximate Back-Translation
Research Papers
Dominique DevrieseiMinds - Distrinet, KU Leuven, Marco PatrignaniKU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven
Pre-print Media Attached
14:45
25m
Talk
Lightweight Verification of Separate Compilation
Research Papers
Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Media Attached File Attached
15:10
25m
Talk
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Research Papers
Media Attached
15:35
25m
Talk
Sound Type-dependent Syntactic Language Extension
Research Papers
Florian LorenzenTU Berlin, Sebastian ErdwegTU Darmstadt, Germany
Pre-print Media Attached File Attached
16:30 - 17:45
Track 2: Decidability and complexityResearch Papers at Grand Bay South
Chair(s): C.-H. Luke OngUniversity of Oxford, UK
16:30
25m
Talk
Decidability of Inferring Inductive Invariants
Research Papers
Oded PadonTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Sharon Shoham, Aleksandr KarbyshevTel Aviv University, Mooly SagivTel Aviv University
Media Attached
16:55
25m
Talk
The Hardness of Data Packing
Research Papers
Rahman Lavaee, Chen DingUniversity of Rochester
Media Attached
17:20
25m
Talk
The Complexity of Interaction
Research Papers
Stéphane GimenezUniversity of Innsbruck, Georg MoserUniversity of Innsbruck
Media Attached

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 2: Probabilistic and statistical analysisResearch Papers at Grand Bay South
Chair(s): Aditya NoriMicrosoft Research, UK
10:30
25m
Talk
Prophet: Automatic Patch Generation via Learning from Successful Patches
Research Papers
Fan LongMIT CSAIL, Martin RinardMassachusetts Institute of Technology, USA
Media Attached
10:55
25m
Talk
Estimating types in binaries using predictive modeling
Research Papers
Omer KatzTechnion, Israel Institute of Technology, Ran El-YanivTechnion, Israel Institute of Technology, Eran YahavTechnion
Media Attached File Attached
11:20
25m
Talk
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
Research Papers
Krishnendu ChatterjeeIST Austria, Hongfei FuIST Austria, Rouzbeh HasheminezhadSharif University, Petr NovotnyIST Austria
Media Attached
11:45
25m
Talk
Transforming Spreadsheet Data Types using Examples
Research Papers
Rishabh SinghMicrosoft Research, Sumit GulwaniMicrosoft Research
Media Attached
14:20 - 16:00
Track 2: Types, Generally or GraduallyResearch Papers at Grand Bay South
Chair(s): Tiark RompfPurdue & Oracle Labs
14:20
25m
Talk
Principal Type Inference for GADTs
Research Papers
Sheng ChenUniversity of louisiana at Lafayette, Martin ErwigOregon State University
Media Attached
14:45
25m
Talk
Abstracting Gradual Typing
Research Papers
Ronald GarciaUniversity of British Columbia, Alison M. Clark, Éric TanterUniversity of Chile, Chile
Link to publication Media Attached
15:10
25m
Talk
The Gradualizer: a methodology and algorithm for generating gradual type systems
Research Papers
Matteo CiminiIndiana University, Jeremy G. SiekIndiana University
Media Attached
15:35
25m
Talk
Is Sound Gradual Typing Dead?
Research Papers
Asumu TakikawaNortheastern University, Daniel FelteyNortheastern University, Ben GreenmanNortheastern University, Max New, Jan VitekNortheastern University, Matthias FelleisenNortheastern University
Pre-print Media Attached File Attached
16:30 - 17:45
Track 2: Sessions and processesResearch Papers at Grand Bay South
Chair(s): Matteo MaffeiSaarland University
16:30
25m
Talk
Effects as sessions, sessions as effects
Research Papers
Dominic OrchardImperial College London, Nobuko YoshidaImperial College London, UK
Pre-print Media Attached
16:55
25m
Talk
Monitors and Blame Assignment for Higher-Order Session Types
Research Papers
Limin JiaCarnegie Mellon University, Hannah GommerstadtCarnegie Mellon University, Frank PfenningCarnegie Mellon University
Media Attached File Attached
17:20
25m
Talk
Environmental Bisimulations for Probabilistic Higher-Order Languages
Research Papers
Davide SangiorgiUniversity of Bologna, Valeria VignudelliUniversity of Bologna/INRIA
Media Attached

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 2: Semantics and memory modelsResearch Papers at Grand Bay South
Chair(s): Alexey GotsmanIMDEA
10:30
25m
Talk
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
Research Papers
Shaked FlurUniversity of Cambridge, Kathryn E. GrayUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Susmit SarkarUniversity of St Andrews, Luc MarangetINRIA Rocquencourt, Ali SezginUniversity of Cambridge, Will DeaconARM Ltd., Peter SewellUniversity of Cambridge
Media Attached File Attached
10:55
25m
Talk
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
Research Papers
Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge
File Attached
11:20
25m
Talk
Overhauling SC atomics in C11 and OpenCL
Research Papers
John WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair DonaldsonImperial College London
Pre-print File Attached
11:45
25m
Talk
Taming Release-Acquire Consistency
Research Papers
Ori LahavMPI-SWS, Nick GiannarakisMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Pre-print Media Attached File Attached

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Thu 21 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change