PADL
Mon 18 - Tue 19 January 2016
St. Petersburg, Florida, United States
co-located with
POPL 2016
Toggle navigation
Attending
Venue: Hilton St. Petersburg Bayfront
Program
PADL Program
Your Program
Mon 18 Jan
Tue 19 Jan
Track/Call
Organization
PADL Committees
Organizers
Track Committees
Program Committee
Contributors
People Index
Search
Series
Series
PADL 2025
PADL 2024
PADL 2023
PADL 2022
PADL 2021
PADL 2020
PADL 2019
PADL 2018
PADL 2017
PADL
Sign in
Sign up
POPL 2016
(
series
) /
PADL
(
series
) /
Hilton St. Petersburg Bayfront
/
Room information: Room St Petersburg III
Venue
Hilton St. Petersburg Bayfront
Room name
Room St Petersburg III
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
Tue 19 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
08:50 - 09:00
Welcome Session
PLMW
at
Room St Petersburg III
09:00 - 10:00
Session I
PLMW
at
Room St Petersburg III
09:00
30m
Talk
Grad School: A Survival Guide
PLMW
Matthew Might
University of Utah, USA
Media Attached
09:30
30m
Talk
Theorem Provers are a PL Researcher's Best Friend
PLMW
Xavier Leroy
Inria
Media Attached
10:30 - 12:00
Session II
PLMW
at
Room St Petersburg III
10:30
30m
Talk
Academia or Industry?
PLMW
Aarti Gupta
Princeton University
Media Attached
11:00
30m
Talk
Refining Types with SMT
PLMW
Ranjit Jhala
University of California, San Diego
Media Attached
11:30
30m
Talk
How to Write Papers So People Can Read Them
PLMW
Derek Dreyer
MPI-SWS
Media Attached
14:00 - 15:30
Session III
PLMW
at
Room St Petersburg III
14:00
30m
Talk
Student Interaction Activity
PLMW
Işıl Dillig
University of Texas, Austin
,
Ross Tate
Cornell University
14:30
30m
Talk
Automata and Coinduction
PLMW
Alexandra Silva
Radboud University Nijmegen
Media Attached
15:00
30m
Talk
Unaccustomed As I Am to Public Speaking
PLMW
John Hughes
Chalmers University of Technology
Media Attached
16:00 - 17:00
Session IV
PLMW
at
Room St Petersburg III
16:00
30m
Talk
Two Notions of Beauty in Programming
PLMW
Robert Harper
Carnegie Mellon University
Media Attached
16:30
30m
Talk
Highs and Lows of a Language Researcher
PLMW
Greg Morrisett
Cornell University
Media Attached
17:00 - 17:45
Session V
PLMW
at
Room St Petersburg III
17:00
45m
Talk
Young Researcher Panel Session, with panelists: Mark Batty (Kent), Mike Carbin (MIT), Lindsey Kuper (Intel), Ilya Sergey (UCL)
PLMW
Dimitrios Vytiniotis
Microsoft Research, Cambridge
Media Attached
Sat 23 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
09:00 - 10:00
Session I
CoqPL
at
Room St Petersburg III
09:00
60m
Talk
Coq 8.5 at work and the future of Coq
CoqPL
Matthieu Sozeau
Inria
10:30 - 12:05
Session II
CoqPL
at
Room St Petersburg III
10:30
25m
Talk
A Coq Library for Binary Logical Relations
CoqPL
Jérémie Koenig
Link to publication
10:55
25m
Talk
A Coinduction Proof Rule for Hoare Doubles
CoqPL
Christian J. Bell
MIT CSAIL
Link to publication
11:20
25m
Talk
Formalizing Simple Refinements in Coq
CoqPL
Nicolás Lehmann
,
Éric Tanter
University of Chile, Chile
Link to publication
11:45
20m
Talk
Company-Coq: Taking Proof General one step closer to a real IDE
CoqPL
Clément Pit-Claudel
MIT CSAIL
,
Pierre Courtieu
Link to publication
14:00 - 15:25
Session III
CoqPL
at
Room St Petersburg III
14:00
60m
Talk
A Tutorial on using the Paco Library for coinductive reasoning
CoqPL
Chung-Kil Hur
Seoul National University
15:00
25m
Talk
Certified Desugaring of Javascript Programs using Coq
CoqPL
Marek Materzok
University of Wroclaw
Link to publication
16:00 - 18:00
Session IV
CoqPL
at
Room St Petersburg III
16:00
25m
Talk
The Category-theoretic Solution of Recursive Ultra-metric Space Equations
CoqPL
Amin Timany
,
Bart Jacobs
iMinds - Distrinet, KU Leuven
Link to publication
16:25
25m
Talk
A Case for Tactics with (Limited) Side Effects
CoqPL
Benjamin Delaware
Pre-print
16:50
25m
Talk
Formal Verification of Stability Properties of Cyber-Physical Systems
CoqPL
Matthew Chan
,
Daniel Ricketts
University of California, San Diego
,
Sorin Lerner
University of California, San Diego
,
Gregory Malecha
UCSD
Link to publication
17:15
30m
Talk
The Science of Deep Specification
CoqPL
Andrew W. Appel
Princeton
17:45
15m
Talk
Discussion
CoqPL
Tue 19 Jan
Displayed time zone:
Guadalajara, Mexico City, Monterrey
change
Room
8:00
30
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 III
PLMW
Welcome Session
PLMW
Session I
PLMW
Session II
PLMW
Session III
PLMW
Session IV
PLMW
Session V
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 III
CoqPL
Session I
CoqPL
Session II
CoqPL
Session III
CoqPL
Session IV
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
17:00
15
30
45
Room St Petersburg III
PLMW
Grad School: A Survival Guide
09:00 - 09:30
PLMW
Theorem Provers are a PL Researcher's Best Friend
09:30 - 10:00
PLMW
Academia or Industry?
10:30 - 11:00
PLMW
Refining Types with SMT
11:00 - 11:30
PLMW
How to Write Papers So People Can Read Them
11:30 - 12:00
PLMW
Student Interaction Activity
14:00 - 14:30
PLMW
Automata and Coinduction
14:30 - 15:00
PLMW
Unaccustomed As I Am to Public Speaking
15:00 - 15:30
PLMW
Two Notions of Beauty in Programming
16:00 - 16:30
PLMW
Highs and Lows of a Language Researcher
16:30 - 17:00
PLMW
Young Researcher Panel Session, with panelists: Mark Batty (Kent), Mike ...
17:00 - 17:45
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 III
CoqPL
Coq 8.5 at work and the future of Coq
09:00 - 10:00
CoqPL
A Coq Library for Binary Logical Relations
10:30 - 10:55
CoqPL
A Coinduction Proof Rule for Hoare Doubles
10:55 - 11:20
CoqPL
Formalizing Simple Refinements in Coq
11:20 - 11:45
CoqPL
Company-Coq: Taking Proof General one step closer to a real IDE
11:45 - 12:05
CoqPL
A Tutorial on using the Paco Library for coinductive reasoning
14:00 - 15:00
CoqPL
Certified Desugaring of Javascript Programs using Coq
15:00 - 15:25
CoqPL
The Category-theoretic Solution of Recursive Ultra-metric Space Equations
16:00 - 16:25
CoqPL
A Case for Tactics with (Limited) Side Effects
16:25 - 16:50
CoqPL
Formal Verification of Stability Properties of Cyber-Physical Systems
16:50 - 17:15
CoqPL
The Science of Deep Specification
17:15 - 17:45
CoqPL
Discussion
17:45 - 18:00
x
Sat 21 Dec 19:23