PriSC 2018
Mon 8 - Sat 13 January 2018
Los Angeles, California, United States
co-located with
POPL 2018
Toggle navigation
Attending
Venue: Omni Hotel
Program
Complete Program
Your Program
Mon 8 Jan
Tue 9 Jan
Wed 10 Jan
Thu 11 Jan
Fri 12 Jan
Sat 13 Jan
Track/Call
Organization
PriSC 2018 Committees
Track Committees
Program Committee
Organizing Committee
Contributors
People Index
Search
Series
Series
PriSC 2024
PriSC 2023
PriSC 2022
PriSC 2021
PriSC 2020
PriSC 2019
PriSC 2018
Sign in
Sign up
POPL 2018
(
series
) /
PriSC 2018 (
series
) /
Omni Hotel
/
Room information: Watercourt A
Venue
Omni Hotel
Room name
Watercourt A
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-08:00) Tijuana, Baja California
.
Use conference time zone: (GMT-08:00) Tijuana, Baja California
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
Sat 13 Jan
Displayed time zone:
Tijuana, Baja California
change
09:00 - 10:00
Keynote
CoqPL
at
Watercourt A
Chair(s):
Yves Bertot
INRIA
09:00
60m
Talk
CoqHammer: Strong Automation for Program Verification
CoqPL
Lukasz Czajka
University of Innsbruck
,
Cezary Kaliszyk
University of Innsbruck
File Attached
10:30 - 12:10
Tactics and Proof Engineering
CoqPL
at
Watercourt A
Chair(s):
Benjamin Delaware
Purdue University
10:30
25m
Talk
A “destruct” Tactic for Mtac2
CoqPL
Jan-Oliver Kaiser
MPI-SWS
,
Beta Ziliani
FAMAF, UNC and CONICET
File Attached
10:55
25m
Talk
Typed Template Coq
CoqPL
Simon Boulier
,
Matthieu Sozeau
Inria
,
Nicolas Tabareau
Inria, France
,
Abhishek Anand
Cornell University
File Attached
11:20
25m
Talk
Elpi: an extension language for Coq
CoqPL
Enrico Tassi
INRIA
File Attached
11:45
25m
Talk
Coqatoo: Generating Natural Language Versions of Coq Proofs
CoqPL
Andrew Bedford
Laval University
File Attached
14:00 - 14:50
PL Metatheory
CoqPL
at
Watercourt A
Chair(s):
Steve Zdancewic
University of Pennsylvania
14:00
25m
Talk
Locally Nameless at Scale
CoqPL
Stephanie Weirich
University of Pennsylvania, USA
,
Antoine Voizard
University of Pennsylvannia
,
Anastasiya Kravchuk-Kirilyuk
University of Pennsylvania
File Attached
14:25
25m
Talk
A Coq Formalisation of a Core of R
CoqPL
Martin Bodin
CMM
File Attached
14:50 - 15:30
Coq developers talk & panel
CoqPL
at
Watercourt A
14:50
40m
Talk
Session with the Coq Development Team
CoqPL
Matthieu Sozeau
Inria
,
Maxime Dénès
INRIA
,
Yves Bertot
INRIA
File Attached
16:00 - 18:05
Semantics and Synthesis
CoqPL
at
Watercourt A
Chair(s):
Ilya Sergey
University College London
16:00
25m
Talk
Phantom Types for Quantum Programs
CoqPL
Robert Rand
University of Pennsylvania
,
Jennifer Paykin
University of Pennsylvania
,
Steve Zdancewic
University of Pennsylvania
File Attached
16:25
25m
Talk
Revisiting Parametricity: Inductives and Uniformity of Propositions
CoqPL
Abhishek Anand
Cornell University
,
Greg Morrisett
Cornell University
File Attached
16:50
25m
Talk
Towards Context-Aware Data Refinement
CoqPL
Paul Krogmeier
Purdue University
,
Steven Kidd
Purdue University
,
Benjamin Delaware
Purdue University
File Attached
17:15
25m
Talk
Mechanizing the Construction and Rewriting of Proper Functions in Coq
CoqPL
Edwin Westbrook
Galois, Inc.
File Attached
17:40
25m
Talk
A calculus for logical refinements in separation logic
CoqPL
Dan Frumin
Radboud University
,
Robbert Krebbers
Delft University of Technology
File Attached
Sat 13 Jan
Displayed time zone:
Tijuana, Baja California
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
Watercourt A
CoqPL
Keynote
CoqPL
Tactics and Proof Engineering
CoqPL
PL Metatheory
CoqPL
Coq developers talk & panel
CoqPL
Semantics and Synthesis
Sat 13 Jan
Displayed time zone:
Tijuana, Baja California
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
Watercourt A
CoqPL
CoqHammer: Strong Automation for Program Verification
09:00 - 10:00
CoqPL
A “destruct” Tactic for Mtac2
10:30 - 10:55
CoqPL
Typed Template Coq
10:55 - 11:20
CoqPL
Elpi: an extension language for Coq
11:20 - 11:45
CoqPL
Coqatoo: Generating Natural Language Versions of Coq Proofs
11:45 - 12:10
CoqPL
Locally Nameless at Scale
14:00 - 14:25
CoqPL
A Coq Formalisation of a Core of R
14:25 - 14:50
CoqPL
Session with the Coq Development Team
14:50 - 15:30
CoqPL
Phantom Types for Quantum Programs
16:00 - 16:25
CoqPL
Revisiting Parametricity: Inductives and Uniformity of Propositions
16:25 - 16:50
CoqPL
Towards Context-Aware Data Refinement
16:50 - 17:15
CoqPL
Mechanizing the Construction and Rewriting of Proper Functions in Coq
17:15 - 17:40
CoqPL
A calculus for logical refinements in separation logic
17:40 - 18:05
x
Sun 28 Apr 23:01