POPL 2017 Program

What is Secure Compilation? Part I

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

09:15 - 10:00
Talk

Marco PatrignaniMPI-SWS, Germany

Link to publication

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

10:00 - 10:30
Coffee break

Partitioned Memory Models for Program Analysis.

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

10:30 - 11:00
Talk

Wei WangGoogle, Inc., Clark BarrettStanford University, Thomas WiesNew York University

Property Directed Reachability for Proving Absence of Concurrent Modification Errors

11:00 - 11:30
Talk

Asya FrumkinTel Aviv University, Yotam FeldmanTel Aviv University, Ondřej LhotákUniversity of Waterloo, Canada, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university

Stabilizing Floating-Point Programs using Provenance Analysis

11:30 - 12:00
Talk

Yijia GuNortheastern University, Thomas WahlNortheastern University

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

Aaron TombGalois, Inc.

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 AllaisRadboud University Nijmegen

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ţcuInria Paris

Link to publication

10:40 - 10:50
Talk

Can relational logic facilitate secure compilation? (Short talk)

David NaumannStevens Institute of Technology

Full Abstraction for Language Design (Short talk)

10:50 - 11:00
Talk

Gabriel SchererNortheastern University

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

11:00 - 11:10
Talk

Christine RizkallahUniversity of Pennsylvania, USA

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

11:15 - 12:00
Talk

Lau Skorstengaard

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

12:00 - 14:00
Lunch

Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms

14:00 - 15:30: VMCAI - Concurrency 1 at Amphitheater 44
Chair(s): Camille CotiLIPN, Université Paris 13

14:00 - 14:30
Talk

Igor KonnovTU Wien, Josef WidderTU Wien, Francesco Spegni, Luca Spalazzi

14:30 - 15:00
Talk

Independence Abstractions and Models of Concurrency

Vijay D'SilvaGoogle Inc., Daniel KroeningUniversity of Oxford, Marcelo SousaUniversity of Oxford

15:00 - 15:30
Talk

Static Analysis of Communicating Process using Symbolic Transducers

Vincent BotbolCEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le GallCEA LIST, Emmanuel ChaillouxLIP6 - UPMC

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örtbergInria

14:50 - 15:10
Talk

Equations: a tool for dependent pattern-matching

Cyprien Mangin, Matthieu SozeauInria

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

15:10 - 15:30
Talk

Théo ZimmermannIRIF, Université Paris Diderot, Hugo Herbelin

Linking Types: Secure compilation of multi-language programs

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

14:00 - 14:45
Talk

Daniel PattersonNortheastern University

Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing

14:45 - 15:30
Talk

Dominique DevrieseiMinds - Distrinet, KU Leuven

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

15:30 - 16:00
Coffee break

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

16:00 - 17:30: VMCAI - Decision procedures at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

16:00 - 16:30
Talk

Ernst Moritz HahnState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences

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

16:30 - 17:00
Talk

Andrew ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-Alpes

Matching multiplications in Bit-Vector formulas

17:00 - 17:30
Talk

Supratik ChakrabortyIIT Bombay, Ashutosh Gupta, Rahul JainTata Institute of Fundamental Research

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

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

16:00 - 16:50
Talk

Robbert KrebbersDelft University of Technology, Netherlands

16:50 - 17:10
Talk

Introducing MetaCoq: A Safe Tactic Language for Coq

Beta ZilianiFAMAF, UNC (Argentina) / CONICET (Argentina)

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

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

16:45 - 17:30
Talk

Jonathan ProtzenkoMicrosoft Research

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

Mon 16 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:50 - 09:00: PADL - Opening remarks at Salle 116, Barre 44-54
Chair(s): Yuliya LierlerUniversity of Nebraska, Walid TahaHalmstad University

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

Avik ChaudhuriFacebook

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

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

09:00 - 12:00
Talk

François BobotCEA, Loïc Correnson, Boris YakobowskiCEA - LIST

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

Jeremy G. SiekIndiana University Bloomington

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

09:00 - 10:00
Talk

Proof checking and logic programming

Dale MillerINRIA Saclay and LIX

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

09:00 - 10:00
Talk

Porting the HOL Light Analysis Library: Some Lessons

Lawrence PaulsonUniversity of Cambridge

Verified Concurrent Code: Tricks of the Trade

09:00 - 10:00: VMCAI - Invited talk 2 at Amphitheater 44
Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot

09:00 - 10:00
Talk

Ernie CohenAmazon Web Services

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

09:00 - 10:00
Talk

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

Daniil BerezunJetBrains, Russia, Neil D. JonesUniversity of Copenhagen, Danmark

DOI

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

09:00 - 12:00
Talk

The Lean Theorem Prover

Leonardo De MouraMicrosoft Research, Redmond, Gabriel EbnerVienna University of Technology, Jared RoeschUniversity of Washington, USA, Sebastian UllrichKarlsruhe Institute of Technology

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

10:00 - 10:30
Coffee break

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

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

10:30 - 11:00
Talk

François Pottier

11:00 - 11:30
Talk

A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm

Jose Divasón, Sebastiaan Joosten, René ThiemannUniversity of Innsbruck, Akihisa Yamada

11:30 - 12:00
Talk

Formal foundations of 3D geometry for modeling robot manipulators

Reynald AffeldtAIST, Japan, 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 VennekensKU Leuven

11:00 - 11:30
Talk

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

Christoph RedlVienna University of Technology

11:30 - 12:00
Talk

Integrating Answer Set Programming with Object-oriented Languages

Jakob RathVienna University of Technology, Christoph RedlVienna University of Technology

10:30 - 12:00: VMCAI - Numerical domains at Amphitheater 44
Chair(s): Laure GonnordUniversity of Lyon & LIP, France

10:30 - 11:00
Talk

Sound Bit-Precise Numerical Domains

Tushar SharmaUniversity of Wisconsin - Madison, USA, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.

Efficient Elimination of Redundancies in Polyhedra using Raytracing

11:00 - 11:30
Talk

Alexandre Maréchal, Michael Perin

Media Attached File Attached

11:30 - 12:00
Talk

Finding Relevant Templates via the Principal Component Analysis

Yassamine SeladjiUniversity of Tlemcen

Lightweight Soundness for Towers of Language Extensions

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

10:30 - 11:00
Talk

Alejandro SerranoUtrecht University, Jurriaan HageUtrecht University

11:00 - 11:30
Talk

Detecting code clones with gaps by function applications

Tsubasa MatsushitaShibaura Institute of Technology, Isao SasanoShibaura Institute of Technology

11:30 - 12:00
Talk

PEG Parsing in Less Space Using Progressive Tabling and Dynamic AnalysisBest Paper

Fritz HengleinDIKU, Denmark, Ulrik Terp RasmussenDIKU, University of Copenhagen

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

12:00 - 14:00
Lunch

BliStrTune: Hierarchical Invention of Theorem Proving Strategies

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

14:00 - 14:30
Talk

Jan Jakubuv, Josef Urban

14:30 - 15:00
Talk

Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic

Reuben RoweUniversity College London, 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?

Avik ChaudhuriFacebook

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

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

14:00 - 17:00
Talk

François BobotCEA, Loïc Correnson, Boris YakobowskiCEA - LIST

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

Jeremy G. SiekIndiana University Bloomington

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

14:00 - 17:00
Talk

The Lean Theorem Prover

Leonardo De MouraMicrosoft Research, Redmond, Gabriel EbnerVienna University of Technology, Jared RoeschUniversity of Washington, USA, Sebastian UllrichKarlsruhe Institute of Technology

14:00 - 15:30: VMCAI - Model-checking and bug finding at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

14:00 - 14:30
Talk

Effective Bug Finding in C Programs with Shape and Effect Abstraction

Iago AbalIT University of Copenhagen, Claus BrabrandIT University of Copenhagen, Denmark, Andrzej WąsowskiIT University of Copenhagen, Denmark

14:30 - 15:00
Talk

Reduction of Workflow Nets for Generalised Soundness Verification

Hadrien BrideFemto-ST / Université de Franche-Comté, Olga KouchnarenkoFemto-ST / Université de Franche-Comté, Fabien PeureuxFemto-ST / Université de Franche-Comté + Smartesting S&S

Dynamic Reductions for Model Checking Concurrent Software.

15:00 - 15:30
Talk

Henning GüntherTechnische Universität Wien, Alfons LaarmanVienna University of Technology, Ana SokolovaUniversity of Salzburg, Georg WeissenbacherTechnische Universität Wien

Failing Faster: Overlapping Patterns for Property-Based Testing

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

14:00 - 14:30
Talk

Jonathan FowlerUniversity of Nottingham, Graham HuttonUniversity of Nottingham

14:30 - 15:00
Talk

Boltzmann Samplers for Closed Simply-Typed Lambda Terms

Maciej BendkowskiJagiellonian University, Katarzyna GrygielJagiellonian University, Paul TarauUniversity of North Texas

15:00 - 15:30
Talk

Selection Equilibria of Higher-Order Games

Paulo OlivaQueen Mary University of London, Jules HedgesUniversity of Oxford, Viktor WinschelETH Zürich, Philipp ZahnUniversity of St. Gallen, Evguenia ShpritsUniversity of Mannheim

14:00 - 15:30: PEPM 2017 - Tutorial (Idris, Inside-Out) and Poster Session at Salle 109, Barre 44-54
Chair(s): Ulrik SchultzUniversity of Southern Denmark, Jeremy YallopUniversity of Cambridge, UK

14:00 - 15:00
Talk

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

David Thrane ChristiansenIndiana University

15:00 - 15:30
Talk

Invited posters

Nada AminEPFL, Tiark RompfPurdue University, Oleg Kiselyov, Aggelos BiboudisUniversity of Athens, Nick PalladinosNessos Information Technologies, SA, Yannis SmaragdakisUniversity of Athens

15:00 - 15:30
Talk

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

Tatsuya KatsushimaTohoku University, Japan, Oleg Kiselyov

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

15:30 - 16:00
Coffee break

A Domain-Specific Language for Software-Defined Radio

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

16:00 - 16:30
Talk

Geoffrey MainlandDrexel University

16:30 - 17:00
Talk

A Declarative DSL for Customized Rendering of Text-Based Art

Felix Klock

17:00 - 17:30
Talk

Using Iterative Deepening for Probabilistic Logic Inference

Theofrastos MantadelisUniversidade do Porto, 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-DorelIRIT, Université Paul Sabatier, Pierre Roux

17:00 - 17:30
Talk

Markov Processes in Isabelle/HOL

Johannes HölzlTechnische Universität München

DOI Pre-print File Attached

17:30 - 18:00
Talk

Formalising Real Numbers in Homotopy Type Theory

Gaetan Gilbert

16:00 - 17:30: VMCAI - Symbolic analysis and invariant synthesis at Amphitheater 44
Chair(s): Constantin EneaLIAFA, Université Paris Diderot

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 GurfinkelUniversity of Waterloo, Sharon ShohamTel Aviv university, Sharad MalikPrinceton University

17:00 - 17:30
Talk

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

Lukáš Holík, Martin HruskaBrno University of Technology , Ondrej LengalBrno University of Technology , Adam RogalewiczBrno University of Technology , Tomas VojnarBrno University of Technology

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

16:00 - 16:30
Talk

Verification of Code Generators via Higher-Order Model Checking

Takashi SuwaUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Atsushi IgarashiKyoto University

16:30 - 17:00
Talk

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

Krishna NarasimhanGoethe University, Julia LawallInria/LIP6, Christoph ReichenbachGoethe University

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

Tue 17 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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 ChupinENSTA ParisTech

09:30 - 10:00
Talk

DALI for Cognitive Robotics: Principles and Prototype Implementation

Stefania CostantiniDipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila, Giovanni De GasperisDipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Giulio NazziconeDipartimento di Ingegneria e Scienze dell'Informazione eMatematica

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

09:00 - 10:00
Talk

Mechanized verification of preemptive OS kernels

Xinyu FengUniversity of Science and Technology of China

Verification of Cancer Programs

09:00 - 10:00: VMCAI - Invited talk 3 at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

09:00 - 10:00
Talk

Jasmin FisherMicrosoft Research

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

09:00 - 10:00
Talk

Towards a metric semantics for probabilistic programming (invited talk)

Gordon Plotkin

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 FisherTufts University

Abductive Reasoning in Deductive Verification

09:30 - 10:00
Talk

Isil DilligUT Austin

Reversible computing from a programming language perspective

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

09:00 - 10:00
Talk

Robert Glück

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

10:00 - 10:30
Coffee break

Reachability for dynamic parametric processes

10:30 - 12:00: VMCAI - Model Checking and Synthesis at Amphitheater 44
Chair(s): Ahmed BouajjaniIRIF, Université Paris Diderot

10:30 - 11:00
Talk

Anca MuschollUniversité de Bordeaux / LaBRI, Helmut SeidlTechnische Universität München, Igor WalukiewiczCNRS, LaBRI

11:00 - 11:30
Talk

Synthesizing Non-Vacuous Systems

Roderick BloemInstitute of Software Technology, Graz University of Technology , Hana Chockler, Masoud EbrahimiInstitute of Applied Information Processing and Communications, Graz University of Technology, Ofer StrichmanTechnion

Solving Nonlinear Integer Arithmetic with MCSat

11:30 - 12:00
Talk

Dejan JovanovićSRI International

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 AntoyKiel University, Michael HanusKiel University

11:00 - 11:30
Talk

Canonicalizing High-Level Constructs in Picat

Neng-Fa ZhouCUNY Brooklyn College and Graduate Center, Jonathan FruhmanCUNY Brooklyn College

11:30 - 12:00
Talk

An Overview of PRhoLog

Besik DunduaInstitute of Applied Mathematics, Tbilisi State University, Temur Kutsia, Klaus Reisenberger-HagmayerJohannes Kepler University Linz

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

10:30 - 10:50
Talk

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

Daniel HuangHarvard University, Greg MorrisettCornell University

10:50 - 11:00
Meeting

Discussion 1

11:00 - 11:20
Talk

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

Michael MisloveTulane

11:20 - 11:30
Meeting

Discussion 2

11:30 - 11:50
Talk

Building inference algorithms from monad transformers

Adam ŚcibiorUniversity of Cambridge, Yufei CaiUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany, Zoubin GhahramaniUniversity of Cambridge

11:50 - 12:00
Meeting

Discussion 3

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.

Michael HicksUniversity of Maryland at College Park, USA

Mechanizing Meta-Theory in Beluga

11:00 - 11:30
Talk

Brigitte PientkaMcGill University

Research: The Industrial Culture

11:30 - 12:00
Talk

Nikhil SwamyMicrosoft Research

Cost versus Precision for Approximate Typing for Python

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

10:30 - 11:00
Talk

Levin FritzUtrecht University, Jurriaan HageUtrecht University

11:00 - 11:30
Talk

Refining types using type guards in TypeScript

Ivo Gabe de WolffUtrecht University, Jurriaan HageUtrecht University

11:30 - 12:00
Talk

Predicting Resource Consumption of Higher-Order Workflows

Markus KlinikRadboud University Nijmegen, Jurriaan HageUtrecht University, Jan Martin JansenNetherlands Defence Academy, Rinus PlasmeijerRadboud University Nijmegen

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 FoxUniversity of Cambridge, UK, Magnus O. MyreenChalmers University of Technology, Sweden, Yong Kiam TanIHPC at A*STAR, Singapore, Ramana Kumar

11:00 - 11:30
Talk

COMPLX: a verification framework for concurrent imperative programs

Sidney AmaniUNSW, Australia, June AndronickData61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin, Corey Lewis, Christine RizkallahUniversity of Pennsylvania, USA, Joseph Tuong

11:30 - 12:00
Talk

Verifying dynamic race detection

William ManskyUniversity of Pennsylvania, Yuanfeng PengUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania, Joseph DeviettiUniversity of Pennsylvania

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

12:00 - 14:00
Lunch

Complete Abstractions and Subclassical Modal Logics

14:00 - 15:30: VMCAI - Abstract Interpretation at Amphitheater 44
Chair(s): Roberto GiacobazziUniversity of Verona, Italy

14:00 - 14:30
Talk

Vijay D'SilvaGoogle, Marcelo SousaUniversity of Oxford

14:30 - 15:00
Talk

Structuring Abstract Interpreters through State and Value Abstractions

David BühlerCEA LIST, Boris YakobowskiCEA - LIST, Sandrine BlazyUniversity of Rennes 1, France

Conjunctive Abstract Interpretation using Paramodulation

15:00 - 15:30
Talk

Mooly SagivTel Aviv University, Or OzeriTel Aviv university, Oded PadonTel Aviv University, Noam RinetzkyTel Aviv University

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

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

14:00 - 14:30
Talk

Andrej BauerUniversity of Ljubljana, Jason GrossMIT CSAIL, Peter Lefanu Lumsdaine, Michael Shulman, Matthieu SozeauInria, Bas Spitters

Lifting proof-relevant unification to higher dimensions

14:30 - 15:00
Talk

Jesper CockxiMinds, Belgium, Dominique DevrieseiMinds - Distrinet, KU Leuven

15:00 - 15:30
Talk

The Next 700 Syntactical models of type theory

Simon Boulier, Pierre-Marie Pédrot, Nicolas TabareauInria, France

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

14:00 - 14:20
Talk

Commutativity logic for probabilistic trace equivalence: complete or not?

Paul Blain Levy, Nathan BowlerUniversität Hamburg

14:20 - 14:30
Meeting

Discussion 4

14:30 - 14:50
Talk

Mathematical structures of probabilistic programming

Ilias GarnierUniversity of Edinburgh, Fredrik DahlqvistUniversity College London, Florence ClercMcGill University, Vincent DanosENS Paris/CNRS

14:50 - 15:00
Meeting

Discussion 5

15:00 - 15:20
Talk

A weakest pre-expectation semantics for mixed-sign expectations

Benjamin Lucien KaminskiRWTH Aachen University, Joost-Pieter KatoenRWTH Aachen University

15:20 - 15:30
Meeting

Discussion 6

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

14:00 - 15:00
Talk

Student Interaction Activity

Eva DarulovaMPI-SWS, Loris D'AntoniUniversity of Wisconsin–Madison, Alexandra SilvaUniversity College London, Dimitrios VytiniotisMicrosoft Research, Cambridge

15:00 - 15:30
Talk

How to Give Talks That People Can Follow

Derek DreyerMPI-SWS

Practical Partial Evaluation for Language Implementation with Graal & Truffle

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

14:00 - 15:30
Talk

Gilles Duboscq

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

15:30 - 16:00
Coffee break

ProbLog and applicative probabilistic programming

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

15:30 - 16:30
Meeting

Alexander VandenbrouckeKU Leuven, Belgium, Tom SchrijversKU Leuven

15:30 - 16:30
Meeting

Encapsulating models and approximate inference programs in probabilistic modules

Marco Cusumano-TownerMIT-CSAIL, Vikash MansinghkaMassachusetts Institute of Technology

15:30 - 16:30
Meeting

The extended semantics for probabilistic programming languages

Siddharth SrivastavaUTRC Berkeley, Nicholas HayVicarious, Yi WUUC Berkeley, Stuart RussellUniversity of California, Berkeley

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 NandiUniversity of Washington, USA, Adrian SampsonCornell University, Dan GrossmanUniversity of Washington, Todd Mytkowicz, Kathryn S McKinleyMicrosoft Research

15:30 - 16:30
Meeting

On computable representations of exchangeable data

Nathanael L. AckermanHarvard University, Jeremy AvigadCarnegie Mellon University, Cameron FreerGamalon and Borelian, Daniel Roy, Jason M. RutePennsylvania State University

15:30 - 16:30
Meeting

Probabilistic logic programs: unifying program trace and possible world semantics

Angelika KimmigKU Leuven, Luc De RaedtKU Leuven

15:30 - 16:30
Meeting

Metropolis-Hastings for mixtures of conditional distributions

Oleg Kiselyov

15:30 - 16:30
Meeting

Support and influence analysis for visualizing posteriors of probabilistic programs

Long OuyangStanford University

15:30 - 16:30
Meeting

Efficient exact inference in discrete Anglican programs

Robert CornishUniversity of Oxford, Frank WoodUniversity of Oxford, Hongseok YangUniversity of Oxford

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

16:00 - 16:30
Talk

Using Abstract Interpretation to Correct Synchronization Faults

Pietro FerraraIBM Research, Omer TrippIBM Thomas J. Watson Research Center, Peng LiuPurdue University, Eric KoskinenYale University

16:30 - 17:00
Talk

Detecting All High-Level Dataraces in an RTOS Kernel.

Suvam MukherjeeIndian Institute of Science, Arunkumar SIndian Institute of Science, Deepak D'Souza

17:00 - 17:30
Talk

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

Raphaël MonatEcole Normale Supérieure de Lyon, Antoine MinéUPMC, France

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 AllaisRadboud University Nijmegen, James Chapman, Conor McBride, James McKinnaUniversity of Edinburgh

16:30 - 17:00
Talk

Formally verified differential dynamic logic

Brandon Bohrer, Vincent RahliSnT, 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 SmolkaSaarland University

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

Martin VechevETH Zurich

16:30 - 17:00
Talk

The Curse of Knowledge

Benjamin C. PierceUniversity of Pennsylvania

Young Researcher Panel Session

17:00 - 18:00
Talk

Roopsha SamantaPurdue University, Nada AminEPFL, Jonathan ProtzenkoMicrosoft Research, Zachary KincaidPrinceton University

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

16:00 - 16:30
Talk

Functional Parallels of Sequential Imperatives

Tiark RompfPurdue University, Kevin J. BrownStanford University

16:30 - 17:00
Talk

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

Kazutaka Matsuda, Kazuyuki AsadaUniversity of Tokyo

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

16:30 - 16:50
Talk

An exponential family basis for probabilistic programming

Chad ScherrerGalois, Inc.

16:50 - 17:00
Meeting

Discussion 7

17:00 - 17:20
Talk

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

Raphaël LaurentProbaYes, Kamel MekhnachaProbaYes, Emmanuel MazerCNRS/LIG, Pierre BessièreCNRS/ISIR

17:20 - 17:30
Meeting

Discussion 8

17:30 - 17:50
Talk

Exchangeable random process and data abstraction

Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, Nathanael L. AckermanHarvard University, Cameron FreerGamalon and Borelian, Daniel Roy

17:50 - 18:00
Meeting

Discussion 9

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

18:15 - 18:35
Talk

Reducing probabilistic choice to nondeterministic choice

Ernie CohenAmazon Web Services

18:35 - 18:45
Meeting

Discussion 10

18:45 - 19:05
Talk

GraPPa: spanning the expressivity vs. efficiency continuum

Edwin WestbrookGalois, Inc., Chad ScherrerGalois, Inc., Nathan CollinsGalois, Inc., Eric MertensGalois, Inc.

19:05 - 19:15
Meeting

Discussion 11

Wed 18 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05: POPL - Opening at Auditorium
Chair(s): Giuseppe CastagnaParis Diderot University & CNRS, Andrew D. GordonMicrosoft Research and University of Edinburgh

09:00 - 09:05
Day opening

Opening

09:05 - 10:00: POPL - Invited speaker at Auditorium
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh

09:05 - 10:00
Talk

The Influence of Dependent Types

Stephanie WeirichUniversity of Pennsylvania

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

10:00 - 10:30
Coffee break

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

10:30 - 12:10: POPL - Abstract Interpretation at Amphitheater 44
Chair(s): Isabella MastroeniUniversity of Verona, Italy

10:30 - 10:55
Talk

Jade AlglaveUniversity College London, Patrick CousotNew York University

10:55 - 11:20
Talk

A Posteriori Environment Analysis with Pushdown Delta CFA

Kimball GermaneUniversity of Utah, Matthew MightUniversity of Utah; Harvard Medical School; The White House

11:20 - 11:45
Talk

Semantic-Directed Clumping of Disjunctive Abstract States

Huisong LiINRIA/CNRS/ENS/PSL*, François BérengerINRIA/CNRS/ENS/PSL*, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Xavier RivalINRIA/CNRS/ENS Paris

11:45 - 12:10
Talk

Fast Polyhedra Abstract Domain

Gagandeep SinghETH Zurich, Switzerland, Markus PüschelETH Zurich, Martin VechevETH Zurich

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

10:30 - 10:55
Talk

Polymorphism, subtyping and type inference in MLsub

Stephen Dolan, Alan MycroftUniversity of Cambridge

10:55 - 11:20
Talk

Java generics are Turing complete

Radu GrigoreUniversity of Kent

11:20 - 11:45
Talk

Hazelnut: A Bidirectionally Typed Structure Editor Calculus

Cyrus OmarCarnegie Mellon University, Ian VoyseyCarnegie Mellon University, Michael HiltonOregon State University, USA, Jonathan AldrichCarnegie Mellon University, Matthew HammerUniversity of Colorado, Boulder

11:45 - 12:10
Talk

Modules, Abstraction, and Parametric Polymorphism

Karl CraryCarnegie Mellon University

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

12:10 - 14:20
Lunch

A Promising Semantics for Relaxed-Memory Concurrency

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

14:20 - 14:45
Talk

Jeehoon KangSeoul National University, Chung-Kil HurSeoul National University, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Derek DreyerMPI-SWS

Link to publication Pre-print Media Attached

14:45 - 15:10
Talk

Automatically Comparing Memory Consistency Models

John WickersonImperial College London, Mark BattyUniversity of Kent, Tyler SorensenImperial College London, George A. ConstantinidesImperial College London, UK

Pre-print Media Attached File Attached

15:10 - 15:35
Talk

Interactive Proofs in Higher-Order Concurrent Separation Logic

Robbert KrebbersDelft University of Technology, Netherlands, Amin Timanyimec - Distrinet, KU Leuven, Lars BirkedalAarhus University

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-JespersenAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University

14:20 - 16:00: POPL - Probabilistic Programming at Amphitheater 44
Chair(s): Marco GaboardiSUNY Buffalo, USA

14:20 - 14:45
Talk

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

Leonidas LampropoulosUniversity of Pennsylvania, Diane Gallois-WongInria Paris, ENS Paris, Cătălin HriţcuInria Paris, John HughesChalmers University of Technology, Benjamin C. PierceUniversity of Pennsylvania, Li-yao XiaENS Paris

Exact Bayesian Inference by Symbolic Disintegration

14:45 - 15:10
Talk

Chung-chieh ShanIndiana University, USA, Norman Ramsey

Stochastic Invariants for Probabilistic Termination

15:10 - 15:35
Talk

Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria, Djordje ZikelicUniversity of Cambridge

15:35 - 16:00
Talk

Coupling proofs are probabilistic product programs

Gilles BartheIMDEA, Benjamin GregoireINRIA, Justin Hsu, Pierre-Yves StrubÉcole Polytechnique

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

16:00 - 16:30
Coffee break

A Program Optimization for Automatic Database Result Caching

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

16:30 - 16:55
Talk

Ziv ScullyCarnegie Mellon University, Adam ChlipalaMIT

16:55 - 17:20
Talk

Stream Fusion, to Completeness

Oleg Kiselyov, Aggelos BiboudisUniversity of Athens, Nick PalladinosNessos Information Technologies, SA, Yannis SmaragdakisUniversity of Athens

Pre-print Media Attached

17:20 - 17:45
Talk

Rigorous Floating-point Mixed Precision Tuning

Wei-Fan ChiangSchool of Computing, University of Utah, Ganesh GopalakrishnanUniversity of Utah, Zvonimir RakamaricUniversity of Utah, Ian BriggsSchool of Computing, University of Utah, Marek S. BaranowskiUniversity of Utah, Alexey SolovyevSchool of Computing, University of Utah

Monadic second-order logic on finite sequences

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

16:30 - 16:55
Talk

Loris D'AntoniUniversity of Wisconsin–Madison, Margus VeanesMicrosoft Research

16:55 - 17:20
Talk

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

Naoki KobayashiUniversity of Tokyo, Japan, Etienne LozesENS Cachan, Florian BruseUniversity of Kassel

17:20 - 17:45
Talk

Coming to Terms with Quantified Reasoning

Simon RobillardChalmers University of Technology, Andrei VoronkovUniversity of Manchester, Laura KovacsChalmers University of Technology

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

19:30 - 23:00
Dinner

Social dinner

Thu 19 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

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 GiacobazziUniversity of Verona, Italy

09:15 - 10:00
Talk

40 Years of Abstract Interpretation — An Interview with Patrick Cousot

Patrick CousotNew York University, Roberto GiacobazziUniversity of Verona, Italy

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

10:00 - 10:30
Coffee break

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

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

10:30 - 10:55
Talk

Relational Cost Analysis

Ezgi ÇiçekMPI-SWS, Germany, Gilles BartheIMDEA, Marco GaboardiSUNY Buffalo, USA, Deepak GargMPI-SWS, Germany, Jan HoffmannCarnegie Mellon University

10:55 - 11:20
Talk

Ravichandhran MadhavanEPFL, Sumith KulalIIT Bombay, Viktor KunčakEPFL, Switzerland

11:20 - 11:45
Talk

Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability

Qirun ZhangUniversity of California, Davis, Zhendong SuUniversity of California, Davis

11:45 - 12:10
Talk

Towards Automatic Resource Bound Analysis for OCaml

Jan HoffmannCarnegie Mellon University, Ankush DasCarnegie Mellon University, Shu-chun WengYale University

10:30 - 12:10: POPL - Type Systems 2 at Auditorium
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh

10:30 - 10:55
Talk

Deciding equivalence with sums and the empty type

Gabriel SchererNortheastern University

10:55 - 11:20
Talk

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

Danko IlikTrusted Labs

11:20 - 11:45
Talk

Contextual isomorphisms

Paul Blain Levy

11:45 - 12:10
Talk

Typed Self-Evaluation via Intensional Type Functions

Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles

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

12:10 - 14:20
Lunch

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

14:20 - 16:00: POPL - Concurrency 2 at Amphitheater 44
Chair(s): Nobuko YoshidaImperial College London, UK

14:20 - 14:45
Talk

Shaked FlurUniversity of Cambridge, Susmit SarkarUniversity of St. Andrews, UK, Christopher PulteUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Luc MarangetINRIA Rocquencourt, Kathryn E. GrayUniversity of Cambridge, Ali SezginUniversity of Cambridge, Mark BattyUniversity of Kent, Peter SewellUniversity of Cambridge

14:45 - 15:10
Talk

Dynamic Race Detection For C++11

Christopher LidburyImperial College London, Alastair DonaldsonImperial College London

15:10 - 15:35
Talk

Serializability for Eventual Consistency: Criterion, Analysis and Applications

Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zurich

Thread Modularity at Many Levels: a Pearl in Compositional Verification

15:35 - 16:00
Talk

Jochen HoenickeUniversität Freiburg, Rupak MajumdarMPI-SWS, Andreas PodelskiUniversity of Freiburg, Germany

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

14:20 - 14:45
Talk

Type Directed Compilation of Row-Typed Algebraic Effects

Daan LeijenMicrosoft Research

14:45 - 15:10
Talk

Do be do be do

Sam LindleyUniversity of Edinburgh, Conor McBride, Craig McLaughlinThe University of Edinburgh

15:10 - 15:35
Talk

Dijkstra Monads for Free

Danel AhmanUniversity of Edinburgh, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris, ENS Paris, and Microsoft Research, Guido MartínezInria Paris, UNR Argentina, Gordon Plotkin, Jonathan ProtzenkoMicrosoft Research, Aseem RastogiMicrosoft Research India, Nikhil SwamyMicrosoft Research

Stateful Manifest Contracts

15:35 - 16:00
Talk

Taro Sekiyama, Atsushi IgarashiKyoto University

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

16:00 - 16:30
Coffee break

Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks

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

16:30 - 16:55
Talk

Kausik SubramanianUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison, Aditya AkellaUniversity of Wisconsin-Madison

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 BirkedalAarhus University

16:30 - 16:55
Talk

A Semantic Account of Metric Preservation

Arthur Azevedo de AmorimUniversity of Pennsylvania, USA, Ikram CheriguiENS Paris, Marco GaboardiSUNY Buffalo, USA, Justin Hsu, Shin-ya KatsumataKyoto University

16:55 - 17:20
Talk

Cantor Meets Scott: Semantic Foundations for Probabilistic Networks

Steffen SmolkaCornell University, Praveen KumarCornell University, Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London

DOI File Attached

17:20 - 18:20: POPL - Business meeting at Auditorium
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh

17:20 - 17:40
Talk

PC Chair report

Andrew D. GordonMicrosoft Research and University of Edinburgh

17:40 - 17:50
Talk

POPL 2018 presentation

Andrew MyersCornell University, Ranjit JhalaUniversity of California, San Diego

17:50 - 18:20
Meeting

SIGPLAN business meeting

Andrew D. GordonMicrosoft Research and University of Edinburgh

18:20 - 20:20: Student Research Competition - Poster Session at Auditorium Hall
Chair(s): Qirun ZhangUniversity of California, Davis, Matteo CiminiIndiana University, USA, Julien SignolesCEA LIST, Kim NguyễnLRI, Université Paris-Sud

18:20 - 18:30
Demonstration

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

Nicholas RiouxNortheastern University

18:30 - 18:40
Demonstration

Gradual Type Precision as Retraction

Max NewNortheastern University

18:40 - 18:50
Demonstration

Linking Types: Specifying Safe Interoperability and Equivalences

Daniel PattersonNortheastern University

18:50 - 19:00
Demonstration

A Monadic Framework for Bidirectional Programming

Li-yao XiaENS Paris

19:00 - 19:10
Demonstration

Gradual Set-Theoretic Types

Victor LanvinENS Paris-Saclay

19:10 - 19:20
Demonstration

Abstract Interpretation of High-Level Transformations

Ahmad Salim Al-SibahiIT University of Copenhagen, Denmark

19:20 - 19:30
Demonstration

FairSquare: A Static Analysis Tool for Algorithmic Fairness

Samuel DrewsUniversity of Wisconsin-Madison

19:30 - 19:40
Demonstration

Toward Type-Preserving Compilation of Coq

William J. BowmanNortheastern University

19:40 - 19:50
Demonstration

A Symbolic Execution Framework for Haskell

Anton XueYale University

19:50 - 20:00
Demonstration

Synthesizing Imperative Programs from Examples for Introductory Programming Assignments

Sunbeom SoKorea University

20:00 - 20:10
Demonstration

Provenance for Configuration Language Security

Weili FuUniversity of Edinburgh

20:10 - 20:20
Demonstration

A gradually typed polymorphic lambda calculus

Yuu IgarashiKyoto University

Fri 20 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05: Student Research Competition - Student Competition Award at Auditorium
Chair(s): Kim NguyễnLRI, Université Paris-Sud

09:00 - 09:05
Awards

Student Competition Award

09:05 - 10:00: POPL - Invited speaker at Auditorium
Chair(s): Giuseppe CastagnaParis Diderot University & CNRS

09:05 - 10:00
Talk

Rust: from POPL to practice

Aaron TuronMPI-SWS

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

10:00 - 10:30
Coffee break

Intersection Type Calculi of Bounded Dimension

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

10:30 - 10:55
Talk

Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund

10:55 - 11:20
Talk

Type Soundness Proofs with Definitional Interpreters

Nada AminEPFL, Tiark RompfPurdue University

11:20 - 11:45
Talk

Computational Higher-Dimensional Type Theory

Carlo AngiuliCarnegie Mellon University, Robert Harper, Todd WilsonCalifornia State University Fresno

11:45 - 12:10
Talk

Type Systems as Macros

Stephen ChangNortheastern University, Alex KnauthNortheastern University, Ben GreenmanNortheastern University

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

10:30 - 10:55
Talk

Component-Based Synthesis for Complex APIs

Yu FengUniversity of Texas at Austin, USA, Ruben Martins, Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.

10:55 - 11:20
Talk

Learning nominal automata

Joshua MoermanRadboud University, Matteo SammartinoUniversity College London, Alexandra SilvaUniversity College London, Bartek KlinUniversity of Warsaw, Michał SzynwelskiUniversity of Warsaw

11:20 - 11:45
Talk

On Verifying Causal Consistency

Ahmed BouajjaniIRIF, Université Paris Diderot, Constantin EneaLIAFA, Université Paris Diderot, Rachid Guerraoui, Jad HamzaLIAFA, Université Paris Diderot

11:45 - 12:10
Talk

Complexity Verification Using Guided Theorem Enumeration

Akhilesh SrikanthGeorgia Institute of Technology, Burak SahinGeorgia Institute of Technology, William Harris

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

12:10 - 14:20
Lunch

Parallel Functional Arrays

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

14:20 - 14:45
Talk

Ananya Kumar, Guy E. BlellochCarnegie Mellon University, Robert Harper

14:45 - 15:10
Talk

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

Igor KonnovTU Wien, Marijana LazićTU Wien, Helmut VeithTU Wien, Josef WidderTU Wien

DOI Pre-print

15:10 - 15:35
Talk

Analyzing divergence in bisimulation semantics

Xinxin LiuInstitute of software, Chinese academy of sciences, Tingting Yu, Wenhui ZhangInstitute of software, Chinese academy of sciences

15:35 - 16:00
Talk

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

Julien LangeImperial College London, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London, UK

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

14:20 - 16:00: POPL - Gradual Typing and Contracts at Auditorium
Chair(s): Ronald GarciaUniversity of British Columbia

14:20 - 14:45
Talk

Michael Vitousek, Cameron SwordsIndiana University, Jeremy G. SiekIndiana University Bloomington

14:45 - 15:10
Talk

Gradual Refinement Types

Nicolás Lehmann, Éric TanterUniversity of Chile, Chile

Link to publication DOI Pre-print

15:10 - 15:35
Talk

Automatically Generating the Dynamic Semantics of Gradually Typed Languages

Matteo CiminiIndiana University, USA, Jeremy G. SiekIndiana University Bloomington

15:35 - 16:00
Talk

Sums of Uncertainty: Refinements go gradual

Khurram A. JaferyUniversity of British Columbia, Joshua DunfieldUniversity of British Columbia

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

16:00 - 16:30
Coffee break

Invariants of Quantum Programs: Characterisations and Generation

16:30 - 17:45: POPL - Quantum at Amphitheater 44
Chair(s): Michele PaganiIRIF, Université Paris Diderot

16:30 - 16:55
Talk

Mingsheng YingUniversity of Technology Sydney, Australia, Shenggang YingUniversity of Technology Sydney, Australia, Xiaodi WuUniversity of Oregon, USA

16:55 - 17:20
Talk

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

Ugo Dal LagoUniversity of Bologna, France, Claudia Faggian, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay, Akira YoshimizuUniv.Tokyo

17:20 - 17:45
Talk

QWIRE: A Core Language for Quantum Circuits

Jennifer Paykin, Robert RandUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania

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

16:30 - 16:55
Talk

LMS-Verify: Abstraction Without Regret for Verified Systems Programming

Nada AminEPFL, Tiark RompfPurdue University

16:55 - 17:20
Talk

Hypercollecting Semantics and its Application to Static Analysis of Information Flow

Mounir AssafStevens Institute of Technology, David NaumannStevens Institute of Technology, Julien SignolesCEA LIST, Éric TotelCentraleSupélec, Frédéric TronelCentraleSupélec

17:20 - 17:45
Talk

LightDP: Towards Automating Differential Privacy Proofs

Danfeng ZhangPennsylvania State University, Daniel KiferDept. of Computer Science and Engineering, Penn State University

Sat 21 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

08:45 - 09:00
Day opening

Opening

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

08:55 - 09:00
Talk

Welcome

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

09:00 - 09:30
Talk

Abstract Interpretation in Absint

Christian FerdinandAbsInt

09:30 - 10:00
Talk

Abstract Interpretation in Facebook

Francesco LogozzoFacebook

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

09:00 - 10:00
Talk

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

Robbert KrebbersDelft University of Technology, Netherlands

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 VianuUC San Diego

09:00 - 09:15
Talk

Welcome

Nate FosterCornell University, Mooly SagivTel Aviv University, Victor VianuUC San Diego

09:15 - 10:00
Talk

Automatic Verification of Database-Centric Workflows

Alin Deutsch

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.

Moa JohanssonChalmers University of Technology

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

10:00 - 10:30
Coffee break

Abstract Interpretation in Amazon

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

10:30 - 11:00
Talk

Byron CookAmazon

11:00 - 11:30
Talk

Abstract Interpretation at Galois

Aaron TombGalois, Inc.

11:30 - 12:00
Talk

Systems biology

Vincent DanosENS Paris/CNRS

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

10:30 - 10:55
Talk

IxFree: Step-Indexed Logical Relations in Coq

Piotr Polesiuk

Logical Relations in Iris

10:55 - 11:20
Talk

Amin Timanyimec - Distrinet, KU Leuven, Robbert KrebbersDelft University of Technology, Netherlands, Lars BirkedalAarhus University

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

11:20 - 11:45
Talk

Edwin WestbrookGalois, Inc., Gregory MalechaUCSD

ppsimpl: a reflexive Coq tactic for canonising goals

11:45 - 12:10
Talk

Frédéric Besson

Peter Sewell (Cambridge) REMS Short Introduction

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

10:30 - 10:35
Talk

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 SagivTel Aviv University

10:30 - 11:00
Talk

Verification Challenges in Applications of Blockchain for Business Collaboration

Takaaki TateishiIBM Research - Tokyo

11:00 - 11:30
Talk

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

Adam ChlipalaMIT

11:30 - 12:00
Talk

Parallel-Correctness and Transferability for Conjunctive Queries

Frank Neven

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 GhicaUniversity of Birmingham, Khulood Alyahya, Victor Patentasu

How Far Apart Should Those Programs Be?

10:55 - 11:20
Talk

Ugo Dal LagoUniversity of Bologna, France

Programming Quantum Annealers

11:20 - 11:45
Talk

George Stelle, Scott Pakin

Understanding the POSIX Shell as a Programming Language

11:45 - 12:10
Talk

Michael GreenbergPomona College

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

12:00 - 14:00
Lunch

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

14:00 - 15:30: CoqPL 2017 - Midday Session at Auditorium
Chair(s): Sandrine BlazyUniversity of Rennes 1, France

14:00 - 15:00
Talk

Nicolas TabareauInria, France

15:00 - 15:30
Demonstration

Session with the Coq Development Team

Matthieu SozeauInria

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

14:00 - 14:30
Talk

Security

Michael HicksUniversity of Maryland at College Park, USA

14:30 - 15:00
Talk

Big Code

Bor-Yuh Evan ChangUniversity of Colorado Boulder

15:00 - 15:30
Talk

Program synthesis

Eran YahavTechnion

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 FosterCornell University

14:00 - 14:45
Talk

Synthesizing Data-parallel Programs

Aws AlbarghouthiUniversity of Wisconsin - Madison

14:45 - 15:30
Talk

Cosette: A Solver for SQL Equivalences

Alvin CheungUniversity of Washington

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

14:00 - 15:00
Talk

Keynote talk: Varieties of Programming Experience

Alan BlackwellUniversity of Cambridge

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

Synthetic topology in HoTT for probabilistic programming

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

16:00 - 16:25
Talk

Florian Faissole, Bas Spitters

CertiCoq: A verified compiler for Coq

16:25 - 16:50
Talk

Abhishek Anand, Andrew AppelPrinceton, Greg MorrisettCornell University, Zoe ParaskevopoulouPrinceton University, USA, Randy PollackHarvard University, Olivier Savary BelangerPrinceton University, Matthieu SozeauInria, Matthew WeaverPrinceton University

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

16:50 - 17:15
Talk

Izumi AsakuraTokyo Institute of Technology, Japan, Hidehiko MasuharaTokyo Institute of Technology, Tomoyuki AotaniTokyo Institute of Technology

Verification of Implementations of Distributed Systems Under Churn

17:15 - 17:40
Talk

Ryan DoengesUniversity of Washington, James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington, Zachary TatlockUniversity of Washington, Karl Palmskog

Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations

17:40 - 18:05
Talk

Nicolas Magaud

Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models

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

16:00 - 16:30
Talk

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 AldrichCarnegie Mellon University, Joshua SunshineCarnegie Mellon University

16:25 - 16:50
Talk

Laziness Boxes You In

Jose CalderonGalois, Inc., Stephen Magill

Programming with Epistemic Logic

16:50 - 17:15
Talk

Markus Eger, Chris MartensCarnegie Mellon University

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

17:15 - 17:40
Talk

Marco GaboardiSUNY Buffalo, USA

Running Incomplete Programs

17:40 - 18:05
Talk

Ian VoyseyCarnegie Mellon University, Cyrus OmarCarnegie Mellon University, Matthew HammerUniversity of Colorado, Boulder