BEAT 2019
Sun 13 - Sat 19 January 2019
Cascais, Portugal
co-located with
POPL 2019
Toggle navigation
Attending
Venue: Hotel Cascais Miragem
Program
BEAT Program
Your Program
Filter by Day
Sun 13 Jan
Mon 14 Jan
Tue 15 Jan
Wed 16 Jan
Thu 17 Jan
Fri 18 Jan
Sat 19 Jan
Track/Call
Organization
BEAT 2019 Committees
Track Committees
Organizing Committee
Program Committee
Contributors
People Index
Search
Series
Sign in
Sign up
POPL 2019
(
series
) /
BEAT 2019 (
series
) /
Hotel Cascais Miragem
/
Room information: Sala VI
Venue
Hotel Cascais Miragem
Room name
Sala VI
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) Belfast
.
Use conference time zone: (GMT) Belfast
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 19 Jan
Displayed time zone:
Belfast
change
09:00 - 10:30
Keynote & Contributed Talks 1
CoqPL
at
Sala VI
Chair(s):
Ilya Sergey
Yale-NUS College and National University of Singapore
09:00
5m
Day opening
Opening
CoqPL
09:05
60m
Talk
Coq User Interfaces: Past, Present, and Future (Keynote)
CoqPL
Emilio Jesús Gallego Arias
INRIA
10:05
25m
Talk
Counterexamples for Coq Conjectures
CoqPL
Samuel Gruetter
Massachusetts Institute of Technology
File Attached
11:15 - 12:30
Contributed Talks 2
CoqPL
at
Sala VI
Chair(s):
Enrico Tassi
INRIA
11:15
25m
Talk
Towards Mechanising Probabilistic Properties of a Blockchain
CoqPL
Kiran Gopinathan
University College London
,
Ilya Sergey
Yale-NUS College and National University of Singapore
File Attached
11:40
25m
Talk
Verifying Finality for Blockchain Systems
CoqPL
Karl Palmskog
University of Texas at Austin
,
Milos Gligoric
University of Texas at Austin
,
Lucas Peña
University of Illinois at Urbana-Champaign
,
Grigore Roşu
University of Illinois at Urbana-Champaign
File Attached
12:05
25m
Talk
WIP: Formalizing the Concordium Consensus Protocol in Coq
CoqPL
Thomas Dinsdale-Young
,
Bas Spitters
Aarhus University
,
Søren Eller Thomsen
Aarhus University
,
Daniel Tschudi
Aarhus University
File Attached
14:00 - 15:30
Contributed Talks 3 & Coq Developers
CoqPL
at
Sala VI
Chair(s):
Qinxiang Cao
Shanghai Jiao Tong University
14:00
25m
Talk
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
CoqPL
Vadim Zaliva
Carnegie Mellon University, USA
,
Matthieu Sozeau
Inria
File Attached
14:25
25m
Talk
Reifying and Translating a Monadic Fragment of Gallina
CoqPL
Paolo Torrini
File Attached
14:50
40m
Demonstration
Session with the Coq Development Team
CoqPL
Maxime Dénès
INRIA
,
Matthieu Sozeau
Inria
16:00 - 17:40
Contributed Talks 4
CoqPL
at
Sala VI
Chair(s):
Robbert Krebbers
Delft University of Technology
16:00
25m
Talk
Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs
CoqPL
Qinxiang Cao
Shanghai Jiao Tong University
File Attached
16:25
25m
Talk
Teaching Discrete Mathematics to Early Undergraduates with Software Foundations
CoqPL
Michael Greenberg
Pomona College
,
Joseph C. Osborn
Pomona College
File Attached
16:50
25m
Talk
Ltac2: Tactical Warfare
CoqPL
Pierre-Marie Pédrot
File Attached
17:15
25m
Talk
Towards a Coq Formalisation of Build Systems
CoqPL
Georgy Lukyanov
Newcastle University, UK
,
Andrey Mokhov
Newcastle University, UK
File Attached
Sat 19 Jan
Displayed time zone:
Belfast
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
Sala VI
CoqPL
Keynote & Contributed Talks 1
CoqPL
Contributed Talks 2
CoqPL
Contributed Talks 3 & Coq Developers
CoqPL
Contributed Talks 4
Sat 19 Jan
Displayed time zone:
Belfast
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
Sala VI
CoqPL
Opening
09:00 - 09:05
CoqPL
Coq User Interfaces: Past, Present, and Future (Keynote)
09:05 - 10:05
CoqPL
Counterexamples for Coq Conjectures
10:05 - 10:30
CoqPL
Towards Mechanising Probabilistic Properties of a Blockchain
11:15 - 11:40
CoqPL
Verifying Finality for Blockchain Systems
11:40 - 12:05
CoqPL
WIP: Formalizing the Concordium Consensus Protocol in Coq
12:05 - 12:30
CoqPL
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
14:00 - 14:25
CoqPL
Reifying and Translating a Monadic Fragment of Gallina
14:25 - 14:50
CoqPL
Session with the Coq Development Team
14:50 - 15:30
CoqPL
Deep Embedded Hoare Logic for Building Machine-Checkable Foundational P ...
16:00 - 16:25
CoqPL
Teaching Discrete Mathematics to Early Undergraduates with Software Fou ...
16:25 - 16:50
CoqPL
Ltac2: Tactical Warfare
16:50 - 17:15
CoqPL
Towards a Coq Formalisation of Build Systems
17:15 - 17:40
x
Thu 21 Nov 16:11