SCM 2017
Wed 18 - Fri 20 January 2017
co-located with
POPL 2017
Toggle navigation
Attending
Campus: Paris Jussieu
Program
SCM Program
Your Program
Wed 18 Jan
Thu 19 Jan
Fri 20 Jan
Track/Call
Organization
SCM 2017 Committees
Track Committees
Organizing Committee
Contributors
People Index
Search
Series
Sign in
Sign up
POPL 2017
(
series
) /
SCM 2017 (
series
) /
Paris Jussieu
/
Room information: Auditorium
Venue
Paris Jussieu
Room name
Auditorium
Floor
0
Room number
AAA
Capacity
500
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
.
Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-03:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-02:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
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 Talk
CPP
at
Auditorium
09:00
60m
Talk
Porting the HOL Light Analysis Library: Some Lessons
CPP
Lawrence Paulson
University of Cambridge
File Attached
10:30 - 12:00
Algorithm and library verification
CPP
at
Auditorium
10:30
30m
Talk
Verifying a hash table and its iterators in higher-order separation logic
CPP
François Pottier
11:00
30m
Talk
A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
CPP
Jose Divasón
,
Sebastiaan Joosten
,
René Thiemann
University of Innsbruck
,
Akihisa Yamada
11:30
30m
Talk
Formal foundations of 3D geometry for modeling robot manipulators
CPP
Reynald Affeldt
AIST, Japan
,
Cyril Cohen
14:00 - 15:30
Automated proof and its verification
CPP
at
Auditorium
14:00
30m
Talk
BliStrTune: Hierarchical Invention of Theorem Proving Strategies
CPP
Jan Jakubuv
,
Josef Urban
14:30
30m
Talk
Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
CPP
Reuben Rowe
University College London
,
James Brotherston
15:00
30m
Talk
Formalization of Karp-Miller Tree Construction on Petri Nets
CPP
Mitsuharu Yamamoto
,
Shogo Sekine
,
Saki Matsumoto
16:00 - 18:00
Formalized mathematics with numerical computations
CPP
at
Auditorium
16:00
30m
Talk
A Coq Formal Proof of the Lax–Milgram theorem
CPP
Sylvie Boldo
,
François Clément
,
Florian Faissole
,
Vincent Martin
,
Micaela Mayero
16:30
30m
Talk
A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations
CPP
Erik Martin-Dorel
IRIT, Université Paul Sabatier
,
Pierre Roux
17:00
30m
Talk
Markov Processes in Isabelle/HOL
CPP
Johannes Hölzl
Technische Universität München
DOI
Pre-print
File Attached
17:30
30m
Talk
Formalising Real Numbers in Homotopy Type Theory
CPP
Gaetan Gilbert
Tue 17 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
09:00 - 10:00
Invited Talk
CPP
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 tools
CPP
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
14:00 - 15:30
Homotopy type theory
CPP
at
Auditorium
14:00
30m
Talk
The HoTT library: a formalization of homotopy type theory in Coq
CPP
Andrej Bauer
University of Ljubljana
,
Jason Gross
MIT CSAIL
,
Peter Lefanu Lumsdaine
,
Michael Shulman
,
Matthieu Sozeau
Inria
,
Bas Spitters
Pre-print
14:30
30m
Talk
Lifting proof-relevant unification to higher dimensions
CPP
Jesper Cockx
iMinds, Belgium
,
Dominique Devriese
iMinds - Distrinet, KU Leuven
15:00
30m
Talk
The Next 700 Syntactical models of type theory
CPP
Simon Boulier
,
Pierre-Marie Pédrot
,
Nicolas Tabareau
Inria, France
16:00 - 17:30
Formal verification of programming language foundations
CPP
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
Brandon Bohrer
,
Vincent Rahli
SnT
,
Ivana Vukotic
,
Marcus Voelp
,
André Platzer
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
Opening
POPL
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 speaker
POPL
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 1
POPL
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 1
POPL
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 Optimisation
POPL
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 Awards
POPL
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 speaker
POPL
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 2
POPL
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
Paul Blain Levy
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 Effects
POPL
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 Programming
POPL
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
Eryk Kopczynski
,
Szymon Toruńczyk
17:20 - 18:20
Business meeting
POPL
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 Award
POPL 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 speaker
POPL
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 3
POPL
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 Contracts
POPL
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 Privacy
POPL
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 Session
CoqPL
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
10:30 - 12:10
Morning Session
CoqPL
at
Auditorium
Chair(s):
Alan Schmitt
Inria
10:30
25m
Talk
IxFree: Step-Indexed Logical Relations in Coq
CoqPL
Piotr Polesiuk
File Attached
10:55
25m
Talk
Logical Relations in Iris
CoqPL
Amin Timany
imec - Distrinet, KU Leuven
,
Robbert Krebbers
Delft University of Technology, Netherlands
,
Lars Birkedal
Aarhus University
File Attached
11:20
25m
Talk
Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting
CoqPL
Edwin Westbrook
Galois, Inc.
,
Gregory Malecha
UCSD
File Attached
11:45
25m
Talk
ppsimpl: a reflexive Coq tactic for canonising goals
CoqPL
Frédéric Besson
File Attached
14:00 - 15:30
Midday Session
CoqPL
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
Matthieu Sozeau
Inria
16:00 - 18:05
Afternoon Session
CoqPL
at
Auditorium
Chair(s):
Matthieu Sozeau
Inria
16:00
25m
Talk
Synthetic topology in HoTT for probabilistic programming
CoqPL
Florian Faissole
,
Bas Spitters
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
Nicolas Magaud
File Attached
Mon 16 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
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
Auditorium
CPP
Invited Talk
CPP
Algorithm and library verification
CPP
Automated proof and its verification
CPP
Formalized mathematics with numerical computations
Tue 17 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
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
Auditorium
CPP
Invited Talk
CPP
Verified programming tools
CPP
Homotopy type theory
CPP
Formal verification of programming language foundations
Wed 18 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
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
Auditorium
POPL
Opening
POPL
Invited speaker
POPL
Type Systems 1
POPL
Concurrency 1
POPL
Compiler Optimisation
Thu 19 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
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
Auditorium
POPL
ACM and SIGPLAN Awards
POPL
Invited speaker
POPL
Type Systems 2
POPL
Functional Programming with Effects
POPL
Logic and Programming
POPL
Business meeting
Fri 20 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
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
Auditorium
POPL Student Research Competition
Student Competition Award
POPL
Invited speaker
POPL
Type Systems 3
POPL
Gradual Typing and Contracts
POPL
Security and Privacy
Sat 21 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
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
Auditorium
CoqPL
Opening Session
CoqPL
Morning Session
CoqPL
Midday Session
CoqPL
Afternoon Session
Mon 16 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
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
Auditorium
CPP
Porting the HOL Light Analysis Library: Some Lessons
09:00 - 10:00
CPP
Verifying a hash table and its iterators in higher-order separation logic
10:30 - 11:00
CPP
A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
11:00 - 11:30
CPP
Formal foundations of 3D geometry for modeling robot manipulators
11:30 - 12:00
CPP
BliStrTune: Hierarchical Invention of Theorem Proving Strategies
14:00 - 14:30
CPP
Automatic Cyclic Termination Proofs for Recursive Procedures in Separat ...
14:30 - 15:00
CPP
Formalization of Karp-Miller Tree Construction on Petri Nets
15:00 - 15:30
CPP
A Coq Formal Proof of the Lax–Milgram theorem
16:00 - 16:30
CPP
A Reflexive Tactic for Polynomial Positivity using Numerical Solvers an ...
16:30 - 17:00
CPP
Markov Processes in Isabelle/HOL
17:00 - 17:30
CPP
Formalising Real Numbers in Homotopy Type Theory
17:30 - 18:00
Tue 17 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
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
Auditorium
CPP
Mechanized verification of preemptive OS kernels
09:00 - 10:00
CPP
Verified compilation of CakeML to multiple machine-code targets
10:30 - 11:00
CPP
COMPLX: a verification framework for concurrent imperative programs
11:00 - 11:30
CPP
Verifying dynamic race detection
11:30 - 12:00
CPP
The HoTT library: a formalization of homotopy type theory in Coq
14:00 - 14:30
CPP
Lifting proof-relevant unification to higher dimensions
14:30 - 15:00
CPP
The Next 700 Syntactical models of type theory
15:00 - 15:30
CPP
Type-and-scope safe programs and their proofs
16:00 - 16:30
CPP
Formally verified differential dynamic logic
16:30 - 17:00
CPP
Equivalence of System F and λ2 in Coq based on context morphism lemmas
17:00 - 17:30
Wed 18 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
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
Auditorium
POPL
Opening
09:00 - 09:05
POPL
The Influence of Dependent Types
09:05 - 10:00
POPL
Polymorphism, subtyping and type inference in MLsub
10:30 - 10:55
POPL
Java generics are Turing complete
10:55 - 11:20
POPL
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
11:20 - 11:45
POPL
Modules, Abstraction, and Parametric Polymorphism
11:45 - 12:10
POPL
A Promising Semantics for Relaxed-Memory Concurrency
14:20 - 14:45
POPL
Automatically Comparing Memory Consistency Models
14:45 - 15:10
POPL
Interactive Proofs in Higher-Order Concurrent Separation Logic
15:10 - 15:35
POPL
A Relational Model of Types-and-Effects in Higher-Order Concurrent Sepa ...
15:35 - 16:00
POPL
A Program Optimization for Automatic Database Result Caching
16:30 - 16:55
POPL
Stream Fusion, to Completeness
16:55 - 17:20
POPL
Rigorous Floating-point Mixed Precision Tuning
17:20 - 17:45
Thu 19 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
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
Auditorium
POPL
Turing Award Video
09:00 - 09:05
POPL
Most Influential Paper Award
09:05 - 09:10
POPL
Reynolds Doctoral Dissertation Award
09:10 - 09:15
POPL
40 Years of Abstract Interpretation — An Interview with Patrick Cousot
09:15 - 10:00
POPL
Deciding equivalence with sums and the empty type
10:30 - 10:55
POPL
The exp-log normal form of types: Decomposing extensional equality and ...
10:55 - 11:20
POPL
Contextual isomorphisms
11:20 - 11:45
POPL
Typed Self-Evaluation via Intensional Type Functions
11:45 - 12:10
POPL
Type Directed Compilation of Row-Typed Algebraic Effects
14:20 - 14:45
POPL
Do be do be do
14:45 - 15:10
POPL
Dijkstra Monads for Free
15:10 - 15:35
POPL
Stateful Manifest Contracts
15:35 - 16:00
POPL
Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
16:30 - 16:55
POPL
LOIS: syntax and semantics
16:55 - 17:20
POPL
PC Chair report
17:20 - 17:40
POPL
POPL 2018 presentation
17:40 - 17:50
POPL
SIGPLAN business meeting
17:50 - 18:20
Fri 20 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
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
Auditorium
POPL Student Research Competition
Student Competition Award
09:00 - 09:05
POPL
Rust: from POPL to practice
09:05 - 10:00
POPL
Intersection Type Calculi of Bounded Dimension
10:30 - 10:55
POPL
Type Soundness Proofs with Definitional Interpreters
10:55 - 11:20
POPL
Computational Higher-Dimensional Type Theory
11:20 - 11:45
POPL
Type Systems as Macros
11:45 - 12:10
POPL
Big Types in Little Runtime: Open World Soundness and Collaborative Bla ...
14:20 - 14:45
POPL
Gradual Refinement Types
14:45 - 15:10
POPL
Automatically Generating the Dynamic Semantics of Gradually Typed Languages
15:10 - 15:35
POPL
Sums of Uncertainty: Refinements go gradual
15:35 - 16:00
POPL
LMS-Verify: Abstraction Without Regret for Verified Systems Programming
16:30 - 16:55
POPL
Hypercollecting Semantics and its Application to Static Analysis of Inf ...
16:55 - 17:20
POPL
LightDP: Towards Automating Differential Privacy Proofs
17:20 - 17:45
Sat 21 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
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
Auditorium
CoqPL
Invited Talk -- Demonstration of the Iris separation logic in Coq
09:00 - 10:00
CoqPL
IxFree: Step-Indexed Logical Relations in Coq
10:30 - 10:55
CoqPL
Logical Relations in Iris
10:55 - 11:20
CoqPL
Predicate Monads: A Framework for Proving Generic Properties of Monadic ...
11:20 - 11:45
CoqPL
ppsimpl: a reflexive Coq tactic for canonising goals
11:45 - 12:10
CoqPL
Invited Talk -- Managing Logical and Computational Complexity using Pro ...
14:00 - 15:00
CoqPL
Session with the Coq Development Team
15:00 - 15:30
CoqPL
Synthetic topology in HoTT for probabilistic programming
16:00 - 16:25
CoqPL
CertiCoq: A verified compiler for Coq
16:25 - 16:50
CoqPL
CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL
16:50 - 17:15
CoqPL
Verification of Implementations of Distributed Systems Under Churn
17:15 - 17:40
CoqPL
Transferring Arithmetic Decision Procedures (on Z) to Alternative Repre ...
17:40 - 18:05
x
Sun 24 Nov 01:15