POPL 2017
Sun 15 - Sat 21 January 2017
VenueParis Jussieu
Room nameAuditorium
Floor0
Room numberAAA
Capacity500
Additional informationThere is no additional information of this room available.
Program

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00: Invited TalkCPP at Auditorium
09:00 - 10:00
Talk
Porting the HOL Light Analysis Library: Some Lessons
CPP
Lawrence PaulsonUniversity of Cambridge
File Attached

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00: Invited TalkCPP at Auditorium
09:00 - 10:00
Talk
Mechanized verification of preemptive OS kernels
CPP
Xinyu FengUniversity of Science and Technology of China
File Attached
10:30 - 12:00: Verified programming toolsCPP at Auditorium
10:30 - 11:00
Talk
Verified compilation of CakeML to multiple machine-code targets
CPP
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
CPP
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
CPP
William ManskyUniversity of Pennsylvania, Yuanfeng PengUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania, Joseph DeviettiUniversity of Pennsylvania
16:00 - 17:30: Formal verification of programming language foundationsCPP at Auditorium
16:00 - 16:30
Talk
Type-and-scope safe programs and their proofs
CPP
Guillaume AllaisRadboud University Nijmegen, James Chapman, Conor McBride, James McKinnaUniversity of Edinburgh
16:30 - 17:00
Talk
Formally verified differential dynamic logic
CPP
17:00 - 17:30
Talk
Equivalence of System F and λ2 in Coq based on context morphism lemmas
CPP

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05: OpeningPOPL at Auditorium
Chair(s): Giuseppe CastagnaParis Diderot University & CNRS, Andrew D. GordonMicrosoft Research and University of Edinburgh
09:00 - 09:05
Day opening
Opening
POPL
09:05 - 10:00: Invited speakerPOPL at Auditorium
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh
09:05 - 10:00
Talk
The Influence of Dependent Types
POPL
Stephanie WeirichUniversity of Pennsylvania
10:30 - 12:10: Type Systems 1POPL at Auditorium
Chair(s): Avik ChaudhuriFacebook
10:30 - 10:55
Talk
Polymorphism, subtyping and type inference in MLsub
POPL
Stephen Dolan, Alan MycroftUniversity of Cambridge
10:55 - 11:20
Talk
Java generics are Turing complete
POPL
Radu GrigoreUniversity of Kent
11:20 - 11:45
Talk
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
POPL
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
POPL
Karl CraryCarnegie Mellon University
14:20 - 16:00: Concurrency 1POPL at Auditorium
Chair(s): Ilya SergeyUniversity College London
14:20 - 14:45
Talk
A Promising Semantics for Relaxed-Memory Concurrency
POPL
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
POPL
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
POPL
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
POPL
Morten Krogh-JespersenAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University
16:30 - 17:45: Compiler OptimisationPOPL at Auditorium
Chair(s): Andrew C. MyersCornell University
16:30 - 16:55
Talk
A Program Optimization for Automatic Database Result Caching
POPL
Ziv ScullyCarnegie Mellon University, Adam ChlipalaMIT
16:55 - 17:20
Talk
Stream Fusion, to Completeness
POPL
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
POPL
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
Pre-print

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:15: ACM and SIGPLAN AwardsPOPL at Auditorium
Chair(s): Satnam SinghFacebook
09:00 - 09:05
Awards
Turing Award Video
POPL
09:05 - 09:10
Awards
Most Influential Paper Award
POPL
09:10 - 09:15
Awards
Reynolds Doctoral Dissertation Award
POPL
09:15 - 10:00: Invited speakerPOPL at Auditorium
Chair(s): Roberto GiacobazziUniversity of Verona, Italy
09:15 - 10:00
Talk
40 Years of Abstract Interpretation — An Interview with Patrick Cousot
POPL
Patrick CousotNew York University, Roberto GiacobazziUniversity of Verona, Italy
10:30 - 12:10: Type Systems 2POPL 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
POPL
Gabriel SchererNortheastern University
10:55 - 11:20
Talk
The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
POPL
Danko IlikTrusted Labs
11:20 - 11:45
Talk
Contextual isomorphisms
POPL
11:45 - 12:10
Talk
Typed Self-Evaluation via Intensional Type Functions
POPL
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles
14:20 - 16:00: Functional Programming with EffectsPOPL at Auditorium
Chair(s): Kathleen FisherTufts University
14:20 - 14:45
Talk
Type Directed Compilation of Row-Typed Algebraic Effects
POPL
Daan LeijenMicrosoft Research
14:45 - 15:10
Talk
Do be do be do
POPL
Sam LindleyUniversity of Edinburgh, Conor McBride, Craig McLaughlinThe University of Edinburgh
15:10 - 15:35
Talk
Dijkstra Monads for Free
POPL
Danel AhmanUniversity of Edinburgh, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris, ENS Paris, and Microsoft Research, Guido MartínezCIFASIS-CONICET, Argentina, Gordon Plotkin, Jonathan ProtzenkoMicrosoft Research, Aseem RastogiMicrosoft Research India, Nikhil SwamyMicrosoft Research
Pre-print
15:35 - 16:00
Talk
Stateful Manifest Contracts
POPL
16:30 - 17:20: Logic and ProgrammingPOPL at Auditorium
Chair(s): Nada AminEPFL
16:30 - 16:55
Talk
Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
POPL
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
POPL
17:20 - 18:20: Business meetingPOPL at Auditorium
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh
17:20 - 17:40
Talk
PC Chair report
POPL
Andrew D. GordonMicrosoft Research and University of Edinburgh
17:40 - 17:50
Talk
POPL 2018 presentation
POPL
Andrew C. MyersCornell University, Ranjit JhalaUniversity of California, San Diego
17:50 - 18:20
Meeting
SIGPLAN business meeting
POPL
C: Andrew D. GordonMicrosoft Research and University of Edinburgh

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05: Student Competition AwardStudent Research Competition at Auditorium
Chair(s): Kim NguyễnLRI, Université Paris-Sud
09:00 - 09:05
Awards
Student Competition Award
Student Research Competition
09:05 - 10:00: Invited speakerPOPL at Auditorium
Chair(s): Giuseppe CastagnaParis Diderot University & CNRS
09:05 - 10:00
Talk
Rust: from POPL to practice
POPL
10:30 - 12:10: Type Systems 3POPL at Auditorium
Chair(s): Derek DreyerMPI-SWS
10:30 - 10:55
Talk
Intersection Type Calculi of Bounded Dimension
POPL
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
10:55 - 11:20
Talk
Type Soundness Proofs with Definitional Interpreters
POPL
Nada AminEPFL, Tiark RompfPurdue University
11:20 - 11:45
Talk
Computational Higher-Dimensional Type Theory
POPL
Carlo AngiuliCarnegie Mellon University, Robert Harper, Todd WilsonCalifornia State University Fresno
11:45 - 12:10
Talk
Type Systems as Macros
POPL
Stephen ChangNortheastern University, Alex KnauthNortheastern University, Ben GreenmanNortheastern University
14:20 - 16:00: Gradual Typing and ContractsPOPL at Auditorium
Chair(s): Ronald GarciaUniversity of British Columbia
14:20 - 14:45
Talk
Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
POPL
Michael Vitousek, Cameron SwordsIndiana University, Jeremy G. SiekIndiana University Bloomington
14:45 - 15:10
Talk
Gradual Refinement Types
POPL
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
POPL
Matteo CiminiIndiana University, USA, Jeremy G. SiekIndiana University Bloomington
15:35 - 16:00
Talk
Sums of Uncertainty: Refinements go gradual
POPL
Khurram A. JaferyUniversity of British Columbia, Jana DunfieldUniversity of British Columbia
16:30 - 17:45: Security and PrivacyPOPL at Auditorium
Chair(s): Cătălin HriţcuInria Paris
16:30 - 16:55
Talk
LMS-Verify: Abstraction Without Regret for Verified Systems Programming
POPL
Nada AminEPFL, Tiark RompfPurdue University
16:55 - 17:20
Talk
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
POPL
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
POPL
Danfeng ZhangPennsylvania State University, Daniel KiferDept. of Computer Science and Engineering, Penn State University

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00: Opening SessionCoqPL 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
CoqPL
I: Robbert KrebbersDelft University of Technology, Netherlands
14:00 - 15:30: Midday SessionCoqPL at Auditorium
Chair(s): Sandrine BlazyUniversity of Rennes 1, France
14:00 - 15:00
Talk
Invited Talk -- Managing Logical and Computational Complexity using Program Transformations
CoqPL
I: Nicolas TabareauInria, France
15:00 - 15:30
Demonstration
Session with the Coq Development Team
CoqPL
16:00 - 18:05: Afternoon SessionCoqPL at Auditorium
Chair(s): Matthieu SozeauInria
16:00 - 16:25
Talk
Synthetic topology in HoTT for probabilistic programming
CoqPL
File Attached
16:25 - 16:50
Talk
CertiCoq: A verified compiler for Coq
CoqPL
Abhishek Anand, Andrew AppelPrinceton, Greg MorrisettCornell University, Zoe ParaskevopoulouPrinceton University, USA, Randy PollackHarvard University, Olivier Savary BelangerPrinceton University, Matthieu SozeauInria, Matthew WeaverPrinceton University
File Attached
16:50 - 17:15
Talk
CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
CoqPL
Izumi AsakuraTokyo Institute of Technology, Japan, Hidehiko MasuharaTokyo Institute of Technology, Tomoyuki AotaniTokyo Institute of Technology
File Attached
17:15 - 17:40
Talk
Verification of Implementations of Distributed Systems Under Churn
CoqPL
Ryan DoengesUniversity of Washington, James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Karl Palmskog
File Attached
17:40 - 18:05
Talk
Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
CoqPL
File Attached

Mon 16 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:0030
Auditorium