SCM 2017
Wed 18 - Fri 20 January 2017
co-located with POPL 2017
VenueParis Jussieu
Room nameAuditorium
Floor0
Room numberAAA
Capacity500
Room InformationNo extra information available
Program

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

Mon 16 Jan

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

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

Tue 17 Jan

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

09:00 - 10:00
Invited TalkCPP at Auditorium
09:00
60m
Talk
Mechanized verification of preemptive OS kernels
CPP
Xinyu Feng University of Science and Technology of China
File Attached
10:30 - 12:00
Verified programming toolsCPP at Auditorium
10:30
30m
Talk
Verified compilation of CakeML to multiple machine-code targets
CPP
Anthony Fox University of Cambridge, UK, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan IHPC at A*STAR, Singapore, Ramana Kumar
11:00
30m
Talk
COMPLX: a verification framework for concurrent imperative programs
CPP
Sidney Amani UNSW, Australia, June Andronick Data61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin , Corey Lewis , Christine Rizkallah University of Pennsylvania, USA, Joseph Tuong
11:30
30m
Talk
Verifying dynamic race detection
CPP
William Mansky University of Pennsylvania, Yuanfeng Peng University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Joseph Devietti University of Pennsylvania
16:00 - 17:30
Formal verification of programming language foundationsCPP at Auditorium
16:00
30m
Talk
Type-and-scope safe programs and their proofs
CPP
Guillaume Allais Radboud University Nijmegen, James Chapman , Conor McBride , James McKinna University of Edinburgh
16:30
30m
Talk
Formally verified differential dynamic logic
CPP
17:00
30m
Talk
Equivalence of System F and λ2 in Coq based on context morphism lemmas
CPP
Jonas Kaiser , Tobias Tebbi , Gert Smolka Saarland University

Wed 18 Jan

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

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

09:05 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
09:05
55m
Talk
The Influence of Dependent Types
POPL
Stephanie Weirich University of Pennsylvania
10:30 - 12:10
Type Systems 1POPL at Auditorium
Chair(s): Avik Chaudhuri Facebook
10:30
25m
Talk
Polymorphism, subtyping and type inference in MLsub
POPL
Stephen Dolan , Alan Mycroft University of Cambridge
10:55
25m
Talk
Java generics are Turing complete
POPL
Radu Grigore University of Kent
11:20
25m
Talk
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
POPL
Cyrus Omar Carnegie Mellon University, Ian Voysey Carnegie Mellon University, Michael Hilton Oregon State University, USA, Jonathan Aldrich Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder
11:45
25m
Talk
Modules, Abstraction, and Parametric Polymorphism
POPL
Karl Crary Carnegie Mellon University
14:20 - 16:00
Concurrency 1POPL at Auditorium
Chair(s): Ilya Sergey University College London
14:20
25m
Talk
A Promising Semantics for Relaxed-Memory Concurrency
POPL
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWS
Link to publication Pre-print Media Attached
14:45
25m
Talk
Automatically Comparing Memory Consistency Models
POPL
John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UK
Pre-print Media Attached File Attached
15:10
25m
Talk
Interactive Proofs in Higher-Order Concurrent Separation Logic
POPL
Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus University
DOI Pre-print Media Attached
15:35
25m
Talk
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
POPL
Morten Krogh-Jespersen Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University
16:30 - 17:45
Compiler OptimisationPOPL at Auditorium
Chair(s): Andrew Myers Cornell University
16:30
25m
Talk
A Program Optimization for Automatic Database Result Caching
POPL
Ziv Scully Carnegie Mellon University, Adam Chlipala MIT
16:55
25m
Talk
Stream Fusion, to Completeness
POPL
Oleg Kiselyov , Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens
Pre-print Media Attached
17:20
25m
Talk
Rigorous Floating-point Mixed Precision Tuning
POPL
Wei-Fan Chiang School of Computing, University of Utah, Ganesh Gopalakrishnan University of Utah, Zvonimir Rakamaric University of Utah, Ian Briggs School of Computing, University of Utah, Marek S. Baranowski University of Utah, Alexey Solovyev School of Computing, University of Utah
Pre-print

Thu 19 Jan

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

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

09:05
5m
Awards
Most Influential Paper Award
POPL

09:10
5m
Awards
Reynolds Doctoral Dissertation Award
POPL

09:15 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Roberto Giacobazzi University of Verona, Italy
09:15
45m
Talk
40 Years of Abstract Interpretation — An Interview with Patrick Cousot
POPL
Patrick Cousot New York University, Roberto Giacobazzi University of Verona, Italy
10:30 - 12:10
Type Systems 2POPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
10:30
25m
Talk
Deciding equivalence with sums and the empty type
POPL
Gabriel Scherer Northeastern University
10:55
25m
Talk
The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
POPL
Danko Ilik Trusted Labs
11:20
25m
Talk
Contextual isomorphisms
POPL
11:45
25m
Talk
Typed Self-Evaluation via Intensional Type Functions
POPL
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles
14:20 - 16:00
Functional Programming with EffectsPOPL at Auditorium
Chair(s): Kathleen Fisher Tufts University
14:20
25m
Talk
Type Directed Compilation of Row-Typed Algebraic Effects
POPL
Daan Leijen Microsoft Research
14:45
25m
Talk
Do be do be do
POPL
Sam Lindley University of Edinburgh, Conor McBride , Craig McLaughlin The University of Edinburgh
15:10
25m
Talk
Dijkstra Monads for Free
POPL
Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Guido Martínez CIFASIS-CONICET, Argentina, Gordon Plotkin , Jonathan Protzenko Microsoft Research, Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft Research
Pre-print
15:35
25m
Talk
Stateful Manifest Contracts
POPL
Taro Sekiyama , Atsushi Igarashi Kyoto University
16:30 - 17:20
Logic and ProgrammingPOPL at Auditorium
Chair(s): Nada Amin EPFL
16:30
25m
Talk
Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
POPL
Kausik Subramanian University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison, Aditya Akella University of Wisconsin-Madison
16:55
25m
Talk
LOIS: syntax and semantics
POPL
17:20 - 18:20
Business meetingPOPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
17:20
20m
Talk
PC Chair report
POPL
Andrew D. Gordon Microsoft Research and University of Edinburgh
17:40
10m
Talk
POPL 2018 presentation
POPL
Andrew Myers Cornell University, Ranjit Jhala University of California, San Diego
17:50
30m
Meeting
SIGPLAN business meeting
POPL
C: Andrew D. Gordon Microsoft Research and University of Edinburgh

Fri 20 Jan

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

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

09:05 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Giuseppe Castagna Paris Diderot University & CNRS
09:05
55m
Talk
Rust: from POPL to practice
POPL
Aaron Turon MPI-SWS
10:30 - 12:10
Type Systems 3POPL at Auditorium
Chair(s): Derek Dreyer MPI-SWS
10:30
25m
Talk
Intersection Type Calculi of Bounded Dimension
POPL
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
10:55
25m
Talk
Type Soundness Proofs with Definitional Interpreters
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
11:20
25m
Talk
Computational Higher-Dimensional Type Theory
POPL
Carlo Angiuli Carnegie Mellon University, Robert Harper , Todd Wilson California State University Fresno
11:45
25m
Talk
Type Systems as Macros
POPL
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University
14:20 - 16:00
Gradual Typing and ContractsPOPL at Auditorium
Chair(s): Ronald Garcia University of British Columbia
14:20
25m
Talk
Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
POPL
Michael Vitousek , Cameron Swords Indiana University, Jeremy G. Siek Indiana University Bloomington
14:45
25m
Talk
Gradual Refinement Types
POPL
Nicolás Lehmann , Éric Tanter University of Chile, Chile
Link to publication DOI Pre-print
15:10
25m
Talk
Automatically Generating the Dynamic Semantics of Gradually Typed Languages
POPL
Matteo Cimini Indiana University, USA, Jeremy G. Siek Indiana University Bloomington
15:35
25m
Talk
Sums of Uncertainty: Refinements go gradual
POPL
Khurram A. Jafery University of British Columbia, Jana Dunfield University of British Columbia
16:30 - 17:45
Security and PrivacyPOPL at Auditorium
Chair(s): Cătălin Hriţcu Inria Paris
16:30
25m
Talk
LMS-Verify: Abstraction Without Regret for Verified Systems Programming
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
16:55
25m
Talk
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
POPL
Mounir Assaf Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Julien Signoles CEA LIST, Éric Totel CentraleSupélec, Frédéric Tronel CentraleSupélec
17:20
25m
Talk
LightDP: Towards Automating Differential Privacy Proofs
POPL
Danfeng Zhang Pennsylvania State University, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University

Sat 21 Jan

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

09:00 - 10:00
Opening SessionCoqPL at Auditorium
Chair(s): Emilio Jesús Gallego Arias MINES ParisTech
09:00
60m
Talk
Invited Talk -- Demonstration of the Iris separation logic in Coq
CoqPL
I: Robbert Krebbers Delft University of Technology, Netherlands
14:00 - 15:30
Midday SessionCoqPL at Auditorium
Chair(s): Sandrine Blazy University of Rennes 1, France
14:00
60m
Talk
Invited Talk -- Managing Logical and Computational Complexity using Program Transformations
CoqPL
I: Nicolas Tabareau Inria, France
15:00
30m
Demonstration
Session with the Coq Development Team
CoqPL
16:00 - 18:05
Afternoon SessionCoqPL at Auditorium
Chair(s): Matthieu Sozeau Inria
16:00
25m
Talk
Synthetic topology in HoTT for probabilistic programming
CoqPL
File Attached
16:25
25m
Talk
CertiCoq: A verified compiler for Coq
CoqPL
Abhishek Anand , Andrew W. Appel Princeton, Greg Morrisett Cornell University, Zoe Paraskevopoulou Princeton University, USA, Randy Pollack Harvard University, Olivier Savary Belanger Princeton University, Matthieu Sozeau Inria, Matthew Weaver Princeton University
File Attached
16:50
25m
Talk
CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
CoqPL
Izumi Asakura Tokyo Institute of Technology, Japan, Hidehiko Masuhara Tokyo Institute of Technology, Tomoyuki Aotani Tokyo Institute of Technology
File Attached
17:15
25m
Talk
Verification of Implementations of Distributed Systems Under Churn
CoqPL
Ryan Doenges University of Washington, James R. Wilcox University of Washington, Doug Woos University of Washington, Zachary Tatlock University of Washington, Seattle, Karl Palmskog
File Attached
17:40
25m
Talk
Transferring Arithmetic Decision Procedures (on Z) to Alternative Representations
CoqPL
File Attached

Mon 16 Jan

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

Tue 17 Jan

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

Wed 18 Jan

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

Thu 19 Jan

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

Fri 20 Jan

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

Sat 21 Jan

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

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