VMCAI
Sun 17 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
VenueHilton St. Petersburg Bayfront
Room nameRoom St Petersburg II
Floor0
Room InformationNo extra information available
Program

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
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

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
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
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

Sat 23 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Room St Petersburg II

Sat 23 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Room St Petersburg II
PPS
Discussion 1
09:20 - 09:30
PPS
Discussion 2
09:50 - 10:00
PPS
DIscussion 3
10:50 - 11:00
PPS
Discussion 4
11:20 - 11:30
PPS
Discussion 5
14:20 - 14:30
PPS
Discussion 6
14:50 - 15:00
PPS
Discussion 7
15:20 - 15:30
PPS
Discussion 8
16:50 - 17:00
PPS
Discussion 9
17:20 - 17:30
PPS
Discussion 10
17:50 - 18:00