POPL 2017
Sun 15 - Sat 21 January 2017
Toggle navigation
Attending
Campus: Paris Jussieu
Proceedings
Students
Registration
Practical information
Visas
Accommodation
Banner image credits
Program
Complete Program
Your Program
Filter by Day
Sun 15 Jan
Mon 16 Jan
Tue 17 Jan
Wed 18 Jan
Thu 19 Jan
Fri 20 Jan
Sat 21 Jan
Tracks
POPL 2017
Tutorials
Student Research Competition
POPL
Artifact Evaluation
Co-hosted Conferences
CPP
CPP
CPP
VMCAI
VMCAI
VMCAI
Workshops
PPS
CoqPL
N40AI
Next 40 years of Abstract Interpretation
Off the Beaten Track
OBT
PEPM
PLMW
PLMW
PiP
RDP
SCM
TTT
Co-hosted Symposia
PADL
Organization
POPL 2017 Committees
Organizing Committee
Steering Committee
Track Committees
Student Research Competition
POPL
Program Committee
External Review Committee
Artifact Evaluation
Contributors
People Index
Co-hosted Conferences
CPP
Program Committee
VMCAI
Organizing Committee
Program committee
Steering Committee
Program Chairs
Workshops
PPS
Program Committee
CoqPL
Program Committee
N40AI
Organizer
Off the Beaten Track
Organizing Committee
Program Committee
PEPM
Programme Committee
Programme Committee
PLMW
Speaker
Program Committee
PiP
Program Committee
RDP
Program Committee
SCM
Organizing Committee
TTT
Program Committee
Co-hosted Symposia
PADL
Organizing Committee
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 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
Student Research Competition
at
Auditorium
Chair(s):
Kim Nguyễn
LRI, Université Paris-Sud
09:00
5m
Awards
Student Competition Award
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
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
Sat 12 Oct 12:28