Room St Petersburg II

VenueHilton St. Petersburg Bayfront

Room nameRoom St Petersburg II

Floor0

Room InformationNo extra information available

Program

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, MonterreySelect other time zone

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 programSpecify 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 FriedmanCPP 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 ProgramsCPP 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 ProversCPP 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: MathematicsCPP 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 MouraCPP 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: FoundationsCPP 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 SystemsCPP 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 VerificationCPP 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 1PPS 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 2PPS 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 3PPS 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 SessionPPS 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 5PPS 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

Room information: Room St Petersburg II

Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

CPP

CPP

CPP

CPP

Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

CPP

CPP

CPP

CPP

Sat 23 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

PPS

PPS

PPS

PPS

PPS

Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: Room St Petersburg II

Program Display Configuration

Mon 18 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

CPP

CPP

CPP

CPP

Tue 19 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

CPP

CPP

CPP

CPP

Sat 23 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

PPS

PPS

PPS

PPS

PPS

Mon 18 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change

Sat 23 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change