Sala I - POPL 2019

Sun 13 - Sat 19 January 2019 Cascais, Portugal

VenueHotel Cascais Miragem

Room nameSala I

Floor0

Room number

Capacity0

Additional informationThere is no additional information of this room available.

Program

Wed 16 Jan

10:35 - 12:03: Research Papers - Reasoning about Probabilistic Programs at Sala I
Chair(s): Jan HoffmannCarnegie Mellon University

10:35 - 10:57
Talk

Formal Verification of Higher-Order Probabilistic Programs

Tetsuya SatoUniversity at Buffalo, SUNY, USA, Alejandro AguirreIMDEA Software Institute, Spain, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Justin HsuUniversity of Wisconsin-Madison, USA

Link to publication DOI File Attached

10:57 - 11:19
Talk

A Separation Logic for Concurrent Randomized Programs

Joseph TassarottiCarnegie Mellon University, Robert Harper

Link to publication DOI File Attached

11:19 - 11:41
Talk

Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs

Kevin BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaRWTH Aachen University, Thomas NollRWTH Aachen University

Link to publication DOI File Attached

11:41 - 12:03
Talk

Trace Abstraction Modulo Probability

Calvin SmithUniversity of Wisconsin - Madison, Justin HsuUniversity of Wisconsin-Madison, USA, Aws AlbarghouthiUniversity of Wisconsin-Madison

Link to publication DOI

13:45 - 14:51: Research Papers - Probabilistic Programming and Semantics at Sala I
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA

13:45 - 14:07
Talk

Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic

Maria I. GorinovaThe University of Edinburgh, Andrew D. GordonMicrosoft Research and University of Edinburgh, Charles SuttonUniversity of Edinburgh

Link to publication DOI Pre-print File Attached

14:07 - 14:29
Talk

A Domain Theory for Statistical Probabilistic ProgrammingDistinguished Paper

Matthijs VákárUniversity of Oxford, Ohad KammarUniversity of Edinburgh, Sam StatonUniversity of Oxford

Link to publication DOI Pre-print File Attached

14:29 - 14:51
Talk

Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling

Feras SaadMassachusetts Institute of Technology, Marco Cusumano-TownerMIT-CSAIL, Ulrich SchaechtleMassachusetts Institute of Technology, USA, Martin RinardMassachusetts Institute of Technology, Vikash MansingkhaMIT

Link to publication DOI File Attached

15:21 - 16:27: Research Papers - Machine Learning and Linear Algebra at Sala I
Chair(s): Aws AlbarghouthiUniversity of Wisconsin-Madison

15:21 - 15:43
Talk

code2vec: Learning Distributed Representations of Code

Uri AlonTechnion, Meital ZilbersteinTechnion, Omer LevyUniversity of Washington, USA, Eran YahavTechnion

Link to publication DOI Pre-print Media Attached File Attached

15:43 - 16:05
Talk

An Abstract Domain for Certifying Neural Networks

Gagandeep Singh, Timon Gehr, Markus PüschelETH Zürich, Martin VechevETH Zürich

Link to publication DOI

16:05 - 16:27
Talk

Closed Forms for Numerical Loops

Zachary KincaidPrinceton University, Jason BreckUniversity of Wisconsin - Madison, John CyphertUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.

Link to publication DOI File Attached

16:37 - 17:43: Research Papers - Quantum Programming at Sala I
Chair(s): Jens PalsbergUniversity of California, Los Angeles (UCLA)

16:37 - 16:59
Talk

Quantitative Robustness Analysis of Quantum Programs

Shih-Han HungUniversity of Maryland, Kesha HietalaUniversity of Maryland, Shaopeng ZhuUniversity of Maryland, Mingsheng YingUniversity of Technology Sydney, Michael HicksUniversity of Maryland, College Park, Xiaodi WuUniversity of Oregon, USA

Link to publication DOI

16:59 - 17:21
Talk

Game Semantics for Quantum Programming

Pierre ClairambaultCNRS & ENS Lyon, Marc De VismeENS Lyon, Glynn Winskel

Link to publication DOI

17:21 - 17:43
Talk

Quantum Relational Hoare Logic

Dominique UnruhUniversity of Tartu

Link to publication DOI Pre-print File Attached

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

18:00 - 18:30
Talk

Microsoft Research: Engage, Verify, Open

Thomas BallMicrosoft Research

Thu 17 Jan

09:00 - 10:06: Research Papers - Type Abstraction and Effects at Sala I
Chair(s): Benjamin DelawarePurdue University

09:00 - 09:22
Talk

Abstraction-Safe Effect Handlers via Tunneling

Yizhou ZhangCornell University, Andrew MyersCornell University

Link to publication DOI Media Attached

09:22 - 09:44
Talk

Abstracting Algebraic Effects

Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław

Link to publication DOI

09:44 - 10:06
Talk

Fully Abstract Module Compilation

Karl CraryCarnegie Mellon University

Link to publication DOI File Attached

10:36 - 12:04: Research Papers - Gradual Types at Sala I
Chair(s): Nikhil SwamyMicrosoft Research

10:36 - 10:58
Talk

Type-Driven Gradual Security with ReferencesTOPLAS

Matías ToroUniversity of Chile, Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile & Inria Paris

DOI File Attached

10:58 - 11:20
Talk

Gradual Type Theory

Max NewNortheastern University, Dan LicataWesleyan University, Amal AhmedNortheastern University, USA

Link to publication DOI File Attached

11:20 - 11:42
Talk

Gradual Parametricity, RevisitedDistinguished Paper

Matías ToroUniversity of Chile, Elizabeth LabradaUniversity of Chile, Éric TanterUniversity of Chile & Inria Paris

Link to publication DOI Pre-print File Attached

11:42 - 12:04
Talk

Live Functional Programming with Typed Holes

Cyrus OmarUniversity of Chicago, Ian VoyseyCarnegie Mellon University, Ravi ChughUniversity of Chicago, Matthew HammerNone

Link to publication DOI Pre-print File Attached

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

13:45 - 14:07
Talk

Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types

Joshua DunfieldQueen's University, Kingston, Ontario, Neelakantan R. KrishnaswamiComputer Laboratory, University of Cambridge

Link to publication DOI

14:07 - 14:29
Talk

Abstracting Extensible Data Types; Or, Rows By Any Other Name

J. Garrett MorrisUniversity of Kansas, USA, James McKinna

Link to publication DOI

14:29 - 14:51
Talk

Polymorphic Symmetric Multiple Dispatch with Variance

Gyunghee ParkKAIST, Oracle Labs, Jaemin HongKAIST, South Korea, Guy L. Steele Jr.Oracle Labs, Sukyoung RyuKAIST, South Korea

Link to publication DOI File Attached

15:21 - 16:49: Research Papers - Type Inference II at Sala I
Chair(s): Niki VazouIMDEA Software Institute

15:21 - 15:43
Talk

Dynamic Type Inference for Gradual Hindley–Milner Typing

Yusuke MiyazakiKyoto University, Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan

Link to publication DOI Pre-print Media Attached File Attached

15:43 - 16:05
Talk

Gradual Typing: A New Perspective

Giuseppe CastagnaCNRS - Université Paris Diderot, France, Victor LanvinIRIF, Université Paris Diderot, France, Tommaso PetruccianiDIBRIS, Università di Genova, Italy & IRIF, Université Paris Diderot, France, Jeremy G. SiekIndiana University, USA

Link to publication DOI File Attached

16:05 - 16:27
Talk

Intersection Types and Runtime Errors in the Pi-Calculus

Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Marc De VismeENS Lyon, Damiano MazzaCNRS, Akira YoshimizuINRIA

Link to publication DOI File Attached

16:27 - 16:49
Talk

Principality and Approximation under Dimensional Bound

Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund

Link to publication DOI File Attached

Fri 18 Jan

10:35 - 12:03: Research Papers - Dependent Types at Sala I
Chair(s): Andreas AbelGothenburg University

10:35 - 10:57
Talk

Higher Inductive Types in Cubical Computational Type Theory

Evan CavalloCarnegie Mellon University, Robert Harper

Link to publication DOI Pre-print File Attached

10:57 - 11:19
Talk

Constructing Quotient Inductive-Inductive Types

Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham, András KovácsEötvös Loránd University

Link to publication DOI File Attached

11:19 - 11:41
Talk

Definitional Proof-Irrelevance without K

Gaetan Gilbert, Jesper CockxChalmers | University of Gothenburg, Matthieu SozeauInria, Nicolas TabareauInria

Link to publication DOI File Attached

11:41 - 12:03
Talk

Bisimulation as Path Type for Guarded Recursive Types

Rasmus Ejlers MøgelbergIT University of Copenhagen, Niccolò VeltriIT University of Copenhagen

Link to publication DOI File Attached

13:45 - 14:51: Research Papers - Semantics at Sala I
Chair(s): Noam ZeilbergerUniversity of Birmingham, UK

13:45 - 14:07
Talk

Better Late Than Never: A Fully Abstract Semantics for Classical Processes

Wen KokkeUniversity of Edinburgh, Fabrizio MontesiUniversity of Southern Denmark, Marco PeressottiUniversity of Southern Denmark

Link to publication DOI Media Attached

14:07 - 14:29
Talk

Diagrammatic Algebra: From Linear to Concurrent Systems

Filippo BonchiUniversity of Pisa, Joshua HollandUniversity of Southampton, Robin PiedeleuUniversity of Oxford, Pawel SobocinskiUniversity of Southampton, Fabio ZanasiUniversity College London

Link to publication DOI

14:29 - 14:51
Talk

Fixpoint Games on Continuous Lattices

Paolo BaldanUniversity of Padova, Barbara KönigUniversity of Duisburg-Essen, Christina Mika-MichalskiUniversity of Duisburg-Essen, Tommaso PadoanUniversity of Padova

Link to publication DOI File Attached

15:21 - 16:27: Research Papers - Security and Information Flow at Sala I
Chair(s): David WalkerPrinceton University

15:21 - 15:43
Talk

LWeb: Information Flow Security for Multi-Tier Web Applications

James ParkerUniversity of Maryland, Niki VazouIMDEA Software Institute, Michael HicksUniversity of Maryland, College Park

Link to publication DOI File Attached

15:43 - 16:05
Talk

From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper

Marco VassenaChalmers University of Technology, Alejandro RussoChalmers University of Technology, Sweden, Deepak GargMax Planck Institute for Software Systems, Vineet RajaniMPI-SWS, Deian StefanUniversity of California San Diego

Link to publication DOI File Attached

16:05 - 16:27
Talk

Modalities, Cohesion, and Information Flow

G. A. KavvosWesleyan University

Link to publication DOI Pre-print File Attached

16:37 - 17:43: Research Papers - Verified Compilation and Concurrency at Sala I
Chair(s): Michael GreenbergPomona College

16:37 - 16:59
Talk

A Calculus for Esterel: If can, can. If no can, no can.

Spencer P. FlorenceNorthwestern University, USA, Shu-Hung YouNorthwestern University, USA, Jesse A. TovNorthwestern University, Department of Electrical Engineering and Computer Science, Robby FindlerNorthwestern University, USA

Link to publication DOI File Attached

16:59 - 17:21
Talk

An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code

Yuting WangYale University, Pierre WilkeYale University, Zhong ShaoYale University

Link to publication DOI File Attached

17:21 - 17:43
Talk

A Verified, Efficient Embedding of a Verifiable Assembly Language

Aymeric FromherzCarnegie Mellon University, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research

Link to publication DOI File Attached

Wed 16 Jan 2019


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								POPL Research Papers Reasoning about Probabilistic Programs 10:35 - 12:03																																						POPL Research Papers Probabilistic Programming and Semantics 13:45 - 14:51																			POPL Research Papers Machine Learning and Linear Algebra 15:21 - 16:27															POPL Research Papers Quantum Programming 16:37 - 17:43																	POPL Research Papers Wednesday Evening Program I 18:00 - 18:30

Thu 17 Jan 2019


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	POPL Research Papers Type Abstraction and Effects 09:00 - 10:06																			POPL Research Papers Gradual Types 10:36 - 12:04																																						POPL Research Papers Type Inference I 13:45 - 14:51																			POPL Research Papers Type Inference II 15:21 - 16:49

Fri 18 Jan 2019


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								POPL Research Papers Dependent Types 10:35 - 12:03																																						POPL Research Papers Semantics 13:45 - 14:51																			POPL Research Papers Security and Information Flow 15:21 - 16:27															POPL Research Papers Verified Compilation and Concurrency 16:37 - 17:43

Wed 16 Jan 2019


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 2019


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 2019


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