Salle 105, Barre 44-54

VenueParis Jussieu

Room nameSalle 105, Barre 44-54

Floor2

Room number105

Capacity80

Room Information

This room is located in barre 44-54.

Program

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect 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

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:50 - 10:00	First Morning SessionTTT at Salle 105, Barre 44-54 Chair(s): Assia Mahboubi INRIA

08:50 10m Day opening		Welcome TTT
09:00 20m Talk		A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method TTT David Thibodeau McGill University, Canada, Alberto Momigliano , Brigitte Pientka McGill University
09:20 20m Talk		Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT Steven Keuchel , Koar Marntirosian , Tom Schrijvers KU Leuven
09:40 20m Talk		Equivalence of System F and λ2 in Abella TTT Jonas Kaiser , Gert Smolka Saarland University

10:30 - 12:00	Second Morning SessionTTT at Salle 105, Barre 44-54 Chair(s): Keiko Nakata

10:30 50m Talk		Invited Talk -- Type Theory in the Software Analysis Workbench TTT Aaron Tomb Galois, Inc.
11:20 20m Talk		Modelling Program Behaviour within Software Verification Tool LAV TTT Milena Vujosevic Janicic
11:40 20m Talk		agdARGS - Declarative Hierarchical Command Line Interfaces TTT Guillaume Allais Radboud University Nijmegen

14:00 - 15:30	First Afternoon SessionTTT at Salle 105, Barre 44-54 Chair(s): Bas Spitters

14:00 50m Talk		Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders Mörtberg Inria
14:50 20m Talk		Equations: a tool for dependent pattern-matching TTT Cyprien Mangin , Matthieu Sozeau Inria File Attached
15:10 20m Talk		Coq's Prolog and application to defining semi-automatic tactics TTT Théo Zimmermann IRIF, Université Paris Diderot, Hugo Herbelin File Attached

16:00 - 18:00	Second Afternoon SessionTTT at Salle 105, Barre 44-54 Chair(s): Hugo Herbelin

16:00 50m Talk		Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq TTT Robbert Krebbers Delft University of Technology, Netherlands
16:50 20m Talk		Introducing MetaCoq: A Safe Tactic Language for Coq TTT Beta Ziliani FAMAF, UNC (Argentina) / CONICET (Argentina)
17:10 50m Other		COST EUTypes session TTT

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 12:00	Gradual Typing (AM)Tutorials at Salle 105, Barre 44-54

09:00 3h Talk		The State of the Art in Gradual Typing Tutorials Jeremy G. Siek Indiana University Bloomington

14:00 - 17:00	Gradual Typing (PM)Tutorials at Salle 105, Barre 44-54

14:00 3h Talk		The State of the Art in Gradual Typing Tutorials Jeremy G. Siek Indiana University Bloomington

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00	Session 1 PPS at Salle 105, Barre 44-54 Chair(s): Cameron Freer Gamalon and Borelian

09:00 60m Talk		Towards a metric semantics for probabilistic programming (invited talk) PPS Gordon Plotkin

10:30 - 12:00	Session 2 PPS at Salle 105, Barre 44-54 Chair(s): Chad Scherrer Galois, Inc.

10:30 20m Talk		An application of computable distributions to the semantics of probabilistic programs: part 2 PPS Daniel Huang Harvard University, Greg Morrisett Cornell University
10:50 10m Meeting		Discussion 1 PPS
11:00 20m Talk		Probabilistic programming and a domain theoretic approach to Skorohod's theorem PPS Michael Mislove Tulane
11:20 10m Meeting		Discussion 2 PPS
11:30 20m Talk		Building inference algorithms from monad transformers PPS Adam Ścibior University of Cambridge, Yufei Cai University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany, Zoubin Ghahramani University of Cambridge
11:50 10m Meeting		Discussion 3 PPS

14:00 - 15:30	Session 3 PPS at Salle 105, Barre 44-54 Chair(s): Sam Staton University of Oxford

14:00 20m Talk		Commutativity logic for probabilistic trace equivalence: complete or not? PPS Paul Blain Levy , Nathan Bowler Universität Hamburg
14:20 10m Meeting		Discussion 4 PPS
14:30 20m Talk		Mathematical structures of probabilistic programming PPS Ilias Garnier University of Edinburgh, Fredrik Dahlqvist University College London, Florence Clerc McGill University, Vincent Danos ENS Paris/CNRS
14:50 10m Meeting		Discussion 5 PPS
15:00 20m Talk		A weakest pre-expectation semantics for mixed-sign expectations PPS Benjamin Lucien Kaminski RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University
15:20 10m Meeting		Discussion 6 PPS

15:30 - 16:30	Poster Session PPS at Salle 105, Barre 44-54

15:30 60m Meeting		ProbLog and applicative probabilistic programming PPS Alexander Vandenbroucke KU Leuven, Belgium, Tom Schrijvers KU Leuven
15:30 60m Meeting		Encapsulating models and approximate inference programs in probabilistic modules PPS Marco Cusumano-Towner MIT-CSAIL, Vikash Mansinghka Massachusetts Institute of Technology
15:30 60m Meeting		The extended semantics for probabilistic programming languages PPS Siddharth Srivastava UTRC Berkeley, Nicholas Hay Vicarious, Yi WU UC Berkeley, Stuart Russell University of California, Berkeley
15:30 60m Meeting		Synthetic topology in homotopy type theory for probabilistic programming PPS Florian Faissole , Bas Spitters
15:30 60m Meeting		Reasoning about inference in probabilistic programs PPS Chandrakana Nandi University of Washington, USA, Adrian Sampson Cornell University, Dan Grossman University of Washington, Todd Mytkowicz , Kathryn S McKinley Microsoft Research
15:30 60m Meeting		On computable representations of exchangeable data PPS Nathanael L. Ackerman Harvard University, Jeremy Avigad Carnegie Mellon University, Cameron Freer Gamalon and Borelian, Daniel Roy , Jason M. Rute Pennsylvania State University
15:30 60m Meeting		Probabilistic logic programs: unifying program trace and possible world semantics PPS Angelika Kimmig KU Leuven, Luc De Raedt KU Leuven
15:30 60m Meeting		Metropolis-Hastings for mixtures of conditional distributions PPS Oleg Kiselyov
15:30 60m Meeting		Support and influence analysis for visualizing posteriors of probabilistic programs PPS Long Ouyang Stanford University
15:30 60m Meeting		Efficient exact inference in discrete Anglican programs PPS Robert Cornish University of Oxford, Frank Wood University of Oxford, Hongseok Yang University of Oxford

16:30 - 18:00	Session 5 PPS at Salle 105, Barre 44-54 Chair(s): Chung-chieh Shan Indiana University, USA

16:30 20m Talk		An exponential family basis for probabilistic programming PPS Chad Scherrer Galois, Inc.
16:50 10m Meeting		Discussion 7 PPS
17:00 20m Talk		The semantics of subroutines and iteration in the Bayesian programming language ProBT PPS Raphaël Laurent ProbaYes, Kamel Mekhnacha ProbaYes, Emmanuel Mazer CNRS/LIG, Pierre Bessière CNRS/ISIR
17:20 10m Meeting		Discussion 8 PPS
17:30 20m Talk		Exchangeable random process and data abstraction PPS Sam Staton University of Oxford, Hongseok Yang University of Oxford, Nathanael L. Ackerman Harvard University, Cameron Freer Gamalon and Borelian, Daniel Roy
17:50 10m Meeting		Discussion 9 PPS

18:15 - 19:15	Session 6 PPS at Salle 105, Barre 44-54 Chair(s): Hongseok Yang University of Oxford

18:15 20m Talk		Reducing probabilistic choice to nondeterministic choice PPS Ernie Cohen Amazon Web Services
18:35 10m Meeting		Discussion 10 PPS
18:45 20m Talk		GraPPa: spanning the expressivity vs. efficiency continuum PPS Edwin Westbrook Galois, Inc., Chad Scherrer Galois, Inc., Nathan Collins Galois, Inc., Eric Mertens Galois, Inc.
19:05 10m Meeting		Discussion 11 PPS

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

08:55 - 09:00	WelcomePiP at Salle 105, Barre 44-54

08:55 5m Talk		Welcome PiP

09:00 - 10:00	Session 1PiP at Salle 105, Barre 44-54

09:00 30m Talk		Andrew Kennedy (Facebook) Static type checking for PHP PiP
09:30 30m Talk		Jean-Louis Colaco (Ansys - Esterel Technologies) A brief history of the Scade language PiP

10:30 - 12:05	Session 2PiP at Salle 105, Barre 44-54

10:30 5m Talk		Peter Sewell (Cambridge) REMS Short Introduction PiP
10:35 30m Talk		Simon Moore (Cambridge) Experiences of Formal Modelling in the CHERI Computer Architecture Research Project PiP
11:05 30m Talk		Stephen Kell/Dominic Mulligan (Cambridge) ELF linking: what it means and why it matters PiP
11:35 30m Talk		Philippa Gardner (Imperial) An Infrastructure for Tractable Verification of JavaScript Programs PiP

14:00 - 15:30	Session 3PiP at Salle 105, Barre 44-54

14:00 30m Talk		John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten years of QuickCheck PiP
14:30 30m Talk		Byron Cook (Amazon) Automated Reasoning about AWS PiP
15:00 30m Talk		Steve Zdancewic (U.Penn) Vellvm2: Semantics and Verification for LLVM PiP

16:00 - 18:00	Session 4PiP at Salle 105, Barre 44-54

16:00 30m Talk		Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models PiP
16:30 60m Talk		Discussion: Methods and Tools for large-scale semantics PiP

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	8:00						30						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
Salle 105, Barre 44-54											TTT First Morning Session																				TTT Second Morning Session																																										TTT First Afternoon Session																								TTT Second Afternoon Session

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Salle 105, Barre 44-54	Tutorials Gradual Typing (AM)																																																												Tutorials Gradual Typing (PM)

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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						19:00						30
Salle 105, Barre 44-54	PPS Session 1																		PPS Session 2																																										PPS Session 3																		PPS Poster Session												PPS Session 5																					PPS Session 6

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	8:00						30						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
Salle 105, Barre 44-54												PiP Welcome	PiP Session 1																		PiP Session 2																																										PiP Session 3																								PiP Session 4

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	8:00			15			30			45			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
Salle 105, Barre 44-54											TTT Welcome 08:50 - 09:00		TTT A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method 09:00 - 09:20				TTT Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding 09:20 - 09:40				TTT Equivalence of System F and λ2 in Abella 09:40 - 10:00										TTT Invited Talk -- Type Theory in the Software Analysis Workbench 10:30 - 11:20										TTT Modelling Program Behaviour within Software Verification Tool LAV 11:20 - 11:40				TTT agdARGS - Declarative Hierarchical Command Line Interfaces 11:40 - 12:00																												TTT Invited Talk -- Cubical Type Theory: a constructive interpretation of t ... 14:00 - 14:50										TTT Equations: a tool for dependent pattern-matching 14:50 - 15:10				TTT Coq's Prolog and application to defining semi-automatic tactics 15:10 - 15:30										TTT Invited Talk -- Iris: a framework for higher-order concurrent separatio ... 16:00 - 16:50										TTT Introducing MetaCoq: A Safe Tactic Language for Coq 16:50 - 17:10				TTT COST EUTypes session 17:10 - 18:00

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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
Salle 105, Barre 44-54	POPL Tutorials The State of the Art in Gradual Typing 09:00 - 12:00																																																												POPL Tutorials The State of the Art in Gradual Typing 14:00 - 17:00

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna 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			19:00			15			30			45
Salle 105, Barre 44-54	PPS Towards a metric semantics for probabilistic programming (invited talk) 09:00 - 10:00																		PPS An application of computable distributions to the semantics of probabil ... 10:30 - 10:50				PPS Discussion 1 10:50 - 11:00		PPS Probabilistic programming and a domain theoretic approach to Skorohod's ... 11:00 - 11:20				PPS Discussion 2 11:20 - 11:30		PPS Building inference algorithms from monad transformers 11:30 - 11:50				PPS Discussion 3 11:50 - 12:00																										PPS Commutativity logic for probabilistic trace equivalence: complete or not? 14:00 - 14:20				PPS Discussion 4 14:20 - 14:30		PPS Mathematical structures of probabilistic programming 14:30 - 14:50				PPS Discussion 5 14:50 - 15:00		PPS A weakest pre-expectation semantics for mixed-sign expectations 15:00 - 15:20				PPS Discussion 6 15:20 - 15:30		PPS ProbLog and applicative probabilistic programming 15:30 - 16:30 Encapsulating models and approximate inference programs in probabilisti ... 15:30 - 16:30 The extended semantics for probabilistic programming languages 15:30 - 16:30 Synthetic topology in homotopy type theory for probabilistic programming 15:30 - 16:30 Reasoning about inference in probabilistic programs 15:30 - 16:30 On computable representations of exchangeable data 15:30 - 16:30 Probabilistic logic programs: unifying program trace and possible world ... 15:30 - 16:30 Metropolis-Hastings for mixtures of conditional distributions 15:30 - 16:30 Support and influence analysis for visualizing posteriors of probabilis ... 15:30 - 16:30 Efficient exact inference in discrete Anglican programs 15:30 - 16:30												PPS An exponential family basis for probabilistic programming 16:30 - 16:50				PPS Discussion 7 16:50 - 17:00		PPS The semantics of subroutines and iteration in the Bayesian programming ... 17:00 - 17:20				PPS Discussion 8 17:20 - 17:30		PPS Exchangeable random process and data abstraction 17:30 - 17:50				PPS Discussion 9 17:50 - 18:00					PPS Reducing probabilistic choice to nondeterministic choice 18:15 - 18:35				PPS Discussion 10 18:35 - 18:45		PPS GraPPa: spanning the expressivity vs. efficiency continuum 18:45 - 19:05				PPS Discussion 11 19:05 - 19:15

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	8:00			15			30			45			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
Salle 105, Barre 44-54												PiP Welcome 08:55 - 09:00	PiP Andrew Kennedy (Facebook) Static type checking for PHP 09:00 - 09:30						PiP Jean-Louis Colaco (Ansys - Esterel Technologies) A brief history of the ... 09:30 - 10:00												PiP Peter Sewell (Cambridge) REMS Short Introduction 10:30 - 10:35	PiP Simon Moore (Cambridge) Experiences of Formal Modelling in the CHERI Co ... 10:35 - 11:05						PiP Stephen Kell/Dominic Mulligan (Cambridge) ELF linking: what it means an ... 11:05 - 11:35						PiP Philippa Gardner (Imperial) An Infrastructure for Tractable Verificatio ... 11:35 - 12:05																													PiP John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten ... 14:00 - 14:30						PiP Byron Cook (Amazon) Automated Reasoning about AWS 14:30 - 15:00						PiP Steve Zdancewic (U.Penn) Vellvm2: Semantics and Verification for LLVM 15:00 - 15:30												PiP Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models 16:00 - 16:30						PiP Discussion: Methods and Tools for large-scale semantics 16:30 - 17:30

Room information: Salle 105, Barre 44-54

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

TTT

TTT

TTT

TTT

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tutorials

Tutorials

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

PPS

PPS

PPS

PPS

PPS

PPS

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

PiP

PiP

PiP

PiP

PiP

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: Salle 105, Barre 44-54

Program Display Configuration

Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

TTT

TTT

TTT

TTT

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tutorials

Tutorials

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

PPS

PPS

PPS

PPS

PPS

PPS

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

PiP

PiP

PiP

PiP

PiP

Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change