POPL 2017
Sun 15 - Sat 21 January 2017
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 15 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited talk 1VMCAI at Amphitheater 44
Chair(s): David Monniaux CNRS, VERIMAG
09:00
60m
Talk
Detecting Strict Aliasing Violations in the Wild
VMCAI
Pascal Cuoq Trust-in-Soft
File Attached
10:00 - 10:30
Coffee breakCatering at Catering area
10:00
30m
Coffee break
Break
Catering

10:30 - 12:00
Program AnalysisVMCAI at Amphitheater 44
Chair(s): Boris Yakobowski CEA - LIST
10:30
30m
Talk
Partitioned Memory Models for Program Analysis.
VMCAI
Wei Wang Google, Inc., Clark Barrett Stanford University, Thomas Wies New York University
File Attached
11:00
30m
Talk
Property Directed Reachability for Proving Absence of Concurrent Modification Errors
VMCAI
Asya Frumkin Tel Aviv University, Yotam M. Y. Feldman Tel Aviv University, Ondřej Lhoták University of Waterloo, Canada, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
File Attached
11:30
30m
Talk
Stabilizing Floating-Point Programs using Provenance Analysis
VMCAI
Yijia Gu Northeastern University, Thomas Wahl Northeastern University
12:00 - 14:00
12:00
2h
Lunch
Lunch
Catering

14:00 - 15:30
Concurrency 1VMCAI at Amphitheater 44
Chair(s): Camille Coti LIPN, Université Paris 13
14:00
30m
Talk
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
VMCAI
14:30
30m
Talk
Independence Abstractions and Models of Concurrency
VMCAI
Vijay D'Silva Google Inc., Daniel Kroening University of Oxford, Marcelo Sousa University of Oxford
15:00
30m
Talk
Static Analysis of Communicating Process using Symbolic Transducers
VMCAI
Vincent Botbol CEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le Gall CEA LIST, Emmanuel Chailloux LIP6 - UPMC
Media Attached File Attached
15:30 - 16:00
Coffee breakCatering at Catering area
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Decision proceduresVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
16:00
30m
Talk
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
VMCAI
Ernst Moritz Hahn State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
File Attached
16:30
30m
Talk
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
VMCAI
Andrew Reynolds EPFL, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Cristina Serban VERIMAG, CNRS, Université Grenoble-Alpes
File Attached
17:00
30m
Talk
Matching multiplications in Bit-Vector formulas
VMCAI
Supratik Chakraborty IIT Bombay, Ashutosh Gupta , Rahul Jain Tata Institute of Fundamental Research
File Attached
16:00 - 18:00
Second Afternoon SessionTTT at Salle 105, Barre 44-54
Chair(s): Hugo Herbelin
16:00
50m
Talk
Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq
TTT
Robbert Krebbers Delft University of Technology, Netherlands
16:50
20m
Talk
Introducing MetaCoq: A Safe Tactic Language for Coq
TTT
Beta Ziliani FAMAF, UNC (Argentina) / CONICET (Argentina)
17:10
50m
Other
COST EUTypes session
TTT

Mon 16 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:50 - 09:00
Opening remarksPADL at Salle 116, Barre 44-54
Chair(s): Yuliya Lierler University of Nebraska, Walid Taha Halmstad University
08:50
10m
Talk
Opening remarks
PADL

09:00 - 10:00
Invited talk 2VMCAI at Amphitheater 44
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
09:00
60m
Talk
Verified Concurrent Code: Tricks of the Trade
VMCAI
A: Ernie Cohen Amazon Web Services
09:00 - 10:00
Invited TalkCPP at Auditorium
09:00
60m
Talk
Porting the HOL Light Analysis Library: Some Lessons
CPP
Lawrence Paulson University of Cambridge
File Attached
09:00 - 12:00
Gradual Typing (AM)Tutorials at Salle 105, Barre 44-54
09:00
3h
Talk
The State of the Art in Gradual Typing
Tutorials
Jeremy G. Siek Indiana University Bloomington
09:00 - 12:00
09:00
3h
Talk
The Lean Theorem Prover
Tutorials
Leonardo de Moura Microsoft Research, Redmond, Gabriel Ebner Vienna University of Technology, Jared Roesch University of Washington, USA, Sebastian Ullrich Karlsruhe Institute of Technology
09:00 - 10:00
KeynotePEPM at Salle 109, Barre 44-54
Chair(s): Ulrik Pagh Schultz University of Southern Denmark
09:00
60m
Talk
Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk)
PEPM
Daniil Berezun JetBrains, Russia, Neil D. Jones University of Copenhagen, Danmark
DOI
09:00 - 10:00
09:00
60m
Talk
Proof checking and logic programming
PADL
Dale Miller INRIA Saclay and LIX
10:00 - 10:30
Coffee breakCatering at Auditorium Hall
10:00
30m
Coffee break
Break
Catering

10:30 - 12:00
Numerical domainsVMCAI at Amphitheater 44
Chair(s): Laure Gonnord University of Lyon & LIP, France
10:30
30m
Talk
Sound Bit-Precise Numerical Domains
VMCAI
Tushar Sharma University of Wisconsin - Madison, USA, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
File Attached
11:00
30m
Talk
Efficient Elimination of Redundancies in Polyhedra using Raytracing
VMCAI
Media Attached File Attached
11:30
30m
Talk
Finding Relevant Templates via the Principal Component Analysis
VMCAI
Yassamine Seladji University of Tlemcen
File Attached
10:30 - 12:00
Programming languagesPEPM at Salle 109, Barre 44-54
Chair(s): Andrew Farmer Facebook
10:30
30m
Talk
Lightweight Soundness for Towers of Language Extensions
PEPM
Alejandro Serrano Utrecht University, Jurriaan Hage Utrecht University
11:00
30m
Talk
Detecting code clones with gaps by function applications
PEPM
Tsubasa Matsushita Shibaura Institute of Technology, Isao Sasano Shibaura Institute of Technology
11:30
30m
Talk
PEG Parsing in Less Space Using Progressive Tabling and Dynamic AnalysisBest Paper
PEPM
Fritz Henglein DIKU, Denmark, Ulrik Terp Rasmussen DIKU, University of Copenhagen
12:00 - 14:00
12:00
2h
Lunch
Lunch
Catering

14:00 - 15:30
Model-checking and bug findingVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
14:00
30m
Talk
Effective Bug Finding in C Programs with Shape and Effect Abstraction
VMCAI
Iago Abal IT University of Copenhagen, Claus Brabrand IT University of Copenhagen, Denmark, Andrzej Wąsowski IT University of Copenhagen, Denmark
14:30
30m
Talk
Reduction of Workflow Nets for Generalised Soundness Verification
VMCAI
Hadrien Bride Femto-ST / Université de Franche-Comté, Olga Kouchnarenko Femto-ST / Université de Franche-Comté, Fabien Peureux Femto-ST / Université de Franche-Comté + Smartesting S&S
Media Attached
15:00
30m
Talk
Dynamic Reductions for Model Checking Concurrent Software.
VMCAI
Henning Günther Technische Universität Wien, Alfons Laarman Vienna University of Technology, Ana Sokolova University of Salzburg, Georg Weissenbacher Technische Universität Wien
File Attached
14:00 - 17:00
Gradual Typing (PM)Tutorials at Salle 105, Barre 44-54
14:00
3h
Talk
The State of the Art in Gradual Typing
Tutorials
Jeremy G. Siek Indiana University Bloomington
14:00 - 17:00
14:00
3h
Talk
The Lean Theorem Prover
Tutorials
Leonardo de Moura Microsoft Research, Redmond, Gabriel Ebner Vienna University of Technology, Jared Roesch University of Washington, USA, Sebastian Ullrich Karlsruhe Institute of Technology
14:00 - 15:30
Tutorial (Idris, Inside-Out) and Poster SessionPEPM at Salle 109, Barre 44-54
Chair(s): Ulrik Pagh Schultz University of Southern Denmark, Jeremy Yallop University of Cambridge, UK
14:00
60m
Talk
Idris, Inside-Out: A Tutorial on Extending Idris in Idris
PEPM
David Thrane Christiansen Indiana University
15:00
30m
Talk
Invited posters
PEPM
Nada Amin EPFL, Tiark Rompf Purdue University, Oleg Kiselyov , Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens
15:00
30m
Talk
Language-integrated Query with Ordering, Grouping and Outer Joins (poster)
PEPM
Tatsuya Katsushima Tohoku University, Japan, Oleg Kiselyov
14:00 - 15:30
Testing and GamesPADL at Salle 116, Barre 44-54
14:00
30m
Talk
Failing Faster: Overlapping Patterns for Property-Based Testing
PADL
Jonathan Fowler University of Nottingham, Graham Hutton University of Nottingham
14:30
30m
Talk
Boltzmann Samplers for Closed Simply-Typed Lambda Terms
PADL
Maciej Bendkowski Jagiellonian University, Katarzyna Grygiel Jagiellonian University, Paul Tarau University of North Texas
15:00
30m
Talk
Selection Equilibria of Higher-Order Games
PADL
Paulo Oliva Queen Mary University of London, Jules Hedges University of Oxford, Viktor Winschel ETH Zürich, Philipp Zahn University of St. Gallen, Evguenia Shprits University of Mannheim
15:30 - 16:00
Coffee breakCatering at Auditorium Hall
15:30
30m
Coffee break
Break
Catering

16:00 - 17:30
Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44
Chair(s): Constantin Enea LIAFA, Université Paris Diderot
16:00
30m
Talk
Block-wise abstract interpretation by combining abstract domains with SMT
VMCAI
16:30
30m
Talk
IC3 - Flipping the E in ICE
VMCAI
Yakir Vizel , Arie Gurfinkel University of Waterloo, Sharon Shoham Tel Aviv university, Sharad Malik Princeton University
17:00
30m
Talk
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
VMCAI
Lukáš Holík , Martin Hruska Brno University of Technology , Ondřej Lengál Brno University of Technology , Adam Rogalewicz Brno University of Technology , Tomáš Vojnar Brno University of Technology
16:00 - 17:00
Transformation (part I)PEPM at Salle 109, Barre 44-54
Chair(s): Chung-chieh Shan Indiana University, USA
16:00
30m
Talk
Verification of Code Generators via Higher-Order Model Checking
PEPM
Takashi Suwa University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Atsushi Igarashi Kyoto University
16:30
30m
Talk
Interactive data representation migration: Exploiting program dependence to aid program transformation
PEPM
Krishna Narasimhan Goethe University, Julia Lawall Inria/LIP6, Christoph Reichenbach Goethe University
19:30 - 22:00
BanquetVMCAI at Procope

Tue 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:50 - 09:00
Welcome SessionPLMW at Salle 107, Barre 44-54
08:50
10m
Day opening
Welcome Sesssion
PLMW

09:00 - 10:00
Invited talk 3VMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
09:00
60m
Talk
Verification of Cancer Programs
VMCAI
Jasmin Fisher Microsoft Research
09:00 - 10:00
Invited TalkCPP at Auditorium
09:00
60m
Talk
Mechanized verification of preemptive OS kernels
CPP
Xinyu Feng University of Science and Technology of China
File Attached
09:00 - 10:00
Tutorial: reversible computingPEPM at Salle 109, Barre 44-54
Chair(s): Ulrik Pagh Schultz University of Southern Denmark
09:00
60m
Talk
Reversible computing from a programming language perspective
PEPM
09:00 - 10:00
Applications IIPADL at Salle 116, Barre 44-54
09:00
30m
Talk
Funky Grooves: Declarative Programming of Full-Fledged Musical Applications
PADL
Henrik Nilsson , Guerric Chupin ENSTA ParisTech
09:30
30m
Talk
DALI for Cognitive Robotics: Principles and Prototype Implementation
PADL
Stefania Costantini Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila, Giovanni De Gasperis Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Giulio Nazzicone Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica
10:00 - 10:30
Coffee breakCatering at Auditorium Hall
10:00
30m
Coffee break
Break
Catering

10:30 - 12:00
Model Checking and SynthesisVMCAI at Amphitheater 44
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
10:30
30m
Talk
Reachability for dynamic parametric processes
VMCAI
Anca Muscholl Université de Bordeaux / LaBRI, Helmut Seidl Technische Universität München, Igor Walukiewicz CNRS, LaBRI
11:00
30m
Talk
Synthesizing Non-Vacuous Systems
VMCAI
Roderick Bloem Institute of Software Technology, Graz University of Technology , Hana Chockler , ma e , Ofer Strichman Technion
File Attached
11:30
30m
Talk
Solving Nonlinear Integer Arithmetic with MCSat
VMCAI
Dejan Jovanović SRI International
10:30 - 12:00
Verified programming toolsCPP at Auditorium
10:30
30m
Talk
Verified compilation of CakeML to multiple machine-code targets
CPP
Anthony Fox University of Cambridge, UK, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan IHPC at A*STAR, Singapore, Ramana Kumar
11:00
30m
Talk
COMPLX: a verification framework for concurrent imperative programs
CPP
Sidney Amani UNSW, Australia, June Andronick Data61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin , Corey Lewis , Christine Rizkallah University of Pennsylvania, USA, Joseph Tuong
11:30
30m
Talk
Verifying dynamic race detection
CPP
William Mansky University of Pennsylvania, Yuanfeng Peng University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Joseph Devietti University of Pennsylvania
10:30 - 12:00
Session 2 PPS at Salle 105, Barre 44-54
Chair(s): Chad Scherrer Galois, Inc.
10:30
20m
Talk
An application of computable distributions to the semantics of probabilistic programs: part 2
PPS
Daniel Huang Harvard University, Greg Morrisett Cornell University
10:50
10m
Meeting
Discussion 1
PPS

11:00
20m
Talk
Probabilistic programming and a domain theoretic approach to Skorohod's theorem
PPS
11:20
10m
Meeting
Discussion 2
PPS

11:30
20m
Talk
Building inference algorithms from monad transformers
PPS
Adam Ścibior University of Cambridge, Yufei Cai University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany, Zoubin Ghahramani University of Cambridge
11:50
10m
Meeting
Discussion 3
PPS

10:30 - 12:00
10:30
30m
Talk
Cost versus Precision for Approximate Typing for Python
PEPM
Levin Fritz Utrecht University, Jurriaan Hage Utrecht University
11:00
30m
Talk
Refining types using type guards in TypeScript
PEPM
Ivo Gabe de Wolff Utrecht University, Jurriaan Hage Utrecht University
11:30
30m
Talk
Predicting Resource Consumption of Higher-Order Workflows
PEPM
Markus Klinik Radboud University Nijmegen, Jurriaan Hage Utrecht University, Jan Martin Jansen Netherlands Defence Academy, Rinus Plasmeijer Radboud University Nijmegen
10:30 - 12:00
Programming LanguagesPADL at Salle 116, Barre 44-54
10:30
30m
Talk
Improving Non-deterministic Computations in Functional Logic Programs
PADL
Sergio Antoy Kiel University, Michael Hanus Kiel University
11:00
30m
Talk
Canonicalizing High-Level Constructs in Picat
PADL
Neng-Fa Zhou CUNY Brooklyn College and Graduate Center, Jonathan Fruhman CUNY Brooklyn College
11:30
30m
Talk
An Overview of PRhoLog
PADL
Besik Dundua Institute of Applied Mathematics, Tbilisi State University, Temur Kutsia , Klaus Reisenberger-Hagmayer Johannes Kepler University Linz
12:00 - 14:00
12:00
2h
Lunch
Lunch
Catering

14:00 - 15:30
Abstract InterpretationVMCAI at Amphitheater 44
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:00
30m
Talk
Complete Abstractions and Subclassical Modal Logics
VMCAI
Vijay D'Silva Google, Marcelo Sousa University of Oxford
14:30
30m
Talk
Structuring Abstract Interpreters through State and Value Abstractions
VMCAI
David Bühler CEA LIST, Boris Yakobowski CEA - LIST, Sandrine Blazy University of Rennes 1, France
Media Attached
15:00
30m
Talk
Conjunctive Abstract Interpretation using Paramodulation
VMCAI
Mooly Sagiv Tel Aviv University, A: Or Ozeri Tel Aviv university, Oded Padon Tel Aviv University, Noam Rinetzky Tel Aviv University
Media Attached
14:00 - 15:30
Session 3 PPS at Salle 105, Barre 44-54
Chair(s): Sam Staton University of Oxford
14:00
20m
Talk
Commutativity logic for probabilistic trace equivalence: complete or not?
PPS
Paul Blain Levy , Nathan Bowler Universität Hamburg
14:20
10m
Meeting
Discussion 4
PPS

14:30
20m
Talk
Mathematical structures of probabilistic programming
PPS
Ilias Garnier University of Edinburgh, Fredrik Dahlqvist University College London, Florence Clerc McGill University, Vincent Danos ENS Paris/CNRS
14:50
10m
Meeting
Discussion 5
PPS

15:00
20m
Talk
A weakest pre-expectation semantics for mixed-sign expectations
PPS
Benjamin Lucien Kaminski RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University
15:20
10m
Meeting
Discussion 6
PPS

14:00 - 15:30
14:00
60m
Talk
Student Interaction Activity
PLMW
Eva Darulova MPI-SWS, Loris D'Antoni University of Wisconsin–Madison, Alexandra Silva University College London, Dimitrios Vytiniotis Microsoft Research, Cambridge
15:00
30m
Talk
How to Give Talks That People Can Follow
PLMW
Derek Dreyer MPI-SWS
File Attached
14:00 - 15:30
Tutorial: Partial Evaluation for Language ImplementationPEPM at Salle 109, Barre 44-54
Chair(s): Jeremy Yallop University of Cambridge, UK
14:00
90m
Talk
Practical Partial Evaluation for Language Implementation with Graal & Truffle
PEPM
15:30 - 16:00
Coffee breakCatering at Auditorium Hall
15:30
30m
Coffee break
Break
Catering

15:30 - 16:30
Poster Session PPS at Salle 105, Barre 44-54
15:30
60m
Meeting
ProbLog and applicative probabilistic programming
PPS
Alexander Vandenbroucke KU Leuven, Belgium, Tom Schrijvers KU Leuven
15:30
60m
Meeting
Encapsulating models and approximate inference programs in probabilistic modules
PPS
Marco Cusumano-Towner MIT-CSAIL, Vikash Mansinghka Massachusetts Institute of Technology
15:30
60m
Meeting
The extended semantics for probabilistic programming languages
PPS
Siddharth Srivastava UTRC Berkeley, Nicholas Hay Vicarious, Yi WU UC Berkeley, Stuart Russell University of California, Berkeley
15:30
60m
Meeting
Synthetic topology in homotopy type theory for probabilistic programming
PPS
15:30
60m
Meeting
Reasoning about inference in probabilistic programs
PPS
Chandrakana Nandi University of Washington, USA, Adrian Sampson Cornell University, Dan Grossman University of Washington, Todd Mytkowicz , Kathryn S McKinley Microsoft Research
15:30
60m
Meeting
On computable representations of exchangeable data
PPS
Nathanael L. Ackerman Harvard University, Jeremy Avigad Carnegie Mellon University, Cameron Freer Gamalon and Borelian, Daniel Roy , Jason M. Rute Pennsylvania State University
15:30
60m
Meeting
Probabilistic logic programs: unifying program trace and possible world semantics
PPS
Angelika Kimmig KU Leuven, Luc De Raedt KU Leuven
15:30
60m
Meeting
Metropolis-Hastings for mixtures of conditional distributions
PPS
15:30
60m
Meeting
Support and influence analysis for visualizing posteriors of probabilistic programs
PPS
Long Ouyang Stanford University
15:30
60m
Meeting
Efficient exact inference in discrete Anglican programs
PPS
Robert Cornish University of Oxford, Frank Wood University of Oxford, Hongseok Yang University of Oxford
16:00 - 17:30
Concurrency 2VMCAI at Amphitheater 44
Chair(s): David Monniaux CNRS, VERIMAG
16:00
30m
Talk
Using Abstract Interpretation to Correct Synchronization Faults
VMCAI
Pietro Ferrara IBM Research, Omer Tripp IBM Thomas J. Watson Research Center, Peng Liu Purdue University, Eric Koskinen Yale University
16:30
30m
Talk
Detecting All High-Level Dataraces in an RTOS Kernel.
VMCAI
Suvam Mukherjee Indian Institute of Science, Arunkumar S Indian Institute of Science, Deepak D'Souza
17:00
30m
Talk
Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
VMCAI
Raphaël Monat Ecole Normale Supérieure de Lyon, Antoine Miné UPMC, France
16:00 - 17:00
Transformation (part II)PEPM at Salle 109, Barre 44-54
Chair(s): Jurriaan Hage Utrecht University
16:00
30m
Talk
Functional Parallels of Sequential Imperatives
PEPM
Tiark Rompf Purdue University, Kevin J. Brown Stanford University
16:30
30m
Talk
A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction
PEPM
Kazutaka Matsuda , Kazuyuki Asada University of Tokyo
16:30 - 18:00
Session 5 PPS at Salle 105, Barre 44-54
Chair(s): Chung-chieh Shan Indiana University, USA
16:30
20m
Talk
An exponential family basis for probabilistic programming
PPS
Chad Scherrer Galois, Inc.
16:50
10m
Meeting
Discussion 7
PPS

17:00
20m
Talk
The semantics of subroutines and iteration in the Bayesian programming language ProBT
PPS
Raphaël Laurent ProbaYes, Kamel Mekhnacha ProbaYes, Emmanuel Mazer CNRS/LIG, Pierre Bessière CNRS/ISIR
17:20
10m
Meeting
Discussion 8
PPS

17:30
20m
Talk
Exchangeable random process and data abstraction
PPS
Sam Staton University of Oxford, Hongseok Yang University of Oxford, Nathanael L. Ackerman Harvard University, Cameron Freer Gamalon and Borelian, Daniel Roy
17:50
10m
Meeting
Discussion 9
PPS

18:15 - 19:15
Session 6 PPS at Salle 105, Barre 44-54
Chair(s): Hongseok Yang University of Oxford
18:15
20m
Talk
Reducing probabilistic choice to nondeterministic choice
PPS
Ernie Cohen Amazon Web Services
18:35
10m
Meeting
Discussion 10
PPS

18:45
20m
Talk
GraPPa: spanning the expressivity vs. efficiency continuum
PPS
Edwin Westbrook Galois, Inc., Chad Scherrer Galois, Inc., Nathan Collins Galois, Inc., Eric Mertens Galois, Inc.
19:05
10m
Meeting
Discussion 11
PPS

Wed 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05
OpeningPOPL at Auditorium
Chair(s): Giuseppe Castagna Paris Diderot University & CNRS, Andrew D. Gordon Microsoft Research and University of Edinburgh
09:00
5m
Day opening
Opening
POPL

09:05 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
09:05
55m
Talk
The Influence of Dependent Types
POPL
Stephanie Weirich University of Pennsylvania
10:00 - 10:30
Coffee breakCatering at Auditorium Hall
10:00
30m
Coffee break
Break
Catering

10:30 - 12:10
Abstract InterpretationPOPL at Amphitheater 44
Chair(s): Isabella Mastroeni University of Verona, Italy
10:30
25m
Talk
Ogre and Pythia, An invariance proof method for weak consistency models
POPL
Jade Alglave University College London, Patrick Cousot New York University
10:55
25m
Talk
A Posteriori Environment Analysis with Pushdown Delta CFA
POPL
Kimball Germane University of Utah, Matthew Might University of Utah; Harvard Medical School; The White House
11:20
25m
Talk
Semantic-Directed Clumping of Disjunctive Abstract States
POPL
Huisong Li INRIA/CNRS/ENS/PSL*, François Bérenger INRIA/CNRS/ENS/PSL*, Bor-Yuh Evan Chang University of Colorado Boulder, Xavier Rival INRIA/CNRS/ENS Paris
11:45
25m
Talk
Fast Polyhedra Abstract Domain
POPL
Gagandeep Singh ETH Zurich, Switzerland, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich
10:30 - 12:10
Type Systems 1POPL at Auditorium
Chair(s): Avik Chaudhuri Facebook
10:30
25m
Talk
Polymorphism, subtyping and type inference in MLsub
POPL
Stephen Dolan , Alan Mycroft University of Cambridge
10:55
25m
Talk
Java generics are Turing complete
POPL
Radu Grigore University of Kent
11:20
25m
Talk
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
POPL
Cyrus Omar Carnegie Mellon University, Ian Voysey Carnegie Mellon University, Michael Hilton Oregon State University, USA, Jonathan Aldrich Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder
11:45
25m
Talk
Modules, Abstraction, and Parametric Polymorphism
POPL
Karl Crary Carnegie Mellon University
12:10 - 14:20
12:10
2h10m
Lunch
Lunch
Catering

14:20 - 16:00
Probabilistic ProgrammingPOPL at Amphitheater 44
Chair(s): Marco Gaboardi SUNY Buffalo, USA
14:20
25m
Talk
Beginner's Luck: A Language for Property-Based Generators
POPL
Leonidas Lampropoulos University of Pennsylvania, Diane Gallois-Wong Inria Paris, ENS Paris, Cătălin Hriţcu Inria Paris, John Hughes Chalmers University of Technology, Benjamin C. Pierce University of Pennsylvania, Li-yao Xia ENS Paris
Pre-print
14:45
25m
Talk
Exact Bayesian Inference by Symbolic Disintegration
POPL
Chung-chieh Shan Indiana University, USA, Norman Ramsey
Pre-print
15:10
25m
Talk
Stochastic Invariants for Probabilistic Termination
POPL
Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria, Djordje Zikelic University of Cambridge
15:35
25m
Talk
Coupling proofs are probabilistic product programs
POPL
Gilles Barthe IMDEA, Benjamin Gregoire INRIA, Justin Hsu , Pierre-Yves Strub École Polytechnique
14:20 - 16:00
Concurrency 1POPL at Auditorium
Chair(s): Ilya Sergey University College London
14:20
25m
Talk
A Promising Semantics for Relaxed-Memory Concurrency
POPL
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWS
Link to publication Pre-print Media Attached
14:45
25m
Talk
Automatically Comparing Memory Consistency Models
POPL
John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UK
Pre-print Media Attached File Attached
15:10
25m
Talk
Interactive Proofs in Higher-Order Concurrent Separation Logic
POPL
Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus University
DOI Pre-print Media Attached
15:35
25m
Talk
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
POPL
Morten Krogh-Jespersen Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University
16:00 - 16:30
Coffee breakCatering at Auditorium Hall
16:00
30m
Coffee break
Break
Catering

16:30 - 17:45
LogicPOPL at Amphitheater 44
Chair(s): Alexandra Silva University College London
16:30
25m
Talk
Monadic second-order logic on finite sequences
POPL
Loris D'Antoni University of Wisconsin–Madison, Margus Veanes Microsoft Research
16:55
25m
Talk
On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
POPL
Naoki Kobayashi University of Tokyo, Japan, Etienne Lozes ENS Cachan, Florian Bruse University of Kassel
17:20
25m
Talk
Coming to Terms with Quantified Reasoning
POPL
Simon Robillard Chalmers University of Technology, Andrei Voronkov University of Manchester, Laura Kovacs Chalmers University of Technology
16:30 - 17:45
Compiler OptimisationPOPL at Auditorium
Chair(s): Andrew Myers Cornell University
16:30
25m
Talk
A Program Optimization for Automatic Database Result Caching
POPL
Ziv Scully Carnegie Mellon University, Adam Chlipala MIT
16:55
25m
Talk
Stream Fusion, to Completeness
POPL
Oleg Kiselyov , Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens
Pre-print Media Attached
17:20
25m
Talk
Rigorous Floating-point Mixed Precision Tuning
POPL
Wei-Fan Chiang School of Computing, University of Utah, Ganesh Gopalakrishnan University of Utah, Zvonimir Rakamaric University of Utah, Ian Briggs School of Computing, University of Utah, Marek S. Baranowski University of Utah, Alexey Solovyev School of Computing, University of Utah
Pre-print
19:30 - 23:00
19:30
3h30m
Dinner
Social dinner
Catering

Thu 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:15
ACM and SIGPLAN AwardsPOPL at Auditorium
Chair(s): Satnam Singh Facebook
09:00
5m
Awards
Turing Award Video
POPL

09:05
5m
Awards
Most Influential Paper Award
POPL

09:10
5m
Awards
Reynolds Doctoral Dissertation Award
POPL

09:15 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Roberto Giacobazzi University of Verona, Italy
09:15
45m
Talk
40 Years of Abstract Interpretation — An Interview with Patrick Cousot
POPL
Patrick Cousot New York University, Roberto Giacobazzi University of Verona, Italy
10:00 - 10:30
Coffee breakCatering at Auditorium Hall
10:00
30m
Coffee break
Break
Catering

10:30 - 12:10
Program AnalysisPOPL at Amphitheater 44
Chair(s): Francesco Logozzo Facebook
10:30
25m
Talk
Relational Cost Analysis
POPL
Ezgi Çiçek MPI-SWS, Germany, Gilles Barthe IMDEA, Marco Gaboardi SUNY Buffalo, USA, Deepak Garg MPI-SWS, Germany, Jan Hoffmann Carnegie Mellon University
10:55
25m
Talk
Contract-based Resource Verification for Higher-order Functions with Memoization
POPL
Ravichandhran Madhavan EPFL, Sumith Kulal IIT Bombay, Viktor Kunčak EPFL, Switzerland
11:20
25m
Talk
Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability
POPL
Qirun Zhang University of California, Davis, Zhendong Su University of California, Davis
11:45
25m
Talk
Towards Automatic Resource Bound Analysis for OCaml
POPL
Jan Hoffmann Carnegie Mellon University, Ankush Das Carnegie Mellon University, Shu-chun Weng Yale University
10:30 - 12:10
Type Systems 2POPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
10:30
25m
Talk
Deciding equivalence with sums and the empty type
POPL
Gabriel Scherer Northeastern University
10:55
25m
Talk
The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
POPL
Danko Ilik Trusted Labs
11:20
25m
Talk
Contextual isomorphisms
POPL
11:45
25m
Talk
Typed Self-Evaluation via Intensional Type Functions
POPL
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles
12:10 - 14:20
12:10
2h10m
Lunch
Lunch
Catering

14:20 - 16:00
Concurrency 2POPL at Amphitheater 44
Chair(s): Nobuko Yoshida Imperial College London, UK
14:20
25m
Talk
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
POPL
Shaked Flur University of Cambridge, Susmit Sarkar University of St. Andrews, UK, Christopher Pulte University of Cambridge, Kyndylan Nienhuis University of Cambridge, Luc Maranget INRIA Rocquencourt, Kathryn E. Gray University of Cambridge, Ali Sezgin University of Cambridge, Mark Batty University of Kent, Peter Sewell University of Cambridge
14:45
25m
Talk
Dynamic Race Detection For C++11
POPL
Christopher Lidbury Imperial College London, Alastair F. Donaldson Imperial College London
15:10
25m
Talk
Serializability for Eventual Consistency: Criterion, Analysis and Applications
POPL
Lucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH Zurich
Pre-print
15:35
25m
Talk
Thread Modularity at Many Levels: a Pearl in Compositional Verification
POPL
Jochen Hoenicke Universität Freiburg, Rupak Majumdar MPI-SWS, Andreas Podelski University of Freiburg, Germany
14:20 - 16:00
Functional Programming with EffectsPOPL at Auditorium
Chair(s): Kathleen Fisher Tufts University
14:20
25m
Talk
Type Directed Compilation of Row-Typed Algebraic Effects
POPL
Daan Leijen Microsoft Research
14:45
25m
Talk
Do be do be do
POPL
Sam Lindley University of Edinburgh, Conor McBride , Craig McLaughlin The University of Edinburgh
15:10
25m
Talk
Dijkstra Monads for Free
POPL
Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Guido Martínez CIFASIS-CONICET, Argentina, Gordon Plotkin , Jonathan Protzenko Microsoft Research, Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft Research
Pre-print
15:35
25m
Talk
Stateful Manifest Contracts
POPL
Taro Sekiyama , Atsushi Igarashi Kyoto University
16:00 - 16:30
Coffee breakCatering at Auditorium Hall
16:00
30m
Coffee break
Break
Catering

16:30 - 17:20
Semantic FoundationsPOPL at Amphitheater 44
Chair(s): Lars Birkedal Aarhus University
16:30
25m
Talk
A Semantic Account of Metric Preservation
POPL
Arthur Azevedo de Amorim University of Pennsylvania, USA, Ikram Cherigui ENS Paris, Marco Gaboardi SUNY Buffalo, USA, Justin Hsu , Shin-ya Katsumata Kyoto University
16:55
25m
Talk
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
POPL
Steffen Smolka Cornell University, Praveen Kumar Cornell University, Nate Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London
DOI File Attached
16:30 - 17:20
Logic and ProgrammingPOPL at Auditorium
Chair(s): Nada Amin EPFL
16:30
25m
Talk
Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
POPL
Kausik Subramanian University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison, Aditya Akella University of Wisconsin-Madison
16:55
25m
Talk
LOIS: syntax and semantics
POPL
17:20 - 18:20
Business meetingPOPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
17:20
20m
Talk
PC Chair report
POPL
Andrew D. Gordon Microsoft Research and University of Edinburgh
17:40
10m
Talk
POPL 2018 presentation
POPL
Andrew Myers Cornell University, Ranjit Jhala University of California, San Diego
17:50
30m
Meeting
SIGPLAN business meeting
POPL
C: Andrew D. Gordon Microsoft Research and University of Edinburgh
18:20 - 20:20
Poster SessionStudent Research Competition at Auditorium Hall
Chair(s): Matteo Cimini Indiana University, USA, Kim Nguyễn LRI, Université Paris-Sud, Julien Signoles CEA LIST, Qirun Zhang University of California, Davis
18:20
10m
Demonstration
Naturality despite Nontermination: A Logical Relation for Linear Types and Polymorphism
Student Research Competition
Nicholas Rioux Northeastern University
18:30
10m
Demonstration
Gradual Type Precision as Retraction
Student Research Competition
Max S. New Northeastern University
18:40
10m
Demonstration
Linking Types: Specifying Safe Interoperability and Equivalences
Student Research Competition
Daniel Patterson Northeastern University
18:50
10m
Demonstration
A Monadic Framework for Bidirectional Programming
Student Research Competition
Li-yao Xia ENS Paris
19:00
10m
Demonstration
Gradual Set-Theoretic Types
Student Research Competition
Victor Lanvin ENS Paris-Saclay
19:10
10m
Demonstration
Abstract Interpretation of High-Level Transformations
Student Research Competition
Ahmad Salim Al-Sibahi IT University of Copenhagen, Denmark
19:20
10m
Demonstration
FairSquare: A Static Analysis Tool for Algorithmic Fairness
Student Research Competition
Samuel Drews University of Wisconsin-Madison
19:30
10m
Demonstration
Toward Type-Preserving Compilation of Coq
Student Research Competition
William J. Bowman Northeastern University
19:40
10m
Demonstration
A Symbolic Execution Framework for Haskell
Student Research Competition
Anton Xue Yale University
19:50
10m
Demonstration
Synthesizing Imperative Programs from Examples for Introductory Programming Assignments
Student Research Competition
Sunbeom So Korea University
20:00
10m
Demonstration
Provenance for Configuration Language Security
Student Research Competition
Weili Fu University of Edinburgh
20:10
10m
Demonstration
A gradually typed polymorphic lambda calculus
Student Research Competition
Yuu Igarashi Kyoto University

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05
Student Competition AwardStudent Research Competition at Auditorium
Chair(s): Kim Nguyễn LRI, Université Paris-Sud
09:00
5m
Awards
Student Competition Award
Student Research Competition

09:05 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Giuseppe Castagna Paris Diderot University & CNRS
09:05
55m
Talk
Rust: from POPL to practice
POPL
Aaron Turon MPI-SWS
10:00 - 10:30
Coffee breakCatering at Auditorium Hall
10:00
30m
Coffee break
Break
Catering

10:30 - 12:10
Verification and SynthesisPOPL at Amphitheater 44
Chair(s): Benjamin Delaware Purdue University
10:30
25m
Talk
Component-Based Synthesis for Complex APIs
POPL
Yu Feng University of Texas at Austin, USA, Ruben Martins , Yuepeng Wang University of Texas at Austin, Işıl Dillig UT Austin, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
10:55
25m
Talk
Learning nominal automata
POPL
Joshua Moerman Radboud University, Matteo Sammartino University College London, Alexandra Silva University College London, Bartek Klin University of Warsaw, Michał Szynwelski University of Warsaw
11:20
25m
Talk
On Verifying Causal Consistency
POPL
Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea LIAFA, Université Paris Diderot, Rachid Guerraoui , Jad Hamza LIAFA, Université Paris Diderot
11:45
25m
Talk
Complexity Verification Using Guided Theorem Enumeration
POPL
Akhilesh Srikanth Georgia Institute of Technology, Burak Sahin Georgia Institute of Technology, William Harris
10:30 - 12:10
Type Systems 3POPL at Auditorium
Chair(s): Derek Dreyer MPI-SWS
10:30
25m
Talk
Intersection Type Calculi of Bounded Dimension
POPL
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
10:55
25m
Talk
Type Soundness Proofs with Definitional Interpreters
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
11:20
25m
Talk
Computational Higher-Dimensional Type Theory
POPL
Carlo Angiuli Carnegie Mellon University, Robert Harper , Todd Wilson California State University Fresno
11:45
25m
Talk
Type Systems as Macros
POPL
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University
12:10 - 14:20
12:10
2h10m
Lunch
Lunch
Catering

14:20 - 16:00
Concurrency 3POPL at Amphitheater 44
Chair(s): Adam Chlipala MIT
14:20
25m
Talk
Parallel Functional Arrays
POPL
Ananya Kumar , Guy E. Blelloch Carnegie Mellon University, Robert Harper
14:45
25m
Talk
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
POPL
Igor Konnov TU Wien, Marijana Lazić TU Wien, Helmut Veith TU Wien, Josef Widder TU Wien
DOI Pre-print
15:10
25m
Talk
Analyzing divergence in bisimulation semantics
POPL
Xinxin Liu Institute of software, Chinese academy of sciences, Tingting Yu , Wenhui Zhang Institute of software, Chinese academy of sciences
15:35
25m
Talk
Fencing off Go: Liveness and Safety for Channel-Based Programming
POPL
Julien Lange Imperial College London, Nicholas Ng Imperial College London, Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London, UK
Pre-print
14:20 - 16:00
Gradual Typing and ContractsPOPL at Auditorium
Chair(s): Ronald Garcia University of British Columbia
14:20
25m
Talk
Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
POPL
Michael Vitousek , Cameron Swords Indiana University, Jeremy G. Siek Indiana University Bloomington
14:45
25m
Talk
Gradual Refinement Types
POPL
Nicolás Lehmann , Éric Tanter University of Chile, Chile
Link to publication DOI Pre-print
15:10
25m
Talk
Automatically Generating the Dynamic Semantics of Gradually Typed Languages
POPL
Matteo Cimini Indiana University, USA, Jeremy G. Siek Indiana University Bloomington
15:35
25m
Talk
Sums of Uncertainty: Refinements go gradual
POPL
Khurram A. Jafery University of British Columbia, Jana Dunfield University of British Columbia
16:00 - 16:30
Coffee breakCatering at Auditorium Hall
16:00
30m
Coffee break
Break
Catering

16:30 - 17:45
QuantumPOPL at Amphitheater 44
Chair(s): Michele Pagani IRIF, Université Paris Diderot
16:30
25m
Talk
Invariants of Quantum Programs: Characterisations and Generation
POPL
Mingsheng Ying University of Technology Sydney, Australia, Shenggang Ying University of Technology Sydney, Australia, Xiaodi Wu University of Oregon, USA
16:55
25m
Talk
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
POPL
Ugo Dal Lago University of Bologna, France, Claudia Faggian , Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay, Akira Yoshimizu Univ.Tokyo
17:20
25m
Talk
QWIRE: A Core Language for Quantum Circuits
POPL
Jennifer Paykin , Robert Rand University of Pennsylvania, Steve Zdancewic University of Pennsylvania
16:30 - 17:45
Security and PrivacyPOPL at Auditorium
Chair(s): Cătălin Hriţcu Inria Paris
16:30
25m
Talk
LMS-Verify: Abstraction Without Regret for Verified Systems Programming
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
16:55
25m
Talk
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
POPL
Mounir Assaf Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Julien Signoles CEA LIST, Éric Totel CentraleSupélec, Frédéric Tronel CentraleSupélec
17:20
25m
Talk
LightDP: Towards Automating Differential Privacy Proofs
POPL
Danfeng Zhang Pennsylvania State University, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University

Sat 21 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:45 - 09:00
OpeningN40AI at Amphitheater 44
Chair(s): Roberto Giacobazzi University of Verona, Italy
08:45
15m
Day opening
Opening
N40AI

08:55 - 09:00
08:55
5m
Talk
Welcome
PiP

09:00 - 10:00
Industrial Panel 1N40AI at Amphitheater 44
Chair(s): Antoine Miné UPMC, France
09:00
30m
Talk
Abstract Interpretation in Absint
N40AI
09:30
30m
Talk
Abstract Interpretation in Facebook
N40AI
09:00 - 10:00
Opening SessionCoqPL at Auditorium
Chair(s): Emilio Jesús Gallego Arias MINES ParisTech
09:00
60m
Talk
Invited Talk -- Demonstration of the Iris separation logic in Coq
CoqPL
I: Robbert Krebbers Delft University of Technology, Netherlands
09:00 - 10:00
Session IRDP at Salle 107, Barre 44-54
Chair(s): Victor Vianu UC San Diego
09:00
15m
Talk
Welcome
RDP
Nate Foster Cornell University, Mooly Sagiv Tel Aviv University, Victor Vianu UC San Diego
09:15
45m
Talk
Automatic Verification of Database-Centric Workflows
RDP
10:00 - 10:30
Coffee breakCatering at Auditorium Hall
10:00
30m
Coffee break
Break
Catering

10:30 - 12:00
Industrial Panel 2 & Systems BiologyN40AI at Amphitheater 44
Chair(s): Jerome Feret INRIA Paris
10:30
30m
Talk
Abstract Interpretation in Amazon
N40AI
Byron Cook Amazon
11:00
30m
Talk
Abstract Interpretation at Galois
N40AI
Aaron Tomb Galois, Inc.
11:30
30m
Talk
Systems biology
N40AI
Vincent Danos ENS Paris/CNRS
12:00 - 14:00
12:00
2h
Lunch
Lunch
Catering

14:00 - 15:30
Security, Big Code and Synthesis N40AI at Amphitheater 44
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
14:00
30m
Talk
Security
N40AI
Michael Hicks University of Maryland at College Park, USA
14:30
30m
Talk
Big Code
N40AI
Bor-Yuh Evan Chang University of Colorado Boulder
15:00
30m
Talk
Program synthesis
N40AI
Eran Yahav Technion
14:00 - 15:30
Midday SessionCoqPL at Auditorium
Chair(s): Sandrine Blazy University of Rennes 1, France
14:00
60m
Talk
Invited Talk -- Managing Logical and Computational Complexity using Program Transformations
CoqPL
I: Nicolas Tabareau Inria, France
15:00
30m
Demonstration
Session with the Coq Development Team
CoqPL
14:00 - 15:30
Session IIIRDP at Salle 107, Barre 44-54
Chair(s): Nate Foster Cornell University
14:00
45m
Talk
Synthesizing Data-parallel Programs
RDP
Aws Albarghouthi University of Wisconsin - Madison
14:45
45m
Talk
Cosette: A Solver for SQL Equivalences
RDP
Alvin Cheung University of Washington
15:30 - 16:00
Coffee breakCatering at Auditorium Hall
15:30
30m
Coffee break
Break
Catering

16:00 - 18:30
System Verification and Patrick Cousot's KeynoteN40AI at Amphitheater 44
Chair(s): Francesco Ranzato University of Padova
16:00
30m
Talk
System verification
N40AI
Arie Gurfinkel University of Waterloo
16:30
75m
Talk
Keynote: the Next 40 years of Abstract Interpretation
N40AI
Patrick Cousot New York University
17:45
45m
Social Event
Concrete Cheese and Wine
N40AI

16:00 - 18:05
Afternoon SessionCoqPL at Auditorium
Chair(s): Matthieu Sozeau Inria
16:00
25m
Talk
Synthetic topology in HoTT for probabilistic programming
CoqPL
File Attached
16:25
25m
Talk
CertiCoq: A verified compiler for Coq
CoqPL
Abhishek Anand , Andrew W. Appel Princeton, Greg Morrisett Cornell University, Zoe Paraskevopoulou Princeton University, USA, Randy Pollack Harvard University, Olivier Savary Belanger Princeton University, Matthieu Sozeau Inria, Matthew Weaver Princeton University
File Attached
16:50
25m
Talk
CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
CoqPL
Izumi Asakura Tokyo Institute of Technology, Japan, Hidehiko Masuhara Tokyo Institute of Technology, Tomoyuki Aotani Tokyo Institute of Technology
File Attached
17:15
25m
Talk
Verification of Implementations of Distributed Systems Under Churn
CoqPL
Ryan Doenges University of Washington, James R. Wilcox University of Washington, Doug Woos University of Washington, Zachary Tatlock University of Washington, Seattle, Karl Palmskog
File Attached
17:40
25m
Talk
Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
CoqPL
File Attached
16:00 - 18:05
16:00
25m
Talk
Designing extensible, domain-specific languages for mathematical diagrams
Off the Beaten Track
Katherine Ye , Keenan Crane , Jonathan Aldrich Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University
File Attached
16:25
25m
Talk
Laziness Boxes You In
Off the Beaten Track
File Attached
16:50
25m
Talk
Programming with Epistemic Logic
Off the Beaten Track
Markus Eger , Chris Martens Carnegie Mellon University
File Attached
17:15
25m
Talk
Preventing False Discoveries in Adaptive Data Analysis: a Programming Language approach
Off the Beaten Track
Marco Gaboardi SUNY Buffalo, USA
File Attached
17:40
25m
Talk
Running Incomplete Programs
Off the Beaten Track
Ian Voysey Carnegie Mellon University, Cyrus Omar Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder
File Attached
19:00 - 21:00
19:00
2h
Social Event
CoqPL Social Event
CoqPL