Sala I - POPL 2019

VenueHotel Cascais Miragem

Room nameSala I

Floor0

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT) Belfast.

Use conference time zone: (GMT) BelfastSelect 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

Wed 16 Jan
Displayed time zone: Belfast change

10:35 - 12:03	Reasoning about Probabilistic ProgramsResearch Papers at Sala I Chair(s): Jan Hoffmann Carnegie Mellon University

10:35 22m Talk		Formal Verification of Higher-Order Probabilistic Programs Research Papers Tetsuya Sato University at Buffalo, SUNY, USA, Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Justin Hsu University of Wisconsin-Madison, USA Link to publication DOI Media Attached File Attached
10:57 22m Talk		A Separation Logic for Concurrent Randomized Programs Research Papers Joseph Tassarotti Carnegie Mellon University, Robert Harper Link to publication DOI Media Attached File Attached
11:19 22m Talk		Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs Research Papers Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University Link to publication DOI Media Attached File Attached
11:41 22m Talk		Trace Abstraction Modulo Probability Research Papers Calvin Smith University of Wisconsin - Madison, Justin Hsu University of Wisconsin-Madison, USA, Aws Albarghouthi University of Wisconsin-Madison Link to publication DOI Media Attached

13:45 - 14:51	Probabilistic Programming and SemanticsResearch Papers at Sala I Chair(s): Justin Hsu University of Wisconsin-Madison, USA

13:45 22m Talk		Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic Research Papers Maria I. Gorinova The University of Edinburgh, Andrew D. Gordon Microsoft Research and University of Edinburgh, Charles Sutton University of Edinburgh Link to publication DOI Pre-print Media Attached File Attached
14:07 22m Talk		A Domain Theory for Statistical Probabilistic ProgrammingDistinguished Paper Research Papers Matthijs Vákár University of Oxford, Ohad Kammar University of Edinburgh, Sam Staton University of Oxford Link to publication DOI Pre-print Media Attached File Attached
14:29 22m Talk		Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling Research Papers Feras Saad Massachusetts Institute of Technology, Marco Cusumano-Towner MIT-CSAIL, Ulrich Schaechtle Massachusetts Institute of Technology, USA, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka MIT Link to publication DOI Media Attached File Attached

15:21 - 16:27	Machine Learning and Linear AlgebraResearch Papers at Sala I Chair(s): Aws Albarghouthi University of Wisconsin-Madison

15:21 22m Talk		code2vec: Learning Distributed Representations of Code Research Papers Uri Alon Technion, Meital Zilberstein Technion, Omer Levy University of Washington, USA, Eran Yahav Technion Link to publication DOI Pre-print Media Attached File Attached
15:43 22m Talk		An Abstract Domain for Certifying Neural Networks Research Papers Gagandeep Singh , Timon Gehr , Markus Püschel ETH Zürich, Martin Vechev ETH Zürich Link to publication DOI Media Attached
16:05 22m Talk		Closed Forms for Numerical Loops Research Papers Zachary Kincaid Princeton University, Jason Breck University of Wisconsin - Madison, John Cyphert University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. Link to publication DOI Media Attached File Attached

16:37 - 17:43	Quantum ProgrammingResearch Papers at Sala I Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)

16:37 22m Talk		Quantitative Robustness Analysis of Quantum Programs Research Papers Shih-Han Hung University of Maryland, Kesha Hietala University of Maryland, Shaopeng Zhu University of Maryland, Mingsheng Ying University of Technology Sydney, Michael Hicks University of Maryland, College Park, Xiaodi Wu University of Oregon, USA Link to publication DOI Media Attached
16:59 22m Talk		Game Semantics for Quantum Programming Research Papers Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS Lyon, Glynn Winskel Link to publication DOI Media Attached
17:21 22m Talk		Quantum Relational Hoare Logic Research Papers Dominique Unruh University of Tartu Link to publication DOI Pre-print Media Attached File Attached

18:00 - 18:30	Wednesday Evening Program IResearch Papers at Sala I

18:00 30m Talk		Microsoft Research: Engage, Verify, Open Research Papers Thomas Ball Microsoft Research Media Attached

Thu 17 Jan
Displayed time zone: Belfast change

09:00 - 10:06	Type Abstraction and EffectsResearch Papers at Sala I Chair(s): Benjamin Delaware Purdue University

09:00 22m Talk		Abstraction-Safe Effect Handlers via Tunneling Research Papers Yizhou Zhang Cornell University, Andrew Myers Cornell University Link to publication DOI Media Attached
09:22 22m Talk		Abstracting Algebraic Effects Research Papers Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław Link to publication DOI Media Attached
09:44 22m Talk		Fully Abstract Module Compilation Research Papers Karl Crary Carnegie Mellon University Link to publication DOI Media Attached File Attached

10:36 - 12:04	Gradual TypesResearch Papers at Sala I Chair(s): Nikhil Swamy Microsoft Research

10:36 22m Talk		Type-Driven Gradual Security with ReferencesTOPLAS Research Papers Matías Toro University of Chile, Ronald Garcia University of British Columbia, Éric Tanter University of Chile & Inria Paris DOI Media Attached File Attached
10:58 22m Talk		Gradual Type Theory Research Papers Max S. New Northeastern University, Daniel R. Licata Wesleyan University, Amal Ahmed Northeastern University, USA Link to publication DOI Media Attached File Attached
11:20 22m Talk		Gradual Parametricity, RevisitedDistinguished Paper Research Papers Matías Toro University of Chile, Elizabeth Labrada University of Chile, Éric Tanter University of Chile & Inria Paris Link to publication DOI Pre-print Media Attached File Attached
11:42 22m Talk		Live Functional Programming with Typed Holes Research Papers Cyrus Omar University of Chicago, Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago, Matthew Hammer None Link to publication DOI Pre-print Media Attached File Attached

13:45 - 14:51	Type Inference IResearch Papers at Sala I Chair(s): Michael Hicks University of Maryland, College Park

13:45 22m Talk		Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types Research Papers Jana Dunfield Queen's University, Kingston, Ontario, Neel Krishnaswami Computer Laboratory, University of Cambridge Link to publication DOI Media Attached
14:07 22m Talk		Abstracting Extensible Data Types; Or, Rows By Any Other Name Research Papers J. Garrett Morris University of Kansas, USA, James McKinna Link to publication DOI Media Attached
14:29 22m Talk		Polymorphic Symmetric Multiple Dispatch with Variance Research Papers Gyunghee Park KAIST, Oracle Labs, Jaemin Hong KAIST, South Korea, Guy L. Steele Jr. Oracle Labs, Sukyoung Ryu KAIST, South Korea Link to publication DOI Media Attached File Attached

15:21 - 16:49	Type Inference IIResearch Papers at Sala I Chair(s): Niki Vazou IMDEA Software Institute

15:21 22m Talk		Dynamic Type Inference for Gradual Hindley–Milner Typing Research Papers Yusuke Miyazaki Kyoto University, Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan Link to publication DOI Pre-print Media Attached File Attached
15:43 22m Talk		Gradual Typing: A New Perspective Research Papers Giuseppe Castagna CNRS - Université Paris Diderot, France, Victor Lanvin IRIF, Université Paris Diderot, France, Tommaso Petrucciani DIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. Siek Indiana University, USA Link to publication DOI Media Attached File Attached
16:05 22m Talk		Intersection Types and Runtime Errors in the Pi-Calculus Research Papers Ugo Dal Lago University of Bologna, Italy / Inria, France, Marc De Visme ENS Lyon, Damiano Mazza CNRS, Akira Yoshimizu INRIA Link to publication DOI Media Attached File Attached
16:27 22m Talk		Principality and Approximation under Dimensional Bound Research Papers Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund Link to publication DOI Media Attached File Attached

Fri 18 Jan
Displayed time zone: Belfast change

10:35 - 12:03	Dependent TypesResearch Papers at Sala I Chair(s): Andreas Abel Gothenburg University

10:35 22m Talk		Higher Inductive Types in Cubical Computational Type Theory Research Papers Evan Cavallo Carnegie Mellon University, Robert Harper Link to publication DOI Pre-print Media Attached File Attached
10:57 22m Talk		Constructing Quotient Inductive-Inductive Types Research Papers Thorsten Altenkirch University of Nottingham, Ambrus Kaposi University of Nottingham, András Kovács Eötvös Loránd University Link to publication DOI Media Attached File Attached
11:19 22m Talk		Definitional Proof-Irrelevance without K Research Papers Gaetan Gilbert , Jesper Cockx Chalmers \| University of Gothenburg, Matthieu Sozeau Inria, Nicolas Tabareau Inria Link to publication DOI Media Attached File Attached
11:41 22m Talk		Bisimulation as Path Type for Guarded Recursive Types Research Papers Rasmus Ejlers Møgelberg IT University of Copenhagen, Niccolò Veltri IT University of Copenhagen Link to publication DOI Media Attached File Attached

13:45 - 14:51	SemanticsResearch Papers at Sala I Chair(s): Noam Zeilberger University of Birmingham, UK

13:45 22m Talk		Better Late Than Never: A Fully Abstract Semantics for Classical Processes Research Papers Wen Kokke University of Edinburgh, Fabrizio Montesi University of Southern Denmark, Marco Peressotti University of Southern Denmark Link to publication DOI Media Attached
14:07 22m Talk		Diagrammatic Algebra: From Linear to Concurrent Systems Research Papers Filippo Bonchi University of Pisa, Joshua Holland University of Southampton, Robin Piedeleu University of Oxford, Pawel Sobocinski University of Southampton, Fabio Zanasi University College London Link to publication DOI Media Attached
14:29 22m Talk		Fixpoint Games on Continuous Lattices Research Papers Paolo Baldan University of Padova, Barbara König University of Duisburg-Essen, Christina Mika-Michalski University of Duisburg-Essen, Tommaso Padoan University of Padova Link to publication DOI Media Attached File Attached

15:21 - 16:27	Security and Information FlowResearch Papers at Sala I Chair(s): David Walker Princeton University

15:21 22m Talk		LWeb: Information Flow Security for Multi-Tier Web Applications Research Papers James Parker University of Maryland, Niki Vazou IMDEA Software Institute, Michael Hicks University of Maryland, College Park Link to publication DOI Media Attached File Attached
15:43 22m Talk		From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper Research Papers Marco Vassena Chalmers University of Technology, Alejandro Russo Chalmers University of Technology, Sweden, Deepak Garg Max Planck Institute for Software Systems, Vineet Rajani MPI-SWS, Deian Stefan University of California San Diego Link to publication DOI Media Attached File Attached
16:05 22m Talk		Modalities, Cohesion, and Information Flow Research Papers Alex Kavvos Wesleyan University Link to publication DOI Pre-print File Attached

16:37 - 17:43	Verified Compilation and ConcurrencyResearch Papers at Sala I Chair(s): Michael Greenberg Pomona College

16:37 22m Talk		A Calculus for Esterel: If can, can. If no can, no can. Research Papers Spencer P. Florence Northwestern University, USA, Shu-Hung You Northwestern University, USA, Jesse A. Tov Northwestern University, Department of Electrical Engineering and Computer Science, Robert Bruce Findler Northwestern University, USA Link to publication DOI Media Attached File Attached
16:59 22m Talk		An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code Research Papers Yuting Wang Yale University, Pierre Wilke Yale University, Zhong Shao Yale University Link to publication DOI Media Attached File Attached
17:21 22m Talk		A Verified, Efficient Embedding of a Verifiable Assembly Language Research Papers Aymeric Fromherz Carnegie Mellon University, Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Bryan Parno , Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research Link to publication DOI Media Attached File Attached

Wed 16 Jan
Displayed time zone: Belfast change


Room	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
Sala I								Research Papers Reasoning about Probabilistic Programs																																						Research Papers Probabilistic Programming and Semantics																			Research Papers Machine Learning and Linear Algebra															Research Papers Quantum Programming																	Research Papers Wednesday Evening Program I

Thu 17 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
Sala I	Research Papers Type Abstraction and Effects																			Research Papers Gradual Types																																						Research Papers Type Inference I																			Research Papers Type Inference II

Fri 18 Jan
Displayed time zone: Belfast change


Room	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 I								Research Papers Dependent Types																																						Research Papers Semantics																			Research Papers Security and Information Flow															Research Papers Verified Compilation and Concurrency

Wed 16 Jan
Displayed time zone: Belfast change


Room	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
Sala I								POPL Research Papers Formal Verification of Higher-Order Probabilistic Programs 10:35 - 10:57				POPL Research Papers A Separation Logic for Concurrent Randomized Programs 10:57 - 11:19					POPL Research Papers Quantitative Separation Logic - A Logic for Reasoning about Probabilist ... 11:19 - 11:41				POPL Research Papers Trace Abstraction Modulo Probability 11:41 - 12:03																									POPL Research Papers Probabilistic Programming with Densities in SlicStan: Efficient, Flexib ... 13:45 - 14:07				POPL Research PapersDistinguished Paper A Domain Theory for Statistical Probabilistic Programming 14:07 - 14:29					POPL Research Papers Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling 14:29 - 14:51										POPL Research Papers code2vec: Learning Distributed Representations of Code 15:21 - 15:43					POPL Research Papers An Abstract Domain for Certifying Neural Networks 15:43 - 16:05				POPL Research Papers Closed Forms for Numerical Loops 16:05 - 16:27						POPL Research Papers Quantitative Robustness Analysis of Quantum Programs 16:37 - 16:59					POPL Research Papers Game Semantics for Quantum Programming 16:59 - 17:21				POPL Research Papers Quantum Relational Hoare Logic 17:21 - 17:43								POPL Research Papers Microsoft Research: Engage, Verify, Open 18:00 - 18:30

Thu 17 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
Sala I	POPL Research Papers Abstraction-Safe Effect Handlers via Tunneling 09:00 - 09:22				POPL Research Papers Abstracting Algebraic Effects 09:22 - 09:44					POPL Research Papers Fully Abstract Module Compilation 09:44 - 10:06										POPL Research PapersTOPLAS Type-Driven Gradual Security with References 10:36 - 10:58					POPL Research Papers Gradual Type Theory 10:58 - 11:20				POPL Research PapersDistinguished Paper Gradual Parametricity, Revisited 11:20 - 11:42				POPL Research Papers Live Functional Programming with Typed Holes 11:42 - 12:04																									POPL Research Papers Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorph ... 13:45 - 14:07				POPL Research Papers Abstracting Extensible Data Types; Or, Rows By Any Other Name 14:07 - 14:29					POPL Research Papers Polymorphic Symmetric Multiple Dispatch with Variance 14:29 - 14:51										POPL Research Papers Dynamic Type Inference for Gradual Hindley–Milner Typing 15:21 - 15:43					POPL Research Papers Gradual Typing: A New Perspective 15:43 - 16:05				POPL Research Papers Intersection Types and Runtime Errors in the Pi-Calculus 16:05 - 16:27				POPL Research Papers Principality and Approximation under Dimensional Bound 16:27 - 16:49

Fri 18 Jan
Displayed time zone: Belfast change


Room	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 I								POPL Research Papers Higher Inductive Types in Cubical Computational Type Theory 10:35 - 10:57				POPL Research Papers Constructing Quotient Inductive-Inductive Types 10:57 - 11:19					POPL Research Papers Definitional Proof-Irrelevance without K 11:19 - 11:41				POPL Research Papers Bisimulation as Path Type for Guarded Recursive Types 11:41 - 12:03																									POPL Research Papers Better Late Than Never: A Fully Abstract Semantics for Classical Processes 13:45 - 14:07				POPL Research Papers Diagrammatic Algebra: From Linear to Concurrent Systems 14:07 - 14:29					POPL Research Papers Fixpoint Games on Continuous Lattices 14:29 - 14:51										POPL Research Papers LWeb: Information Flow Security for Multi-Tier Web Applications 15:21 - 15:43					POPL Research PapersDistinguished Paper From Fine- to Coarse-Grained Dynamic Information Flow Control and Back 15:43 - 16:05				POPL Research Papers Modalities, Cohesion, and Information Flow 16:05 - 16:27						POPL Research Papers A Calculus for Esterel: If can, can. If no can, no can. 16:37 - 16:59					POPL Research Papers An Abstract Stack Based Approach to Verified Compositional Compilation ... 16:59 - 17:21				POPL Research Papers A Verified, Efficient Embedding of a Verifiable Assembly Language 17:21 - 17:43

Room information: Sala I

Wed 16 Jan
Displayed time zone: Belfast change

Thu 17 Jan
Displayed time zone: Belfast change

Fri 18 Jan
Displayed time zone: Belfast change

Wed 16 Jan
Displayed time zone: Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Thu 17 Jan
Displayed time zone: Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Fri 18 Jan
Displayed time zone: Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Wed 16 Jan
Displayed time zone: Belfast change

Thu 17 Jan
Displayed time zone: Belfast change

Fri 18 Jan
Displayed time zone: Belfast change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: Sala I

Program Display Configuration

Wed 16 JanDisplayed time zone: Belfast change

Thu 17 JanDisplayed time zone: Belfast change

Fri 18 JanDisplayed time zone: Belfast change

Wed 16 JanDisplayed time zone: Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Thu 17 JanDisplayed time zone: Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Fri 18 JanDisplayed time zone: Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Wed 16 JanDisplayed time zone: Belfast change

Thu 17 JanDisplayed time zone: Belfast change

Fri 18 JanDisplayed time zone: Belfast change

Wed 16 Jan
Displayed time zone: Belfast change

Thu 17 Jan
Displayed time zone: Belfast change

Fri 18 Jan
Displayed time zone: Belfast change

Wed 16 Jan
Displayed time zone: Belfast change

Thu 17 Jan
Displayed time zone: Belfast change

Fri 18 Jan
Displayed time zone: Belfast change

Wed 16 Jan
Displayed time zone: Belfast change

Thu 17 Jan
Displayed time zone: Belfast change

Fri 18 Jan
Displayed time zone: Belfast change