OPCT 2019
Sun 13 - Sat 19 January 2019
Cascais, Portugal
co-located with
POPL 2019
Toggle navigation
Attending
Venue: Hotel Cascais Miragem
Program
OPCT 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
OPCT 2019 Committees
Track Committees
Organizing Committee
Program Committee
Contributors
People Index
Search
Series
Sign in
Sign up
POPL 2019
(
series
) /
OPCT 2019 (
series
) /
Hotel Cascais Miragem
/
Room information: Sala XII
Venue
Hotel Cascais Miragem
Room name
Sala XII
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
Mon 14 Jan
Displayed time zone:
Belfast
change
09:00 - 10:30
Keynote 1 and Research Paper
CPP
at
Sala XII
Chair(s):
Magnus O. Myreen
Chalmers University of Technology, Sweden
09:00
60m
Talk
A Linear Logical Framework in Hybrid
CPP
Amy Felty
University of Ottawa
DOI
10:00
30m
Research paper
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
CPP
Yannick Forster
Saarland University
,
Dominique Larchey-Wendling
CNRS, LORIA
DOI
11:00 - 12:30
Research Papers: Proof Theory, Theory of Programming Languages
CPP
at
Sala XII
Chair(s):
Assia Mahboubi
INRIA
11:00
30m
Research paper
A Proof-Theoretic Approach to Certifying Skolemization
CPP
Kaustuv Chaudhuri
Inria, France
,
Matteo Manighetti
Inria & École Polytechnique
,
Dale Miller
INRIA Saclay and LIX
DOI
11:30
30m
Research paper
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
CPP
Yannick Forster
Saarland University
,
Steven Schäfer
Saarland University
,
Simon Spies
Saarland University
,
Kathrin Stark
Saarland University, Germany
DOI
12:00
30m
Research paper
Eliminating Reflection from Type Theory
CPP
Théo Winterhalter
Gallinette / Inria / LS2N
,
Nicolas Tabareau
Inria
,
Matthieu Sozeau
Inria
DOI
14:00 - 15:30
Research Papers: Program Verification
CPP
at
Sala XII
Chair(s):
Chris Hawblitzel
Microsoft Research
14:00
30m
Research paper
Formally Verified Big Step Semantics out of x86-64 Binaries
CPP
Ian Roessle
Virginia Tech, USA
,
Freek Verbeek
Open University of the Netherlands, The Netherlands
,
Binoy Ravindran
Virginia Tech
DOI
14:30
30m
Research paper
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
CPP
Sandrine Blazy
Univ Rennes- IRISA
,
Rémi Hutin
IRISA / ENS Rennes
DOI
15:00
30m
Research paper
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
CPP
Nicolas Koh
,
Yao Li
University of Pennsylvania
,
Yishuai Li
University of Pennsylvania
,
Li-yao Xia
University of Pennsylvania
,
Lennart Beringer
Princeton University
,
Wolf Honore
,
William Mansky
University of Illinois at Chicago
,
Benjamin C. Pierce
University of Pennsylvania
,
Steve Zdancewic
University of Pennsylvania
DOI
16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer Algebra
CPP
at
Sala XII
Chair(s):
Georges Gonthier
Inria
16:00
30m
Research paper
A Formal Proof of Hensel's Lemma over the p-adic Integers
CPP
Robert Y. Lewis
Vrije Universiteit Amsterdam
DOI
16:30
30m
Research paper
Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem
CPP
Wenda Li
University of Cambridge
,
Lawrence Paulson
University of Cambridge
DOI
17:00
30m
Research paper
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
CPP
Fabian Immler
,
Bohua Zhan
DOI
Tue 15 Jan
Displayed time zone:
Belfast
change
09:00 - 10:30
Keynote 2 and Research Paper
CPP
at
Sala XII
Chair(s):
Assia Mahboubi
INRIA
09:00
60m
Talk
Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL
CPP
Jasmin Blanchette
Vrije Universiteit Amsterdam
DOI
10:00
30m
Research paper
A Verified Prover Based on Ordered Resolution
CPP
Anders Schlichtkrull
Technical University of Denmark
,
Jasmin Blanchette
Vrije Universiteit Amsterdam
,
Dmitriy Traytel
ETH Zurich
DOI
11:00 - 12:30
Research Papers: Rewriting, Automated Reasoning
CPP
at
Sala XII
Chair(s):
Andrei Popescu
Middlesex University, London
11:00
30m
Research paper
Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
CPP
Kathrin Stark
Saarland University, Germany
,
Steven Schäfer
Saarland University
,
Jonas Kaiser
DOI
11:30
30m
Research paper
Certified ACKBO
CPP
Alexander Lochmann
,
Christian Sternagel
University of Innsbruck, Austria
DOI
12:00
30m
Research paper
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
CPP
Bertram Felgenhauer
,
Aart Middeldorp
,
Turaga Prathamesh
,
Franziska Rapp
DOI
14:00 - 15:30
Research Papers: Program Verification
CPP
at
Sala XII
Chair(s):
Nicolas Tabareau
Inria
14:00
30m
Research paper
A Verified Protocol Buffer Compiler
CPP
Qianchuan Ye
Purdue University
,
Benjamin Delaware
Purdue University
DOI
14:30
30m
Research paper
A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
CPP
Véronique Benzaken
LRI, Université Paris-Sud
,
Evelyne Contejean
DOI
15:00
30m
Research paper
Dynamic Class Initialization Semantics: a Jinja Extension
CPP
Susannah Mansky
,
Elsa Gunter
University of Illinois
DOI
16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer Algebra
CPP
at
Sala XII
Chair(s):
Zhong Shao
Yale University
16:00
30m
Research paper
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
CPP
Yannick Forster
Saarland University
,
Dominik Kirst
Saarland University
,
Gert Smolka
Saarland University
DOI
16:30
30m
Research paper
Verified Solving and Asymptotics of Linear Recurrences
CPP
Manuel Eberl
Technische Universität München
DOI
17:00
30m
Meeting
Business Meeting
CPP
Assia Mahboubi
INRIA
,
Magnus O. Myreen
Chalmers University of Technology, Sweden
Mon 14 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 XII
CPP
Keynote 1 and Research Paper
CPP
Research Papers: Proof Theory, Theory of Programming Languages
CPP
Research Papers: Program Verification
CPP
Research Papers: Formalization of Mathematics and Computer Algebra
Tue 15 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 XII
CPP
Keynote 2 and Research Paper
CPP
Research Papers: Rewriting, Automated Reasoning
CPP
Research Papers: Program Verification
CPP
Research Papers: Formalization of Mathematics and Computer Algebra
Mon 14 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 XII
CPP
A Linear Logical Framework in Hybrid
09:00 - 10:00
CPP
Certified Undecidability of Intuitionistic Linear Logic via Binary Stac ...
10:00 - 10:30
CPP
A Proof-Theoretic Approach to Certifying Skolemization
11:00 - 11:30
CPP
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
11:30 - 12:00
CPP
Eliminating Reflection from Type Theory
12:00 - 12:30
CPP
Formally Verified Big Step Semantics out of x86-64 Binaries
14:00 - 14:30
CPP
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Ari ...
14:30 - 15:00
CPP
From C to Interaction Trees: Specifying, Verifying, and Testing a Netwo ...
15:00 - 15:30
CPP
A Formal Proof of Hensel's Lemma over the p-adic Integers
16:00 - 16:30
CPP
Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan- ...
16:30 - 17:00
CPP
Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
17:00 - 17:30
Tue 15 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 XII
CPP
Formalizing the Metatheory of Logical Calculi and Automatic Provers in ...
09:00 - 10:00
CPP
A Verified Prover Based on Ordered Resolution
10:00 - 10:30
CPP
Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Sub ...
11:00 - 11:30
CPP
Certified ACKBO
11:30 - 12:00
CPP
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite ...
12:00 - 12:30
CPP
A Verified Protocol Buffer Compiler
14:00 - 14:30
CPP
A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally ...
14:30 - 15:00
CPP
Dynamic Class Initialization Semantics: a Jinja Extension
15:00 - 15:30
CPP
On Synthetic Undecidability in Coq, with an Application to the Entschei ...
16:00 - 16:30
CPP
Verified Solving and Asymptotics of Linear Recurrences
16:30 - 17:00
CPP
Business Meeting
17:00 - 17:30
x
Sat 23 Nov 22:14