Program - POPL 2017

Sun 15 - Sat 21 January 2017

Filter

Sun 15 Jan

08:50 - 10:00: TTT - First Morning Session at Salle 105, Barre 44-54
Chair(s): Assia Mahboubi

08:50 - 09:00
Day opening

09:00 - 09:20
Talk

A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method

David Thibodeau, Alberto Momigliano, Brigitte Pientka

09:20 - 09:40
Talk

Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding

Steven Keuchel, Klara Mardirosian, Tom Schrijvers

09:40 - 10:00
Talk

Equivalence of System F and λ2 in Abella

Jonas Kaiser, Gert Smolka

09:00 - 10:00: VMCAI - Invited talk 1 at Amphitheater 44
Chair(s): David Monniaux

09:00 - 10:00
Talk

Detecting Strict Aliasing Violations in the Wild

09:15 - 10:00: SCM - Session I at Salle 109, Barre 44-54

09:15 - 10:00
Talk

What is Secure Compilation? Part I

Marco Patrignani

Link to publication

10:00 - 10:30: Catering - Coffee break at Catering area

10:00 - 10:30
Coffee break

10:30 - 12:00: VMCAI - Program Analysis at Amphitheater 44
Chair(s): Boris Yakobowski

10:30 - 11:00
Talk

Partitioned Memory Models for Program Analysis.

Wei Wang, Clark Barrett, Thomas Wies

11:00 - 11:30
Talk

Property Directed Reachability for Proving Absence of Concurrent Modification Errors

Asya Frumkin, Yotam Feldman, Ondřej Lhoták, Oded Padon, Mooly Sagiv, Sharon Shoham

11:30 - 12:00
Talk

Stabilizing Floating-Point Programs using Provenance Analysis

Yijia Gu, Thomas Wahl

10:30 - 12:00: TTT - Second Morning Session at Salle 105, Barre 44-54
Chair(s): Keiko Nakata

10:30 - 11:20
Talk

Invited Talk -- Type Theory in the Software Analysis Workbench

11:20 - 11:40
Talk

Modelling Program Behaviour within Software Verification Tool LAV

Milena Vujosevic Janicic

11:40 - 12:00
Talk

agdARGS - Declarative Hierarchical Command Line Interfaces

Guillaume Allais

10:30 - 12:00: SCM - Session II at Salle 109, Barre 44-54

10:30 - 10:40
Talk

What is Secure Compilation? Part II (Short talk)

Cătălin Hriţcu

Link to publication

10:40 - 10:50
Talk

Can relational logic facilitate secure compilation? (Short talk)

10:50 - 11:00
Talk

Full Abstraction for Language Design (Short talk)

Gabriel Scherer

11:00 - 11:10
Talk

Cogent: Where we Stand and What Comes Next (Short talk)

Christine Rizkallah

11:15 - 12:00
Talk

Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities

Lau Skorstengaard

12:00 - 14:00: Catering - Buffet at Catering area

12:00 - 14:00
Lunch

14:00 - 15:30: VMCAI - Concurrency 1 at Amphitheater 44
Chair(s): Camille Coti

14:00 - 14:30
Talk

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

Igor Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi

14:30 - 15:00
Talk

Independence Abstractions and Models of Concurrency

Vijay D'Silva, Daniel Kroening, Marcelo Sousa

15:00 - 15:30
Talk

Static Analysis of Communicating Process using Symbolic Transducers

Vincent Botbol, Tristan Le Gall, Emmanuel Chailloux

Media Attached File Attached

14:00 - 15:30: TTT - First Afternoon Session at Salle 105, Barre 44-54
Chair(s): Bas Spitters

14:00 - 14:50
Talk

Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom

Anders Mörtberg

14:50 - 15:10
Talk

Equations: a tool for dependent pattern-matching

Cyprien Mangin, Matthieu Sozeau

15:10 - 15:30
Talk

Coq's Prolog and application to defining semi-automatic tactics

Théo Zimmermann, Hugo Herbelin

14:00 - 15:30: SCM - Session III at Salle 109, Barre 44-54

14:00 - 14:45
Talk

Linking Types: Secure compilation of multi-language programs

Daniel Patterson

14:45 - 15:30
Talk

Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing

Dominique Devriese

15:30 - 16:00: Catering - Coffee break at Catering area

15:30 - 16:00
Coffee break

16:00 - 17:30: VMCAI - Decision procedures at Amphitheater 44
Chair(s): Andreas Podelski

16:00 - 16:30
Talk

Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games

Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang

16:30 - 17:00
Talk

Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic

Andrew Reynolds, Radu Iosif, Cristina Serban

17:00 - 17:30
Talk

Matching multiplications in Bit-Vector formulas

Supratik Chakraborty, Ashutosh Gupta, Rahul Jain

16:00 - 18:00: TTT - Second Afternoon Session at Salle 105, Barre 44-54
Chair(s): Hugo Herbelin

16:00 - 16:50
Talk

Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq

Robbert Krebbers

16:50 - 17:10
Talk

Introducing MetaCoq: A Safe Tactic Language for Coq

17:10 - 18:00
Other

COST EUTypes session

16:00 - 17:30: SCM - Session IV at Salle 109, Barre 44-54

16:00 - 16:45
Talk

Software Fault Isolation avec CompCert

Frédéric Besson

16:45 - 17:30
Talk

Security preserving compilation of low-level programs embedded in F*

Jonathan Protzenko

Mon 16 Jan

08:50 - 09:00: PADL - Opening remarks at Salle 116, Barre 44-54
Chair(s): Yuliya Lierler, Walid Taha

08:50 - 09:00
Talk

Opening remarks

09:00 - 12:00: Tutorials - Flow (AM) at Salle 112, Barre 44-54

09:00 - 12:00
Talk

Fast and Precise Type Checking for JavaScript: Are you in Flow?

09:00 - 12:00: Tutorials - Frama-C (AM) at Salle 114, Barre 44-54

09:00 - 12:00
Talk

Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins

François Bobot, Loïc Correnson, Boris Yakobowski

09:00 - 12:00: Tutorials - Gradual Typing (AM) at Salle 105, Barre 44-54

09:00 - 12:00
Talk

The State of the Art in Gradual Typing

09:00 - 10:00: PADL - Invited Talk at Salle 116, Barre 44-54

09:00 - 10:00
Talk

Proof checking and logic programming

09:00 - 10:00: CPP - Invited Talk at Auditorium

09:00 - 10:00
Talk

Porting the HOL Light Analysis Library: Some Lessons

Lawrence Paulson

09:00 - 10:00: VMCAI - Invited talk 2 at Amphitheater 44
Chair(s): Ahmed Bouajjani

09:00 - 10:00
Talk

Verified Concurrent Code: Tricks of the Trade

09:00 - 10:00: PEPM 2017 - Keynote at Salle 109, Barre 44-54
Chair(s): Ulrik Schultz

09:00 - 10:00
Talk

Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk)

Daniil Berezun, Neil D. Jones

09:00 - 12:00: Tutorials - Lean (AM) at Salle 107, Barre 44-54

09:00 - 12:00
Talk

The Lean Theorem Prover

Leonardo De Moura, Gabriel Ebner, Jared Roesch, Sebastian Ullrich

10:00 - 10:30: Catering - Coffee break at Auditorium Hall

10:00 - 10:30
Coffee break

10:30 - 12:00: CPP - Algorithm and library verification at Auditorium

10:30 - 11:00
Talk

Verifying a hash table and its iterators in higher-order separation logic

François Pottier

11:00 - 11:30
Talk

A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

11:30 - 12:00
Talk

Formal foundations of 3D geometry for modeling robot manipulators

Reynald Affeldt, Cyril Cohen

10:30 - 12:00: PADL - Answer Set Programming at Salle 116, Barre 44-54

10:30 - 11:00
Talk

Lowering the learning curve for declarative programming: a Python API for the IDP system

Joost Vennekens

11:00 - 11:30
Talk

Extending Answer Set Programs with Interpreted Functions as First-class Citizens

11:30 - 12:00
Talk

Integrating Answer Set Programming with Object-oriented Languages

Jakob Rath, Christoph Redl

10:30 - 12:00: VMCAI - Numerical domains at Amphitheater 44
Chair(s): Laure Gonnord

10:30 - 11:00
Talk

Sound Bit-Precise Numerical Domains

Tushar Sharma, Thomas Reps

11:00 - 11:30
Talk

Efficient Elimination of Redundancies in Polyhedra using Raytracing

Alexandre Maréchal, Michael Perin

Media Attached File Attached

11:30 - 12:00
Talk

Finding Relevant Templates via the Principal Component Analysis

Yassamine Seladji

10:30 - 12:00: PEPM 2017 - Programming languages at Salle 109, Barre 44-54
Chair(s): Andrew Farmer

10:30 - 11:00
Talk

Lightweight Soundness for Towers of Language Extensions

Alejandro Serrano, Jurriaan Hage

11:00 - 11:30
Talk

Detecting code clones with gaps by function applications

Tsubasa Matsushita, Isao Sasano

11:30 - 12:00
Talk

PEG Parsing in Less Space Using Progressive Tabling and Dynamic Analysis

Fritz Henglein, Ulrik Terp Rasmussen

12:00 - 14:00: Catering - Buffet at Catering area

12:00 - 14:00
Lunch

14:00 - 15:30: CPP - Automated proof and its verification at Auditorium

14:00 - 14:30
Talk

BliStrTune: Hierarchical Invention of Theorem Proving Strategies

Jan Jakubuv, Josef Urban

14:30 - 15:00
Talk

Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic

Reuben Rowe, James Brotherston

15:00 - 15:30
Talk

Formalization of Karp-Miller Tree Construction on Petri Nets

Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto

14:00 - 17:00: Tutorials - Flow (PM) at Salle 112, Barre 44-54

14:00 - 17:00
Talk

Fast and Precise Type Checking for JavaScript: Are you in Flow?

14:00 - 17:00: Tutorials - Frama-C (PM) at Salle 114, Barre 44-54

14:00 - 17:00
Talk

Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins

François Bobot, Loïc Correnson, Boris Yakobowski

14:00 - 17:00: Tutorials - Gradual Typing (PM) at Salle 105, Barre 44-54

14:00 - 17:00
Talk

The State of the Art in Gradual Typing

14:00 - 17:00: Tutorials - Lean (PM) at Salle 107, Barre 44-54

14:00 - 17:00
Talk

The Lean Theorem Prover

Leonardo De Moura, Gabriel Ebner, Jared Roesch, Sebastian Ullrich

14:00 - 15:30: VMCAI - Model-checking and bug finding at Amphitheater 44
Chair(s): Andreas Podelski

14:00 - 14:30
Talk

Effective Bug Finding in C Programs with Shape and Effect Abstraction

Iago Abal, Claus Brabrand, Andrzej Wąsowski

14:30 - 15:00
Talk

Reduction of Workflow Nets for Generalised Soundness Verification

Hadrien Bride, Olga Kouchnarenko, Fabien Peureux

15:00 - 15:30
Talk

Dynamic Reductions for Model Checking Concurrent Software.

Henning Günther, Alfons Laarman, Ana Sokolova, Georg Weissenbacher

14:00 - 15:30: PADL - Testing and Games at Salle 116, Barre 44-54

14:00 - 14:30
Talk

Failing Faster: Overlapping Patterns for Property-Based Testing

Jonathan Fowler, Graham Hutton

14:30 - 15:00
Talk

Boltzmann Samplers for Closed Simply-Typed Lambda Terms

Maciej Bendkowski, Katarzyna Grygiel, Paul Tarau

15:00 - 15:30
Talk

Selection Equilibria of Higher-Order Games

Paulo Oliva, Jules Hedges, Viktor Winschel, Philipp Zahn, Evguenia Shprits

14:00 - 15:30: PEPM 2017 - Tutorial (Idris, Inside-Out) and Poster Session at Salle 109, Barre 44-54
Chair(s): Ulrik Schultz, Jeremy Yallop

14:00 - 15:00
Talk

Idris, Inside-Out: A Tutorial on Extending Idris in Idris

David Christiansen

15:00 - 15:30
Talk

Invited posters

Nada Amin, Tiark Rompf, Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis

15:00 - 15:30
Talk

Language-integrated Query with Ordering, Grouping and Outer Joins (poster)

Tatsuya Katsushima, Oleg Kiselyov

15:30 - 16:00: Catering - Coffee break at Auditorium Hall

15:30 - 16:00
Coffee break

16:00 - 17:30: PADL - Applications I and Inference at Salle 116, Barre 44-54

16:00 - 16:30
Talk

A Domain-Specific Language for Software-Defined Radio

Geoffrey Mainland

16:30 - 17:00
Talk

A Declarative DSL for Customized Rendering of Text-Based Art

17:00 - 17:30
Talk

Using Iterative Deepening for Probabilistic Logic Inference

Theofrastos Mantadelis, Ricardo Rocha

16:00 - 18:00: CPP - Formalized mathematics with numerical computations at Auditorium

16:00 - 16:30
Talk

A Coq Formal Proof of the Lax–Milgram theorem

Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero

16:30 - 17:00
Talk

A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations

Erik Martin-Dorel, Pierre Roux

17:00 - 17:30
Talk

Markov Processes in Isabelle/HOL

Johannes Hölzl

DOI Pre-print File Attached

17:30 - 18:00
Talk

Formalising Real Numbers in Homotopy Type Theory

16:00 - 17:30: VMCAI - Symbolic analysis and invariant synthesis at Amphitheater 44
Chair(s): Constantin Enea

16:00 - 16:30
Talk

Block-wise abstract interpretation by combining abstract domains with SMT

Jiahong Jiang, Liqian Chen, Xueguang Wu, Ji Wang

16:30 - 17:00
Talk

IC3 - Flipping the E in ICE

Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik

17:00 - 17:30
Talk

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

Lukas Holik, Martin Hruska, Ondrej Lengal, Adam Rogalewicz, Tomas Vojnar

16:00 - 17:00: PEPM 2017 - Transformation (part I) at Salle 109, Barre 44-54
Chair(s): Chung-chieh Shan

16:00 - 16:30
Talk

Verification of Code Generators via Higher-Order Model Checking

Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi

16:30 - 17:00
Talk

Interactive data representation migration: Exploiting program dependence to aid program transformation

Krishna Narasimhan, Julia Lawall, Christoph Reichenbach

19:30 - 22:00: VMCAI - Banquet at Procope

Tue 17 Jan

08:50 - 09:00: PLMW - Welcome Session at Salle 107, Barre 44-54

08:50 - 09:00
Day opening

Welcome Sesssion

09:00 - 10:00: PADL - Applications II at Salle 116, Barre 44-54

09:00 - 09:30
Talk

Funky Grooves: Declarative Programming of Full-Fledged Musical Applications

Henrik Nilsson, Guerric Chupin

09:30 - 10:00
Talk

DALI for Cognitive Robotics: Principles and Prototype Implementation

Stefania Costantini, Giovanni De Gasperis, Giulio Nazzicone

09:00 - 10:00: CPP - Invited Talk at Auditorium

09:00 - 10:00
Talk

Mechanized verification of preemptive OS kernels

09:00 - 10:00: VMCAI - Invited talk 3 at Amphitheater 44
Chair(s): Andreas Podelski

09:00 - 10:00
Talk

Verification of Cancer Programs

09:00 - 10:00: PPS - Session 1 at Salle 105, Barre 44-54
Chair(s): Cameron Freer

09:00 - 10:00
Talk

Towards a metric semantics for probabilistic programming (invited talk)

09:00 - 10:00: PLMW - Session I at Salle 107, Barre 44-54

09:00 - 09:30
Talk

Time management, family and quality of life

Kathleen Fisher

09:30 - 10:00
Talk

Abductive Reasoning in Deductive Verification

09:00 - 10:00: PEPM 2017 - Tutorial: reversible computing at Salle 109, Barre 44-54
Chair(s): Ulrik Schultz

09:00 - 10:00
Talk

Reversible computing from a programming language perspective

10:00 - 10:30: Catering - Coffee break at Auditorium Hall

10:00 - 10:30
Coffee break

10:30 - 12:00: VMCAI - Model Checking and Synthesis at Amphitheater 44
Chair(s): Ahmed Bouajjani

10:30 - 11:00
Talk

Reachability for dynamic parametric processes

Anca Muscholl, Helmut Seidl, Igor Walukiewicz

11:00 - 11:30
Talk

Synthesizing Non-Vacuous Systems

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman

11:30 - 12:00
Talk

Solving Nonlinear Integer Arithmetic with MCSat

Dejan Jovanović

10:30 - 12:00: PADL - Programming Languages at Salle 116, Barre 44-54

10:30 - 11:00
Talk

Improving Non-deterministic Computations in Functional Logic Programs

Sergio Antoy, Michael Hanus

11:00 - 11:30
Talk

Canonicalizing High-Level Constructs in Picat

Neng-Fa Zhou, Jonathan Fruhman

11:30 - 12:00
Talk

An Overview of PRhoLog

Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayer

10:30 - 12:00: PPS - Session 2 at Salle 105, Barre 44-54
Chair(s): Chad Scherrer

10:30 - 10:50
Talk

An application of computable distributions to the semantics of probabilistic programs: part 2

Daniel Huang, Greg Morrisett

10:50 - 11:00
Meeting

11:00 - 11:20
Talk

Probabilistic programming and a domain theoretic approach to Skorohod's theorem

Michael Mislove

11:20 - 11:30
Meeting

11:30 - 11:50
Talk

Building inference algorithms from monad transformers

Adam Ścibior, Yufei Cai, Klaus Ostermann, Zoubin Ghahramani

11:50 - 12:00
Meeting

10:30 - 12:00: PLMW - Session II at Salle 107, Barre 44-54

10:30 - 11:00
Talk

What is research and how to do it? Thinking globally and acting locally.

11:00 - 11:30
Talk

Mechanizing Meta-Theory in Beluga

Brigitte Pientka

11:30 - 12:00
Talk

Research: The Industrial Culture

10:30 - 12:00: PEPM 2017 - Types at Salle 109, Barre 44-54
Chair(s): Robert Glück

10:30 - 11:00
Talk

Cost versus Precision for Approximate Typing for Python

Levin Fritz, Jurriaan Hage

11:00 - 11:30
Talk

Refining types using type guards in TypeScript

Ivo Gabe de Wolff, Jurriaan Hage

11:30 - 12:00
Talk

Predicting Resource Consumption of Higher-Order Workflows

Markus Klinik, Jurriaan Hage, Jan Martin Jansen, Rinus Plasmeijer

10:30 - 12:00: CPP - Verified programming tools at Auditorium

10:30 - 11:00
Talk

Verified compilation of CakeML to multiple machine-code targets

Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar

11:00 - 11:30
Talk

COMPLX: a verification framework for concurrent imperative programs

Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong

11:30 - 12:00
Talk

Verifying dynamic race detection

William Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti

12:00 - 14:00: Catering - Buffet at Catering area

12:00 - 14:00
Lunch

14:00 - 15:30: VMCAI - Abstract Interpretation at Amphitheater 44
Chair(s): Roberto Giacobazzi

14:00 - 14:30
Talk

Complete Abstractions and Subclassical Modal Logics

Vijay D'Silva, Marcelo Sousa

14:30 - 15:00
Talk

Structuring Abstract Interpreters through State and Value Abstractions

David Bühler, Boris Yakobowski, Sandrine Blazy

15:00 - 15:30
Talk

Conjunctive Abstract Interpretation using Paramodulation

Mooly Sagiv, Or Ozeri, Oded Padon, Noam Rinetzky

14:00 - 15:30: CPP - Homotopy type theory at Auditorium

14:00 - 14:30
Talk

The HoTT library: a formalization of homotopy type theory in Coq

Andrej Bauer, Jason Gross, Peter Lefanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters

14:30 - 15:00
Talk

Lifting proof-relevant unification to higher dimensions

Jesper Cockx, Dominique Devriese

15:00 - 15:30
Talk

The Next 700 Syntactical models of type theory

Simon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau

14:00 - 15:30: PPS - Session 3 at Salle 105, Barre 44-54
Chair(s): Sam Staton

14:00 - 14:20
Talk

Commutativity logic for probabilistic trace equivalence: complete or not?

Paul Blain Levy, Nathan Bowler

14:20 - 14:30
Meeting

14:30 - 14:50
Talk

Mathematical structures of probabilistic programming

Ilias Garnier, Fredrik Dahlqvist, Florence Clerc, Vincent Danos

14:50 - 15:00
Meeting

15:00 - 15:20
Talk

A weakest pre-expectation semantics for mixed-sign expectations

Benjamin Lucien Kaminski, Joost-Pieter Katoen

15:20 - 15:30
Meeting

14:00 - 15:30: PLMW - Session III at Salle 107, Barre 44-54

14:00 - 15:00
Talk

Student Interaction Activity

Eva Darulova, Loris D'Antoni, Alexandra Silva, Dimitrios Vytiniotis

15:00 - 15:30
Talk

How to Give Talks That People Can Follow

14:00 - 15:30: PEPM 2017 - Tutorial: Partial Evaluation for Language Implementation at Salle 109, Barre 44-54
Chair(s): Jeremy Yallop

14:00 - 15:30
Talk

Practical Partial Evaluation for Language Implementation with Graal & Truffle

15:30 - 16:00: Catering - Coffee break at Auditorium Hall

15:30 - 16:00
Coffee break

15:30 - 16:30: PPS - Poster Session at Salle 105, Barre 44-54

15:30 - 16:30
Meeting

ProbLog and applicative probabilistic programming

Alexander Vandenbroucke, Tom Schrijvers

15:30 - 16:30
Meeting

Encapsulating models and approximate inference programs in probabilistic modules

Marco Cusumano-Towner, Vikash Mansinghka

15:30 - 16:30
Meeting

The extended semantics for probabilistic programming languages

Siddharth Srivastava, Nicholas Hay, Yi WU, Stuart Russell

15:30 - 16:30
Meeting

Synthetic topology in homotopy type theory for probabilistic programming

Florian Faissole, Bas Spitters

15:30 - 16:30
Meeting

Reasoning about inference in probabilistic programs

Chandrakana Nandi, Adrian Sampson, Dan Grossman, Todd Mytkowicz, Kathryn S McKinley

15:30 - 16:30
Meeting

On computable representations of exchangeable data

Nathanael L. Ackerman, Jeremy Avigad, Cameron Freer, Daniel Roy, Jason M. Rute

15:30 - 16:30
Meeting

Probabilistic logic programs: unifying program trace and possible world semantics

Angelika Kimmig, Luc De Raedt

15:30 - 16:30
Meeting

Metropolis-Hastings for mixtures of conditional distributions

15:30 - 16:30
Meeting

Support and influence analysis for visualizing posteriors of probabilistic programs

15:30 - 16:30
Meeting

Efficient exact inference in discrete Anglican programs

Robert Cornish, Frank Wood, Hongseok Yang

16:00 - 17:30: VMCAI - Concurrency 2 at Amphitheater 44
Chair(s): David Monniaux

16:00 - 16:30
Talk

Using Abstract Interpretation to Correct Synchronization Faults

Pietro Ferrara, Omer Tripp, Peng Liu, Eric Koskinen

16:30 - 17:00
Talk

Detecting All High-Level Dataraces in an RTOS Kernel.

Suvam Mukherjee, Arunkumar S, Deepak D'Souza

17:00 - 17:30
Talk

Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions

Raphaël Monat, Antoine Miné

16:00 - 17:30: CPP - Formal verification of programming language foundations at Auditorium

16:00 - 16:30
Talk

Type-and-scope safe programs and their proofs

Guillaume Allais, James Chapman, Conor McBride, James McKinna

16:30 - 17:00
Talk

Formally verified differential dynamic logic

Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Voelp, André Platzer

17:00 - 17:30
Talk

Equivalence of System F and λ2 in Coq based on context morphism lemmas

Jonas Kaiser, Tobias Tebbi, Gert Smolka

16:00 - 18:00: PLMW - Session IV at Salle 107, Barre 44-54

16:00 - 16:30
Talk

Machine Learning and Programming Languages: latest directions and research opportunities

16:30 - 17:00
Talk

The Curse of Knowledge

Benjamin C. Pierce

17:00 - 18:00
Talk

Young Researcher Panel Session

Roopsha Samanta, Nada Amin, Jonathan Protzenko, Zachary Kincaid

16:00 - 17:00: PEPM 2017 - Transformation (part II) at Salle 109, Barre 44-54
Chair(s): Jurriaan Hage

16:00 - 16:30
Talk

Functional Parallels of Sequential Imperatives

Tiark Rompf, Kevin J. Brown

16:30 - 17:00
Talk

A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction

Kazutaka Matsuda, Kazuyuki Asada

16:30 - 18:00: PPS - Session 5 at Salle 105, Barre 44-54
Chair(s): Chung-chieh Shan

16:30 - 16:50
Talk

An exponential family basis for probabilistic programming

16:50 - 17:00
Meeting

17:00 - 17:20
Talk

The semantics of subroutines and iteration in the Bayesian programming language ProBT

Raphaël Laurent, Kamel Mekhnacha, Emmanuel Mazer, Pierre Bessière

17:20 - 17:30
Meeting

17:30 - 17:50
Talk

Exchangeable random process and data abstraction

Sam Staton, Hongseok Yang, Nathanael L. Ackerman, Cameron Freer, Daniel Roy

17:50 - 18:00
Meeting

18:15 - 19:15: PPS - Session 6 at Salle 105, Barre 44-54
Chair(s): Hongseok Yang

18:15 - 18:35
Talk

Reducing probabilistic choice to nondeterministic choice

18:35 - 18:45
Meeting

18:45 - 19:05
Talk

GraPPa: spanning the expressivity vs. efficiency continuum

Edwin Westbrook, Chad Scherrer, Nathan Collins, Eric Mertens

19:05 - 19:15
Meeting

Wed 18 Jan

09:00 - 09:05: POPL - Opening at Auditorium
Chair(s): Giuseppe Castagna, Andrew D. Gordon

09:00 - 09:05
Day opening

09:05 - 10:00: POPL - Invited speaker at Auditorium
Chair(s): Andrew D. Gordon

09:05 - 10:00
Talk

The Influence of Dependent Types

Stephanie Weirich

10:00 - 10:30: Catering - Coffee break at Auditorium Hall

10:00 - 10:30
Coffee break

10:30 - 12:10: POPL - Abstract Interpretation at Amphitheater 44
Chair(s): Isabella Mastroeni

10:30 - 10:55
Talk

Ogre and Pythia, An invariance proof method for weak consistency models

Jade Alglave, Patrick Cousot

10:55 - 11:20
Talk

A Posteriori Environment Analysis with Pushdown Delta CFA

Kimball Germane, Matthew Might

11:20 - 11:45
Talk

Semantic-Directed Clumping of Disjunctive Abstract States

Huisong Li, François Bérenger, Bor-Yuh Evan Chang, Xavier Rival

11:45 - 12:10
Talk

Fast Polyhedra Abstract Domain

Gagandeep Singh, Markus Püschel, Martin Vechev

10:30 - 12:10: POPL - Type Systems 1 at Auditorium
Chair(s): Avik Chaudhuri

10:30 - 10:55
Talk

Polymorphism, subtyping and type inference in MLsub

Stephen Dolan, Alan Mycroft

10:55 - 11:20
Talk

Java generics are Turing complete

11:20 - 11:45
Talk

Hazelnut: A Bidirectionally Typed Structure Editor Calculus

Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew Hammer

11:45 - 12:10
Talk

Modules, Abstraction, and Parametric Polymorphism

12:10 - 14:20: Catering - Buffet at Catering area

12:10 - 14:20
Lunch

14:20 - 16:00: POPL - Concurrency 1 at Auditorium
Chair(s): Ilya Sergey

14:20 - 14:45
Talk

A Promising Semantics for Relaxed-Memory Concurrency

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer

Link to publication Pre-print Media Attached

14:45 - 15:10
Talk

Automatically Comparing Memory Consistency Models

John Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides

Pre-print Media Attached File Attached

15:10 - 15:35
Talk

Interactive Proofs in Higher-Order Concurrent Separation Logic

Robbert Krebbers, Amin Timany, Lars Birkedal

DOI Pre-print Media Attached

15:35 - 16:00
Talk

A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic

Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal

14:20 - 16:00: POPL - Probabilistic Programming at Amphitheater 44
Chair(s): Marco Gaboardi

14:20 - 14:45
Talk

Beginner's Luck: A Language for Property-Based Generators

Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Li-yao Xia

14:45 - 15:10
Talk

Exact Bayesian Inference by Symbolic Disintegration

Chung-chieh Shan, Norman Ramsey

15:10 - 15:35
Talk

Stochastic Invariants for Probabilistic Termination

Krishnendu Chatterjee, Petr Novotny, Djordje Zikelic

15:35 - 16:00
Talk

Coupling proofs are probabilistic product programs

Gilles Barthe, Benjamin Gregoire, Justin Hsu, Pierre-Yves Strub

16:00 - 16:30: Catering - Coffee break at Auditorium Hall

16:00 - 16:30
Coffee break

16:30 - 17:45: POPL - Compiler Optimisation at Auditorium
Chair(s): Andrew Myers

16:30 - 16:55
Talk

A Program Optimization for Automatic Database Result Caching

Ziv Scully, Adam Chlipala

16:55 - 17:20
Talk

Stream Fusion, to Completeness

Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis

Pre-print Media Attached

17:20 - 17:45
Talk

Rigorous Floating-point Mixed Precision Tuning

Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Ian Briggs, Marek S. Baranowski, Alexey Solovyev

16:30 - 17:45: POPL - Logic at Amphitheater 44
Chair(s): Alexandra Silva

16:30 - 16:55
Talk

Monadic second-order logic on finite sequences

Loris D'Antoni, Margus Veanes

16:55 - 17:20
Talk

On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic

Naoki Kobayashi, Etienne Lozes, Florian Bruse

17:20 - 17:45
Talk

Coming to Terms with Quantified Reasoning

Simon Robillard, Andrei Voronkov, Laura Kovacs

19:30 - 23:00: Catering - Social dinner at Musée des Arts Forains

19:30 - 23:00
Dinner

Thu 19 Jan

09:00 - 09:15: POPL - ACM and SIGPLAN Awards at Auditorium
Chair(s): Satnam Singh

09:00 - 09:05
Awards

Turing Award Video

09:05 - 09:10
Awards

Most Influential Paper Award

09:10 - 09:15
Awards

Reynolds Doctoral Dissertation Award

09:15 - 10:00: POPL - Invited speaker at Auditorium
Chair(s): Roberto Giacobazzi

09:15 - 10:00
Talk

40 Years of Abstract Interpretation — An Interview with Patrick Cousot

Patrick Cousot, Roberto Giacobazzi

10:00 - 10:30: Catering - Coffee break at Auditorium Hall

10:00 - 10:30
Coffee break

10:30 - 12:10: POPL - Program Analysis at Amphitheater 44
Chair(s): Francesco Logozzo

10:30 - 10:55
Talk

Relational Cost Analysis

Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann

10:55 - 11:20
Talk

Contract-based Resource Verification for Higher-order Functions with Memoization

Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak

11:20 - 11:45
Talk

Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability

Qirun Zhang, Zhendong Su

11:45 - 12:10
Talk

Towards Automatic Resource Bound Analysis for OCaml

Jan Hoffmann, Ankush Das, Shu-Chun Weng

10:30 - 12:10: POPL - Type Systems 2 at Auditorium
Chair(s): Andrew D. Gordon

10:30 - 10:55
Talk

Deciding equivalence with sums and the empty type

Gabriel Scherer

10:55 - 11:20
Talk

The exp-log normal form of types: Decomposing extensional equality and representing terms compactly

11:20 - 11:45
Talk

Contextual isomorphisms

Paul Blain Levy

11:45 - 12:10
Talk

Typed Self-Evaluation via Intensional Type Functions

Matt Brown, Jens Palsberg

12:10 - 14:20: Catering - Buffet at Catering area

12:10 - 14:20
Lunch

14:20 - 16:00: POPL - Concurrency 2 at Amphitheater 44
Chair(s): Nobuko Yoshida

14:20 - 14:45
Talk

Mixed-size Concurrency: ARM, POWER, C/C++11, and SC

Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell

14:45 - 15:10
Talk

Dynamic Race Detection For C++11

Christopher Lidbury, Alastair Donaldson

15:10 - 15:35
Talk

Serializability for Eventual Consistency: Criterion, Analysis and Applications

Lucas Brutschy, Dimitar Dimitrov, Peter Müller, Martin Vechev

15:35 - 16:00
Talk

Thread Modularity at Many Levels: a Pearl in Compositional Verification

Jochen Hoenicke, Rupak Majumdar, Andreas Podelski

14:20 - 16:00: POPL - Functional Programming with Effects at Auditorium
Chair(s): Kathleen Fisher

14:20 - 14:45
Talk

Type Directed Compilation of Row-Typed Algebraic Effects

14:45 - 15:10
Talk

Sam Lindley, Conor McBride, Craig McLaughlin

15:10 - 15:35
Talk

Dijkstra Monads for Free

Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

15:35 - 16:00
Talk

Stateful Manifest Contracts

Taro Sekiyama, Atsushi Igarashi

16:00 - 16:30: Catering - Coffee break at Auditorium Hall

16:00 - 16:30
Coffee break

16:30 - 17:20: POPL - Logic and Programming at Auditorium
Chair(s): Nada Amin

16:30 - 16:55
Talk

Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks

Kausik Subramanian, Loris D'Antoni, Aditya Akella

16:55 - 17:20
Talk

LOIS: syntax and semantics

Eryk Kopczynski, Szymon Toruńczyk

16:30 - 17:20: POPL - Semantic Foundations at Amphitheater 44
Chair(s): Lars Birkedal

16:30 - 16:55
Talk

A Semantic Account of Metric Preservation

Arthur Azevedo de Amorim, Ikram Cherigui, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata

16:55 - 17:20
Talk

Cantor Meets Scott: Semantic Foundations for Probabilistic Networks

Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva

DOI File Attached

17:20 - 18:20: POPL - Business meeting at Auditorium
Chair(s): Andrew D. Gordon

17:20 - 17:40
Talk

PC Chair report

Andrew D. Gordon

17:40 - 17:50
Talk

POPL 2018 presentation

Andrew Myers, Ranjit Jhala

17:50 - 18:20
Meeting

SIGPLAN business meeting

Andrew D. Gordon

18:20 - 20:20: Student Research Competition - Poster Session at Auditorium Hall
Chair(s): Qirun Zhang, Matteo Cimini, Julien Signoles, Kim Nguyễn

18:20 - 18:30
Demonstration

Naturality despite Nontermination: A Logical Relation for Linear Types and Polymorphism

18:30 - 18:40
Demonstration

Gradual Type Precision as Retraction

18:40 - 18:50
Demonstration

Linking Types: Specifying Safe Interoperability and Equivalences

Daniel Patterson

18:50 - 19:00
Demonstration

A Monadic Framework for Bidirectional Programming

19:00 - 19:10
Demonstration

Gradual Set-Theoretic Types

19:10 - 19:20
Demonstration

Abstract Interpretation of High-Level Transformations

Ahmad Salim Al-Sibahi

19:20 - 19:30
Demonstration

FairSquare: A Static Analysis Tool for Algorithmic Fairness

19:30 - 19:40
Demonstration

Toward Type-Preserving Compilation of Coq

William J. Bowman

19:40 - 19:50
Demonstration

A Symbolic Execution Framework for Haskell

19:50 - 20:00
Demonstration

Synthesizing Imperative Programs from Examples for Introductory Programming Assignments

20:00 - 20:10
Demonstration

Provenance for Configuration Language Security

20:10 - 20:20
Demonstration

A gradually typed polymorphic lambda calculus

Fri 20 Jan

09:00 - 09:05: Student Research Competition - Student Competition Award at Auditorium
Chair(s): Kim Nguyễn

09:00 - 09:05
Awards

Student Competition Award

09:05 - 10:00: POPL - Invited speaker at Auditorium
Chair(s): Giuseppe Castagna

09:05 - 10:00
Talk

Rust: from POPL to practice

10:00 - 10:30: Catering - Coffee break at Auditorium Hall

10:00 - 10:30
Coffee break

10:30 - 12:10: POPL - Type Systems 3 at Auditorium
Chair(s): Derek Dreyer

10:30 - 10:55
Talk

Intersection Type Calculi of Bounded Dimension

Andrej Dudenhefner, Jakob Rehof

10:55 - 11:20
Talk

Type Soundness Proofs with Definitional Interpreters

Nada Amin, Tiark Rompf

11:20 - 11:45
Talk

Computational Higher-Dimensional Type Theory

Carlo Angiuli, Robert Harper, Todd Wilson

11:45 - 12:10
Talk

Type Systems as Macros

Stephen Chang, Alex Knauth, Ben Greenman

10:30 - 12:10: POPL - Verification and Synthesis at Amphitheater 44
Chair(s): Benjamin Delaware

10:30 - 10:55
Talk

Component-Based Synthesis for Complex APIs

Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas Reps

10:55 - 11:20
Talk

Learning nominal automata

Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, Michał Szynwelski

11:20 - 11:45
Talk

On Verifying Causal Consistency

Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza

11:45 - 12:10
Talk

Complexity Verification Using Guided Theorem Enumeration

Akhilesh Srikanth, Burak Sahin, William Harris

12:10 - 14:20: Catering - Buffet at Catering area

12:10 - 14:20
Lunch

14:20 - 16:00: POPL - Concurrency 3 at Amphitheater 44
Chair(s): Adam Chlipala

14:20 - 14:45
Talk

Parallel Functional Arrays

Ananya Kumar, Guy E. Blelloch, Robert Harper

14:45 - 15:10
Talk

A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms

Igor Konnov, Marijana Lazić, Helmut Veith, Josef Widder

15:10 - 15:35
Talk

Analyzing divergence in bisimulation semantics

Xinxin Liu, Tingting Yu, Wenhui Zhang

15:35 - 16:00
Talk

Fencing off Go: Liveness and Safety for Channel-Based Programming

Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida

14:20 - 16:00: POPL - Gradual Typing and Contracts at Auditorium
Chair(s): Ronald Garcia

14:20 - 14:45
Talk

Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System

Michael Vitousek, Cameron Swords, Jeremy G. Siek

14:45 - 15:10
Talk

Gradual Refinement Types

Nicolás Lehmann, Éric Tanter

Link to publication DOI Pre-print

15:10 - 15:35
Talk

Automatically Generating the Dynamic Semantics of Gradually Typed Languages

Matteo Cimini, Jeremy G. Siek

15:35 - 16:00
Talk

Sums of Uncertainty: Refinements go gradual

Khurram A. Jafery, Joshua Dunfield

16:00 - 16:30: Catering - Coffee break at Auditorium Hall

16:00 - 16:30
Coffee break

16:30 - 17:45: POPL - Quantum at Amphitheater 44
Chair(s): Michele Pagani

16:30 - 16:55
Talk

Invariants of Quantum Programs: Characterisations and Generation

Mingsheng Ying, Shenggang Ying, Xiaodi Wu

16:55 - 17:20
Talk

The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects

Ugo Dal Lago, Claudia Faggian, Benoit Valiron, Akira Yoshimizu

17:20 - 17:45
Talk

QWIRE: A Core Language for Quantum Circuits

Jennifer Paykin, Robert Rand, Steve Zdancewic

16:30 - 17:45: POPL - Security and Privacy at Auditorium
Chair(s): Cătălin Hriţcu

16:30 - 16:55
Talk

LMS-Verify: Abstraction Without Regret for Verified Systems Programming

Nada Amin, Tiark Rompf

16:55 - 17:20
Talk

Hypercollecting Semantics and its Application to Static Analysis of Information Flow

Mounir Assaf, David Naumann, Julien Signoles, Éric Totel, Frédéric Tronel

17:20 - 17:45
Talk

LightDP: Towards Automating Differential Privacy Proofs

Danfeng Zhang, Daniel Kifer

Sat 21 Jan

08:45 - 09:00: Next 40 years of Abstract Interpretation - Opening at Amphitheater 44
Chair(s): Roberto Giacobazzi

08:45 - 09:00
Day opening

08:55 - 09:00: PiP 2017 - Welcome at Salle 105, Barre 44-54

08:55 - 09:00
Talk

09:00 - 10:00: Next 40 years of Abstract Interpretation - Industrial Panel 1 at Amphitheater 44
Chair(s): Antoine Miné

09:00 - 09:30
Talk

Abstract Interpretation in Absint

Christian Ferdinand

09:30 - 10:00
Talk

Abstract Interpretation in Facebook

Francesco Logozzo

09:00 - 10:00: CoqPL 2017 - Opening Session at Auditorium
Chair(s): Emilio Jesús Gallego Arias

09:00 - 10:00
Talk

Invited Talk -- Demonstration of the Iris separation logic in Coq

Robbert Krebbers

09:00 - 10:00: PiP 2017 - Session 1 at Salle 105, Barre 44-54

09:00 - 09:30
Talk

Andrew Kennedy (Facebook) Static type checking for PHP

09:30 - 10:00
Talk

Jean-Louis Colaco (Ansys - Esterel Technologies) A brief history of the Scade language

09:00 - 10:00: RDP - Session I at Salle 107, Barre 44-54
Chair(s): Victor Vianu

09:00 - 09:15
Talk

Nate Foster, Mooly Sagiv, Victor Vianu

09:15 - 10:00
Talk

Automatic Verification of Database-Centric Workflows

09:00 - 10:00: OBT - Session One at Salle 109, Barre 44-54

09:00 - 10:00
Talk

Keynote talk: Reasoning about Functional Programs: Exploring, Testing and Inductive Proofs.

10:00 - 10:30: Catering - Coffee break at Auditorium Hall

10:00 - 10:30
Coffee break

10:30 - 12:00: Next 40 years of Abstract Interpretation - Industrial Panel 2 & Systems Biology at Amphitheater 44
Chair(s): Jerome Feret

10:30 - 11:00
Talk

Abstract Interpretation in Amazon

11:00 - 11:30
Talk

Abstract Interpretation at Galois

11:30 - 12:00
Talk

Systems biology

10:30 - 12:10: CoqPL 2017 - Morning Session at Auditorium
Chair(s): Alan Schmitt

10:30 - 10:55
Talk

IxFree: Step-Indexed Logical Relations in Coq

10:55 - 11:20
Talk

Logical Relations in Iris

Amin Timany, Robbert Krebbers, Lars Birkedal

11:20 - 11:45
Talk

Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting

Edwin Westbrook, Gregory Malecha

11:45 - 12:10
Talk

ppsimpl: a reflexive Coq tactic for canonising goals

Frédéric Besson

10:30 - 12:05: PiP 2017 - Session 2 at Salle 105, Barre 44-54

10:30 - 10:35
Talk

Peter Sewell (Cambridge) REMS Short Introduction

10:35 - 11:05
Talk

Simon Moore (Cambridge) Experiences of Formal Modelling in the CHERI Computer Architecture Research Project

11:05 - 11:35
Talk

Stephen Kell/Dominic Mulligan (Cambridge) ELF linking: what it means and why it matters

11:35 - 12:05
Talk

Philippa Gardner (Imperial) An Infrastructure for Tractable Verification of JavaScript Programs

10:30 - 12:00: RDP - Session II at Salle 107, Barre 44-54
Chair(s): Mooly Sagiv

10:30 - 11:00
Talk

Verification Challenges in Applications of Blockchain for Business Collaboration

Takaaki Tateishi

11:00 - 11:30
Talk

Fiat: A New Take on Domain-Specific Languages by Programming with Specifications

11:30 - 12:00
Talk

Parallel-Correctness and Transferability for Conjunctive Queries

10:30 - 12:10: OBT - Session Two at Salle 109, Barre 44-54

10:30 - 10:55
Talk

Can we machine-learn programming language semantics?

Dan Ghica, Khulood Alyahya, Victor Patentasu

10:55 - 11:20
Talk

How Far Apart Should Those Programs Be?

11:20 - 11:45
Talk

Programming Quantum Annealers

George Stelle, Scott Pakin

11:45 - 12:10
Talk

Understanding the POSIX Shell as a Programming Language

Michael Greenberg

12:00 - 14:00: Catering - Buffet at Catering area

12:00 - 14:00
Lunch

14:00 - 15:30: CoqPL 2017 - Midday Session at Auditorium
Chair(s): Sandrine Blazy

14:00 - 15:00
Talk

Invited Talk -- Managing Logical and Computational Complexity using Program Transformations

Nicolas Tabareau

15:00 - 15:30
Demonstration

Session with the Coq Development Team

Matthieu Sozeau

14:00 - 15:30: Next 40 years of Abstract Interpretation - Security, Big Code and Synthesis at Amphitheater 44
Chair(s): Xavier Rival

14:00 - 14:30
Talk

14:30 - 15:00
Talk

Bor-Yuh Evan Chang

15:00 - 15:30
Talk

Program synthesis

14:00 - 15:30: PiP 2017 - Session 3 at Salle 105, Barre 44-54

14:00 - 14:30
Talk

John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten years of QuickCheck

14:30 - 15:00
Talk

Byron Cook (Amazon) Automated Reasoning about AWS

15:00 - 15:30
Talk

Steve Zdancewic (U.Penn) Vellvm2: Semantics and Verification for LLVM

14:00 - 15:30: RDP - Session III at Salle 107, Barre 44-54
Chair(s): Nate Foster

14:00 - 14:45
Talk

Synthesizing Data-parallel Programs

Aws Albarghouthi

14:45 - 15:30
Talk

Cosette: A Solver for SQL Equivalences

14:00 - 15:25: OBT - Session Three at Salle 109, Barre 44-54

14:00 - 15:00
Talk

Keynote talk: Varieties of Programming Experience

15:00 - 15:25
Talk

Bootstrapping the next generation of mathematical social machines

Ursula Martin, Alison Pease, Joe Corneli

15:30 - 16:00: Catering - Coffee break at Auditorium Hall

15:30 - 16:00
Coffee break

16:00 - 18:05: CoqPL 2017 - Afternoon Session at Auditorium
Chair(s): Matthieu Sozeau

16:00 - 16:25
Talk

Synthetic topology in HoTT for probabilistic programming

Florian Faissole, Bas Spitters

16:25 - 16:50
Talk

CertiCoq: A verified compiler for Coq

Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, Matthew Weaver

16:50 - 17:15
Talk

CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL

Izumi Asakura, Hidehiko Masuhara, Tomoyuki Aotani

17:15 - 17:40
Talk

Verification of Implementations of Distributed Systems Under Churn

Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, Karl Palmskog

17:40 - 18:05
Talk

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

16:00 - 18:00: PiP 2017 - Session 4 at Salle 105, Barre 44-54

16:00 - 16:30
Talk

Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models

16:30 - 17:30
Talk

Discussion: Methods and Tools for large-scale semantics

16:00 - 18:05: OBT - Session Four at Salle 109, Barre 44-54

16:00 - 16:25
Talk

Designing extensible, domain-specific languages for mathematical diagrams

Katherine Ye, Keenan Crane, Jonathan Aldrich, Joshua Sunshine

16:25 - 16:50
Talk

Laziness Boxes You In

Jose Calderon, Stephen Magill

16:50 - 17:15
Talk

Programming with Epistemic Logic

Markus Eger, Chris Martens

17:15 - 17:40
Talk

Preventing False Discoveries in Adaptive Data Analysis: a Programming Language approach

17:40 - 18:05
Talk

Running Incomplete Programs

Ian Voysey, Cyrus Omar, Matthew Hammer

16:00 - 18:00: RDP - Session IV at Salle 107, Barre 44-54
Chair(s): Victor Vianu

16:00 - 16:30
Talk

Building performance-sensitive systems in high-level languages

Christoph E. Koch

16:30 - 17:00
Talk

Programming Language Ideas Escape the Lab: Declarative Data Description Languages for Managing Ad hoc Data

Kathleen Fisher

17:00 - 17:30
Talk

Computation with Atoms

Szymon Toruńczyk

17:30 - 18:00
Talk

Nate Foster, Victor Vianu, Mooly Sagiv

16:00 - 18:30: Next 40 years of Abstract Interpretation - System Verification and Patrick Cousot's Keynote at Amphitheater 44
Chair(s): Francesco Ranzato

16:00 - 16:30
Talk

System verification

16:30 - 17:45
Talk

Keynote: the Next 40 years of Abstract Interpretation

17:45 - 18:30
Social Event

Concrete Cheese and Wine

19:00 - 21:00: CoqPL 2017 - Social Event at CoqPL-social-event-room

19:00 - 21:00
Social Event

CoqPL Social Event

Sun 15 Jan 2017


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
Amphitheater 44													VMCAI Invited talk 1 09:00 - 10:00																		VMCAI Program Analysis 10:30 - 12:00																																										VMCAI Concurrency 1 14:00 - 15:30																								VMCAI Decision procedures 16:00 - 17:30
Catering area																									Catering Coffee break 10:00 - 10:30																								Catering Buffet 12:00 - 14:00																																										Catering Coffee break 15:30 - 16:00
Salle 105, Barre 44-54											TTT First Morning Session 08:50 - 10:00																				TTT Second Morning Session 10:30 - 12:00																																										TTT First Afternoon Session 14:00 - 15:30																								TTT Second Afternoon Session 16:00 - 18:00
Salle 109, Barre 44-54																SCM Session I 09:15 - 10:00															SCM Session II 10:30 - 12:00																																										SCM Session III 14:00 - 15:30																								SCM Session IV 16:00 - 17:30

Mon 16 Jan 2017


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30						21:00						30						22:00						30
Amphitheater 44													VMCAI Invited talk 2 09:00 - 10:00																		VMCAI Numerical domains 10:30 - 12:00																																										VMCAI Model-checking and bug finding 14:00 - 15:30																								VMCAI Symbolic analysis and invariant synthesis 16:00 - 17:30
Auditorium													CPP Invited Talk 09:00 - 10:00																		CPP Algorithm and library verification 10:30 - 12:00																																										CPP Automated proof and its verification 14:00 - 15:30																								CPP Formalized mathematics with numerical computations 16:00 - 18:00
Auditorium Hall																									Catering Coffee break 10:00 - 10:30																																																																		Catering Coffee break 15:30 - 16:00
Catering area																																																	Catering Buffet 12:00 - 14:00
Procope																																																																	VMCAI Banquet 19:30 - 22:00
Salle 105, Barre 44-54													Tutorials Gradual Typing (AM) 09:00 - 12:00																																																												Tutorials Gradual Typing (PM) 14:00 - 17:00
Salle 107, Barre 44-54													Tutorials Lean (AM) 09:00 - 12:00																																																												Tutorials Lean (PM) 14:00 - 17:00
Salle 109, Barre 44-54													PEPM 2017 Keynote 09:00 - 10:00																		PEPM 2017 Programming languages 10:30 - 12:00																																										PEPM 2017 Tutorial (Idris, Inside-Out) and Poster Session 14:00 - 15:30																								PEPM 2017 Transformation (part I) 16:00 - 17:00
Salle 112, Barre 44-54													Tutorials Flow (AM) 09:00 - 12:00																																																												Tutorials Flow (PM) 14:00 - 17:00
Salle 114, Barre 44-54													Tutorials Frama-C (AM) 09:00 - 12:00																																																												Tutorials Frama-C (PM) 14:00 - 17:00
Salle 116, Barre 44-54											PADL Opening remarks 08:50 - 09:00		PADL Invited Talk 09:00 - 10:00																		PADL Answer Set Programming 10:30 - 12:00																																										PADL Testing and Games 14:00 - 15:30																								PADL Applications I and Inference 16:00 - 17:30

Tue 17 Jan 2017


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30
Amphitheater 44													VMCAI Invited talk 3 09:00 - 10:00																		VMCAI Model Checking and Synthesis 10:30 - 12:00																																										VMCAI Abstract Interpretation 14:00 - 15:30																								VMCAI Concurrency 2 16:00 - 17:30
Auditorium													CPP Invited Talk 09:00 - 10:00																		CPP Verified programming tools 10:30 - 12:00																																										CPP Homotopy type theory 14:00 - 15:30																								CPP Formal verification of programming language foundations 16:00 - 17:30
Auditorium Hall																									Catering Coffee break 10:00 - 10:30																																																																		Catering Coffee break 15:30 - 16:00
Catering area																																																	Catering Buffet 12:00 - 14:00
Salle 105, Barre 44-54													PPS Session 1 09:00 - 10:00																		PPS Session 2 10:30 - 12:00																																										PPS Session 3 14:00 - 15:30																		PPS Poster Session 15:30 - 16:30												PPS Session 5 16:30 - 18:00																					PPS Session 6 18:15 - 19:15
Salle 107, Barre 44-54											PLMW Welcome Session 08:50 - 09:00		PLMW Session I 09:00 - 10:00																		PLMW Session II 10:30 - 12:00																																										PLMW Session III 14:00 - 15:30																								PLMW Session IV 16:00 - 18:00
Salle 109, Barre 44-54													PEPM 2017 Tutorial: reversible computing 09:00 - 10:00																		PEPM 2017 Types 10:30 - 12:00																																										PEPM 2017 Tutorial: Partial Evaluation for Language Implementation 14:00 - 15:30																								PEPM 2017 Transformation (part II) 16:00 - 17:00
Salle 116, Barre 44-54													PADL Applications II 09:00 - 10:00																		PADL Programming Languages 10:30 - 12:00

Wed 18 Jan 2017


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30						21:00						30						22:00						30						23:00						30
Amphitheater 44																			POPL Abstract Interpretation 10:30 - 12:10																																														POPL Probabilistic Programming 14:20 - 16:00																										POPL Logic 16:30 - 17:45
Auditorium	POPL Opening 09:00 - 09:05	POPL Invited speaker 09:05 - 10:00																	POPL Type Systems 1 10:30 - 12:10																																														POPL Concurrency 1 14:20 - 16:00																										POPL Compiler Optimisation 16:30 - 17:45
Auditorium Hall													Catering Coffee break 10:00 - 10:30																																																																								Catering Coffee break 16:00 - 16:30
Catering area																																							Catering Buffet 12:10 - 14:20
Musée des Arts Forains																																																																	Catering Social dinner 19:30 - 23:00

Thu 19 Jan 2017


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30
Amphitheater 44																			POPL Program Analysis 10:30 - 12:10																																														POPL Concurrency 2 14:20 - 16:00																										POPL Semantic Foundations 16:30 - 17:20
Auditorium	POPL ACM and SIGPLAN Awards 09:00 - 09:15			POPL Invited speaker 09:15 - 10:00															POPL Type Systems 2 10:30 - 12:10																																														POPL Functional Programming with Effects 14:20 - 16:00																										POPL Logic and Programming 16:30 - 17:20										POPL Business meeting 17:20 - 18:20
Auditorium Hall													Catering Coffee break 10:00 - 10:30																																																																								Catering Coffee break 16:00 - 16:30																												Student Research Competition Poster Session 18:20 - 20:20
Catering area																																							Catering Buffet 12:10 - 14:20

Fri 20 Jan 2017


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
Amphitheater 44																			POPL Verification and Synthesis 10:30 - 12:10																																														POPL Concurrency 3 14:20 - 16:00																										POPL Quantum 16:30 - 17:45
Auditorium	Student Research Competition Student Competition Award 09:00 - 09:05	POPL Invited speaker 09:05 - 10:00																	POPL Type Systems 3 10:30 - 12:10																																														POPL Gradual Typing and Contracts 14:20 - 16:00																										POPL Security and Privacy 16:30 - 17:45
Auditorium Hall													Catering Coffee break 10:00 - 10:30																																																																								Catering Coffee break 16:00 - 16:30
Catering area																																							Catering Buffet 12:10 - 14:20

Sat 21 Jan 2017


Room	8:00						30						9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30						19:00						30						20:00						30						21:00						30
Amphitheater 44										Next 40 years of Abstract Interpretation Opening 08:45 - 09:00			Next 40 years of Abstract Interpretation Industrial Panel 1 09:00 - 10:00																		Next 40 years of Abstract Interpretation Industrial Panel 2 & Systems Biology 10:30 - 12:00																																										Next 40 years of Abstract Interpretation Security, Big Code and Synthesis 14:00 - 15:30																								Next 40 years of Abstract Interpretation System Verification and Patrick Cousot's Keynote 16:00 - 18:30
Auditorium													CoqPL 2017 Opening Session 09:00 - 10:00																		CoqPL 2017 Morning Session 10:30 - 12:10																																										CoqPL 2017 Midday Session 14:00 - 15:30																								CoqPL 2017 Afternoon Session 16:00 - 18:05
Auditorium Hall																									Catering Coffee break 10:00 - 10:30																																																																		Catering Coffee break 15:30 - 16:00
Catering area																																																	Catering Buffet 12:00 - 14:00
CoqPL-social-event-room																																																																	CoqPL 2017 Social Event 19:00 - 21:00
Salle 105, Barre 44-54												PiP 2017 Welcome 08:55 - 09:00	PiP 2017 Session 1 09:00 - 10:00																		PiP 2017 Session 2 10:30 - 12:05																																										PiP 2017 Session 3 14:00 - 15:30																								PiP 2017 Session 4 16:00 - 18:00
Salle 107, Barre 44-54													RDP Session I 09:00 - 10:00																		RDP Session II 10:30 - 12:00																																										RDP Session III 14:00 - 15:30																								RDP Session IV 16:00 - 18:00
Salle 109, Barre 44-54													OBT Session One 09:00 - 10:00																		OBT Session Two 10:30 - 12:10																																										OBT Session Three 14:00 - 15:25																								OBT Session Four 16:00 - 18:05

Sun 15 Jan 2017


Room	8:00			15			30			45			9:00			15			30			45			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			18:00			15			30			45
Amphitheater 44													VMCAI 2017 Detecting Strict Aliasing Violations in the Wild 09:00 - 10:00																		VMCAI 2017 Partitioned Memory Models for Program Analysis. 10:30 - 11:00						VMCAI 2017 Property Directed Reachability for Proving Absence of Concurrent Modifi ... 11:00 - 11:30						VMCAI 2017 Stabilizing Floating-Point Programs using Provenance Analysis 11:30 - 12:00