Write a Blog >>
POPL 2016
Wed 20 - Sat 23 January 2016
St. Petersburg, Florida, United States
Toggle navigation
Attending
Venue: Hilton St. Petersburg Bayfront
Registration
Accommodation
Student Volunteers
Financial Support
Travel
Visas
Conduct
Program
Complete Program
Your Program
Filter by Day
Sun 17 Jan
Mon 18 Jan
Tue 19 Jan
Wed 20 Jan
Thu 21 Jan
Fri 22 Jan
Sat 23 Jan
Tracks
POPL 2016
Invited Speakers
Artifact Evaluation
Tutorials
Research Papers
SRC
Co-hosted Conferences
CPP
CPP
CPP
VMCAI
VMCAI
VMCAI
Workshops
CoqPL
CoqPL
CoqPL
Off the Beaten Track
Off the Beaten Track
Off the Beaten Track
PEPM
PEPM
PEPM
Invited Talks
PEPM
PLMW
PLMW
PLMW
PPS
PPS
PPS
Co-hosted Symposia
PADL
PADL
PADL
Organization
POPL 2016 Committees
Organizing Committee
Program Committee
External Reviewing Committee
Steering Committee
Track Committees
Artifact Evaluation
Tutorials
Research Papers
Program Committee
External Reviewing Committee
Contributors
People Index
Co-hosted Conferences
CPP
Program Committee
VMCAI
Program Chairs
Program Committee
Organizing Committee
Steering Committee
Workshops
CoqPL
Organizing Committee
Program Committee
Off the Beaten Track
Organizing Committee
Program Committee
PEPM
Program Committee
PLMW
Organizing Committee
PPS
Program Committee
Co-hosted Symposia
PADL
Organizers
Program 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 2016
(
series
) /
Hilton St. Petersburg Bayfront
/
Room information: Room St Petersburg II
Venue
Hilton St. Petersburg Bayfront
Room name
Room St Petersburg II
Floor
0
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-05:00) Guadalajara, Mexico City, Monterrey
.
Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey
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:30) 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+06: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+10: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 18 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
09:00 - 10:00
Session 1: Invited talk by Harvey Friedman
CPP
at
Room St Petersburg II
09:00
60m
Talk
Perspectives on Formal Verfication
CPP
Harvey Friedman
Ohio State University
10:30 - 12:00
Session 2: Verifying Imperative Programs
CPP
at
Room St Petersburg II
10:30
30m
Talk
Higher-order Representation Predicates in Separation Logic
CPP
Arthur Charguéraud
11:00
30m
Talk
A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
CPP
Tahina Ramananandro
,
Paul Mountcastle
,
Benoit Meister
,
Richard Lethin
11:30
30m
Talk
Refinement Based Verification of Imperative Data Structures
CPP
Peter Lammich
Technische Universität München
14:00 - 15:30
Session 3: Design and Implementation of Theorem Provers
CPP
at
Room St Petersburg II
14:00
30m
Talk
The Vampire and the FOOL
CPP
Evgenii Kotelnikov
Chalmers University of Technology
,
Laura Kovacs
Chalmers University of Technology
,
Giles Reger
University of Manchester
,
Andrei Voronkov
University of Manchester
14:30
30m
Talk
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
CPP
Lukasz Czajka
University of Innsbruck
15:00
30m
Talk
Mizar Environment for Isabelle
CPP
Cezary Kaliszyk
University of Innsbruck
,
Karol Pąk
University of Bialystok, Institute of Computer Science
,
Josef Urban
16:00 - 18:00
Session 4: Mathematics
CPP
at
Room St Petersburg II
16:00
30m
Talk
A Modular, Efficient Formalisation of Real Algebraic Numbers
CPP
Wenda Li
University of Cambridge
,
Lawrence Paulson
Cambridge University
16:30
30m
Talk
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
CPP
Sophie Bernard
INRIA
,
Yves Bertot
INRIA
,
Laurence Rideau
INRIA
,
Pierre-Yves Strub
IMDEA Software Institute
17:00
30m
Talk
Formalizing Jordan Normal Forms in Isabelle/HOL
CPP
René Thiemann
University of Innsbruck
,
Akihisa Yamada
17:30
30m
Talk
Formalization of a Newton series representation of polynomials
CPP
Cyril Cohen
,
Boris Djalal
INRIA
Tue 19 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
09:00 - 10:00
Session 5: Invited talk by Leonardo de Moura
CPP
at
Room St Petersburg II
09:00
60m
Talk
Dependent Type Practice
CPP
Leonardo de Moura
Microsoft Research, Redmond
10:30 - 12:00
Session 6: Foundations
CPP
at
Room St Petersburg II
10:30
30m
Talk
A Logic of Proofs for Differential Dynamic Logic
CPP
Nathan Fulton
Carnegie Mellon University
,
André Platzer
11:00
30m
Talk
Constructing the Propositional Truncation using Non-recursive HITs
CPP
Floris van Doorn
Carnegie Mellon University
11:30
30m
Talk
A Nominal Exploration of Intuitionism
CPP
Vincent Rahli
SnT
,
Mark Bickford
Cornell University
14:00 - 15:30
Session 7: Verification for Concurrent and Distributed Systems
CPP
at
Room St Petersburg II
14:00
30m
Talk
Bisimulation Up-to Techniques for Psi-calculi
CPP
Johannes Å. Pohjola
Uppsala University
,
Joachim Parrow
Uppsala University
14:30
30m
Talk
Planning for Change in a Formal Verification of the Raft Consensus Protocol
CPP
Doug Woos
University of Washington
,
James R. Wilcox
University of Washington
,
Steve Anton
University of Washington
,
Zachary Tatlock
University of Washington, Seattle
,
Michael D. Ernst
University of Washington
,
Thomas Anderson
University of Washington
Pre-print
15:00
30m
Talk
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
CPP
Michel St-Martin
University of Ottawa
,
Amy Felty
University of Ottawa
16:00 - 17:00
Session 8: Compiler Verification
CPP
at
Room St Petersburg II
16:00
30m
Talk
Formal Verification of Control-flow Graph Flattening
CPP
Sandrine Blazy
IRISA / University of Rennes 1
,
Alix Trieu
ENS Rennes
16:30
30m
Talk
Axiomatic Semantics for Compiler Verification
CPP
Steven Schäfer
,
Sigurd Schneider
Saarland University
,
Gert Smolka
Saarland University
Sat 23 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
09:00 - 10:00
Session 1
PPS
at
Room St Petersburg II
Chair(s):
Cameron Freer
Gamalon
09:00
20m
Talk
All You Need is the Monad... What Monad Was That Again?
PPS
Norman Ramsey
Pre-print
09:20
10m
Meeting
Discussion 1
PPS
09:30
20m
Talk
An Interface for Black Box Learning in Probabilistic Programs
PPS
Jan-Willem van de Meent
University of Oxford
,
Brooks Paige
University of Oxford
,
David Tolpin
University of Oxford
,
Frank Wood
University of Oxford
Pre-print
09:50
10m
Meeting
Discussion 2
PPS
10:30 - 12:15
Session 2
PPS
at
Room St Petersburg II
Chair(s):
Chad Scherrer
Galois, Inc.
10:30
20m
Talk
Models for Probabilistic Programs with an Adversary
PPS
Robert Rand
University of Pennsylvania
,
Steve Zdancewic
University of Pennsylvania
Pre-print
10:50
10m
Meeting
DIscussion 3
PPS
11:00
20m
Talk
The Semantics of Figaro, an Embedded Probabilistic Programming Language
PPS
Avi Pfeffer
Charles River Analytics
,
Brian Ruttenberg
Charles River Analytics
Pre-print
11:20
10m
Meeting
Discussion 4
PPS
11:30
45m
Meeting
Implementor Panel: What can semantics do for probabilistic programming and what can probabilistic programming do for semantics?
PPS
Angelika Kimmig
KU Leuven
,
Oleg Kiselyov
,
Jan-Willem van de Meent
University of Oxford
,
Avi Pfeffer
Charles River Analytics
,
M:
Frank Wood
University of Oxford
14:00 - 15:30
Session 3
PPS
at
Room St Petersburg II
Chair(s):
Mitchell Wand
Northeastern University
14:00
20m
Talk
A Lambda-Calculus Foundation for Universal Probabilistic Programming
PPS
Johannes Borgström
Uppsala University
,
Ugo Dal Lago
University of Bologna
,
Andrew D. Gordon
Microsoft Research and University of Edinburgh
,
Marcin Szymczak
University of Edinburgh
Pre-print
14:20
10m
Meeting
Discussion 5
PPS
14:30
20m
Talk
Making our Own Luck: A Language for Random Generators
PPS
Leonidas Lampropoulos
University of Pennsylvania
,
Benjamin C. Pierce
University of Pennsylvania
,
Cătălin Hriţcu
INRIA Paris
,
John Hughes
Chalmers University of Technology
,
Zoe Paraskevopoulou
Princeton University
,
Li-yao Xia
ENS Paris
Pre-print
14:50
10m
Meeting
Discussion 6
PPS
15:00
20m
Talk
Semantics of Higher-order Probabilistic Programs
PPS
Sam Staton
University of Oxford
,
Hongseok Yang
University of Oxford, UK
,
Chris Heunen
University of Edinburgh
,
Ohad Kammar
University of Cambridge
,
Frank Wood
University of Oxford
Pre-print
15:20
10m
Meeting
Discussion 7
PPS
15:30 - 16:30
Poster Session
PPS
at
Room St Petersburg II
15:30
60m
Meeting
Insomnia: Types and Modules for Probabilistic Programming
PPS
Aleksey Kliger
Xamarin, Inc.
,
Sean Stromsten
BAE Systems, Inc.
Pre-print
15:30
60m
Meeting
Finite-depth Higher-order Abstract Syntax Trees for Reasoning about Probabilistic Programs
PPS
Theophilos Giannakopoulos
BAE Systems, Inc.
,
Mitchell Wand
Northeastern University
,
Andrew Cobb
Northeastern University
Pre-print
15:30
60m
Meeting
Coalgebraic Trace Semantics for Probabilistic Processes: Preliminary Proposal
PPS
Larry Moss
Indiana University
,
Chung-chieh Shan
Indiana University
,
Alexandra Silva
Radboud University Nijmegen
Pre-print
15:30
60m
Meeting
Reasoning about Probability and Nondeterminism
PPS
Faris Abou-Saleh
University of Oxford
,
Kwok-Ho Cheung
University of Oxford
,
Jeremy Gibbons
University of Oxford, UK
Pre-print
15:30
60m
Meeting
Fixed Points for Markov Decision Processes
PPS
Johannes Hölzl
Technische Universität München
Pre-print
15:30
60m
Meeting
A Denotational Semantics of a Probabilistic Stream-Processing Language
PPS
Yohei Miyamoto
Graduate School of Informatics, Kyoto University
,
Kohei Suenaga
,
Koji Nakazawa
Graduate School of Information Science, Nagoya University
Pre-print
15:30
60m
Meeting
Observation Propagation for Importance Sampling with Likelihood Weighting
PPS
Ryan Culpepper
Northeastern University
Pre-print
15:30
60m
Meeting
Problems of the Lightweight Implementation of Probabilistic Programming
PPS
Oleg Kiselyov
Pre-print
15:30
60m
Meeting
Parameterized Probability Monad
PPS
Adam Ścibior
University of Cambridge
,
Andrew D. Gordon
Microsoft Research and University of Edinburgh
Pre-print
15:30
60m
Meeting
Reproducing Kernel Hilbert Space Semantics for Probabilistic Programs
PPS
Adam Ścibior
University of Cambridge
,
Bernhard Schölkopf
MPI Tuebingen
Pre-print
16:30 - 18:00
Session 5
PPS
at
Room St Petersburg II
Chair(s):
Chung-chieh Shan
Indiana University
16:30
20m
Talk
eXchangeable Random Primitives
PPS
Nathanael L. Ackerman
Harvard University
,
Cameron Freer
Gamalon
,
Daniel Roy
University of Toronto
Pre-print
16:50
10m
Meeting
Discussion 8
PPS
17:00
20m
Talk
An Application of Computable Distributions to the Semantics of Probabilistic Programs
PPS
Daniel Huang
Harvard University
,
Greg Morrisett
Cornell University
Pre-print
17:20
10m
Meeting
Discussion 9
PPS
17:30
20m
Talk
On The Semantic Intricacies of Conditioning
PPS
Friedrich Gretz
RWTH Aachen University
,
Nils Jansen
RWTH Aachen University
,
Benjamin Lucien Kaminski
RWTH Aachen University
,
Joost-Pieter Katoen
RWTH Aachen University
,
Federico Olmedo
RWTH Aachen University
Pre-print
17:50
10m
Meeting
Discussion 10
PPS
Mon 18 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg II
CPP
Session 1: Invited talk by Harvey Friedman
CPP
Session 2: Verifying Imperative Programs
CPP
Session 3: Design and Implementation of Theorem Provers
CPP
Session 4: Mathematics
Tue 19 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg II
CPP
Session 5: Invited talk by Leonardo de Moura
CPP
Session 6: Foundations
CPP
Session 7: Verification for Concurrent and Distributed Systems
CPP
Session 8: Compiler Verification
Sat 23 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg II
PPS
Session 1
PPS
Session 2
PPS
Session 3
PPS
Poster Session
PPS
Session 5
Mon 18 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg II
CPP
Perspectives on Formal Verfication
09:00 - 10:00
CPP
Higher-order Representation Predicates in Separation Logic
10:30 - 11:00
CPP
A Unified Coq Framework for Verifying C Programs with Floating-Point Co ...
11:00 - 11:30
CPP
Refinement Based Verification of Imperative Data Structures
11:30 - 12:00
CPP
The Vampire and the FOOL
14:00 - 14:30
CPP
Improving automation in interactive theorem provers by efficient encodi ...
14:30 - 15:00
CPP
Mizar Environment for Isabelle
15:00 - 15:30
CPP
A Modular, Efficient Formalisation of Real Algebraic Numbers
16:00 - 16:30
CPP
Formal proofs of transcendence for e and pi as an application of multiv ...
16:30 - 17:00
CPP
Formalizing Jordan Normal Forms in Isabelle/HOL
17:00 - 17:30
CPP
Formalization of a Newton series representation of polynomials
17:30 - 18:00
Tue 19 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg II
CPP
Dependent Type Practice
09:00 - 10:00
CPP
A Logic of Proofs for Differential Dynamic Logic
10:30 - 11:00
CPP
Constructing the Propositional Truncation using Non-recursive HITs
11:00 - 11:30
CPP
A Nominal Exploration of Intuitionism
11:30 - 12:00
CPP
Bisimulation Up-to Techniques for Psi-calculi
14:00 - 14:30
CPP
Planning for Change in a Formal Verification of the Raft Consensus Protocol
14:30 - 15:00
CPP
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
15:00 - 15:30
CPP
Formal Verification of Control-flow Graph Flattening
16:00 - 16:30
CPP
Axiomatic Semantics for Compiler Verification
16:30 - 17:00
Sat 23 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
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
Room St Petersburg II
PPS
All You Need is the Monad... What Monad Was That Again?
09:00 - 09:20
PPS
Discussion 1
09:20 - 09:30
PPS
An Interface for Black Box Learning in Probabilistic Programs
09:30 - 09:50
PPS
Discussion 2
09:50 - 10:00
PPS
Models for Probabilistic Programs with an Adversary
10:30 - 10:50
PPS
DIscussion 3
10:50 - 11:00
PPS
The Semantics of Figaro, an Embedded Probabilistic Programming Language
11:00 - 11:20
PPS
Discussion 4
11:20 - 11:30
PPS
Implementor Panel: What can semantics do for probabilistic programming ...
11:30 - 12:15
PPS
A Lambda-Calculus Foundation for Universal Probabilistic Programming
14:00 - 14:20
PPS
Discussion 5
14:20 - 14:30
PPS
Making our Own Luck: A Language for Random Generators
14:30 - 14:50
PPS
Discussion 6
14:50 - 15:00
PPS
Semantics of Higher-order Probabilistic Programs
15:00 - 15:20
PPS
Discussion 7
15:20 - 15:30
PPS
Insomnia: Types and Modules for Probabilistic Programming
15:30 - 16:30
Finite-depth Higher-order Abstract Syntax Trees for Reasoning about Pro ...
15:30 - 16:30
Coalgebraic Trace Semantics for Probabilistic Processes: Preliminary Pr ...
15:30 - 16:30
Reasoning about Probability and Nondeterminism
15:30 - 16:30
Fixed Points for Markov Decision Processes
15:30 - 16:30
A Denotational Semantics of a Probabilistic Stream-Processing Language
15:30 - 16:30
Observation Propagation for Importance Sampling with Likelihood Weighting
15:30 - 16:30
Problems of the Lightweight Implementation of Probabilistic Programming
15:30 - 16:30
Parameterized Probability Monad
15:30 - 16:30
Reproducing Kernel Hilbert Space Semantics for Probabilistic Programs
15:30 - 16:30
PPS
eXchangeable Random Primitives
16:30 - 16:50
PPS
Discussion 8
16:50 - 17:00
PPS
An Application of Computable Distributions to the Semantics of Probabil ...
17:00 - 17:20
PPS
Discussion 9
17:20 - 17:30
PPS
On The Semantic Intricacies of Conditioning
17:30 - 17:50
PPS
Discussion 10
17:50 - 18:00
x
Fri 11 Oct 07:32