Sala I - POPL 2019

VenueHotel Cascais Miragem

Room nameSala I

Floor0

Additional informationThere is no additional information of this room available.

Program

Time Zone

The program is currently displayed in (GMT) Greenwich Mean Time : Belfast.

Use conference time zone: (GMT) Greenwich Mean Time : 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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

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

	10:35 - 10:57 Talk		Formal Verification of Higher-Order Probabilistic Programs Research Papers 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 Media Attached File Attached
	10:57 - 11:19 Talk		A Separation Logic for Concurrent Randomized Programs Research Papers Joseph TassarottiCarnegie Mellon University, Robert Harper Link to publication DOI Media Attached File Attached
	11:19 - 11:41 Talk		Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs Research Papers 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 Media Attached File Attached
	11:41 - 12:03 Talk		Trace Abstraction Modulo Probability Research Papers Calvin SmithUniversity of Wisconsin - Madison, Justin HsuUniversity of Wisconsin-Madison, USA, Aws AlbarghouthiUniversity of Wisconsin-Madison Link to publication DOI Media Attached

	13:45 - 14:51: Probabilistic Programming and SemanticsResearch Papers 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 Research Papers Maria I. GorinovaThe University of Edinburgh, Andrew D. GordonMicrosoft Research and University of Edinburgh, Charles SuttonUniversity of Edinburgh Link to publication DOI Pre-print Media Attached File Attached
	14:07 - 14:29 Talk		A Domain Theory for Statistical Probabilistic ProgrammingDistinguished Paper Research Papers Matthijs VákárUniversity of Oxford, Ohad KammarUniversity of Edinburgh, Sam StatonUniversity of Oxford Link to publication DOI Pre-print Media Attached File Attached
	14:29 - 14:51 Talk		Bayesian Synthesis of Probabilistic Programs for Automatic Data Modeling Research Papers Feras SaadMassachusetts Institute of Technology, Marco Cusumano-TownerMIT-CSAIL, Ulrich SchaechtleMassachusetts Institute of Technology, USA, Martin RinardMassachusetts Institute of Technology, Vikash MansinghkaMIT Link to publication DOI Media Attached File Attached

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

	15:21 - 15:43 Talk		code2vec: Learning Distributed Representations of Code Research Papers 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 Research Papers Gagandeep Singh, Timon Gehr, Markus PüschelETH Zürich, Martin VechevETH Zürich Link to publication DOI Media Attached
	16:05 - 16:27 Talk		Closed Forms for Numerical Loops Research Papers 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 Media Attached File Attached

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

	16:37 - 16:59 Talk		Quantitative Robustness Analysis of Quantum Programs Research Papers 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 Media Attached
	16:59 - 17:21 Talk		Game Semantics for Quantum Programming Research Papers Pierre ClairambaultCNRS & ENS Lyon, Marc De VismeENS Lyon, Glynn Winskel Link to publication DOI Media Attached
	17:21 - 17:43 Talk		Quantum Relational Hoare Logic Research Papers Dominique UnruhUniversity 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 - 18:30 Talk		Microsoft Research: Engage, Verify, Open Research Papers Thomas BallMicrosoft Research Media Attached

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

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

	09:00 - 09:22 Talk		Abstraction-Safe Effect Handlers via Tunneling Research Papers Yizhou ZhangCornell University, Andrew C. MyersCornell University Link to publication DOI Media Attached
	09:22 - 09:44 Talk		Abstracting Algebraic Effects Research Papers 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 Media Attached
	09:44 - 10:06 Talk		Fully Abstract Module Compilation Research Papers Karl CraryCarnegie Mellon University Link to publication DOI Media Attached File Attached

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

	10:36 - 10:58 Talk		Type-Driven Gradual Security with ReferencesTOPLAS Research Papers Matías ToroUniversity of Chile, Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile & Inria Paris DOI Media Attached File Attached
	10:58 - 11:20 Talk		Gradual Type Theory Research Papers Max NewNortheastern University, Dan LicataWesleyan University, Amal AhmedNortheastern University, USA Link to publication DOI Media Attached File Attached
	11:20 - 11:42 Talk		Gradual Parametricity, RevisitedDistinguished Paper Research Papers Matías ToroUniversity of Chile, Elizabeth LabradaUniversity of Chile, Éric TanterUniversity of Chile & Inria Paris Link to publication DOI Pre-print Media Attached File Attached
	11:42 - 12:04 Talk		Live Functional Programming with Typed Holes Research Papers Cyrus OmarUniversity of Chicago, Ian VoyseyCarnegie Mellon University, Ravi ChughUniversity of Chicago, Matthew HammerNone Link to publication DOI Pre-print Media Attached File Attached

	13:45 - 14:51: Type Inference IResearch Papers 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 Research Papers Jana DunfieldQueen's University, Kingston, Ontario, Neel KrishnaswamiComputer Laboratory, University of Cambridge Link to publication DOI Media Attached
	14:07 - 14:29 Talk		Abstracting Extensible Data Types; Or, Rows By Any Other Name Research Papers J. Garrett MorrisUniversity of Kansas, USA, James McKinna Link to publication DOI Media Attached
	14:29 - 14:51 Talk		Polymorphic Symmetric Multiple Dispatch with Variance Research Papers Gyunghee ParkKAIST, Oracle Labs, Jaemin HongKAIST, South Korea, Guy L. Steele Jr.Oracle Labs, Sukyoung RyuKAIST, South Korea Link to publication DOI Media Attached File Attached

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

	15:21 - 15:43 Talk		Dynamic Type Inference for Gradual Hindley–Milner Typing Research Papers 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 Research Papers 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 Media Attached File Attached
	16:05 - 16:27 Talk		Intersection Types and Runtime Errors in the Pi-Calculus Research Papers Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Marc De VismeENS Lyon, Damiano MazzaCNRS, Akira YoshimizuINRIA Link to publication DOI Media Attached File Attached
	16:27 - 16:49 Talk		Principality and Approximation under Dimensional Bound Research Papers Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund Link to publication DOI Media Attached File Attached

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

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

	10:35 - 10:57 Talk		Higher Inductive Types in Cubical Computational Type Theory Research Papers Evan CavalloCarnegie Mellon University, Robert Harper Link to publication DOI Pre-print Media Attached File Attached
	10:57 - 11:19 Talk		Constructing Quotient Inductive-Inductive Types Research Papers Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham, András KovácsEötvös Loránd University Link to publication DOI Media Attached File Attached
	11:19 - 11:41 Talk		Definitional Proof-Irrelevance without K Research Papers Gaetan Gilbert, Jesper CockxChalmers \| University of Gothenburg, Matthieu SozeauInria, Nicolas TabareauInria Link to publication DOI Media Attached File Attached
	11:41 - 12:03 Talk		Bisimulation as Path Type for Guarded Recursive Types Research Papers Rasmus Ejlers MøgelbergIT University of Copenhagen, Niccolò VeltriIT University of Copenhagen Link to publication DOI Media Attached File Attached

	13:45 - 14:51: SemanticsResearch Papers 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 Research Papers 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 Research Papers Filippo BonchiUniversity of Pisa, Joshua HollandUniversity of Southampton, Robin PiedeleuUniversity of Oxford, Pawel SobocinskiUniversity of Southampton, Fabio ZanasiUniversity College London Link to publication DOI Media Attached
	14:29 - 14:51 Talk		Fixpoint Games on Continuous Lattices Research Papers Paolo BaldanUniversity of Padova, Barbara KönigUniversity of Duisburg-Essen, Christina Mika-MichalskiUniversity of Duisburg-Essen, Tommaso PadoanUniversity 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 WalkerPrinceton University

	15:21 - 15:43 Talk		LWeb: Information Flow Security for Multi-Tier Web Applications Research Papers James ParkerUniversity of Maryland, Niki VazouIMDEA Software Institute, Michael HicksUniversity of Maryland, College Park Link to publication DOI Media Attached File Attached
	15:43 - 16:05 Talk		From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper Research Papers 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 Media Attached File Attached
	16:05 - 16:27 Talk		Modalities, Cohesion, and Information Flow Research Papers Alex KavvosWesleyan University Link to publication DOI Pre-print File Attached

	16:37 - 17:43: Verified Compilation and ConcurrencyResearch Papers 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. Research Papers 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 Media Attached File Attached
	16:59 - 17:21 Talk		An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code Research Papers Yuting WangYale University, Pierre WilkeYale University, Zhong ShaoYale University Link to publication DOI Media Attached File Attached
	17:21 - 17:43 Talk		A Verified, Efficient Embedding of a Verifiable Assembly Language Research Papers Aymeric FromherzCarnegie Mellon University, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research Link to publication DOI Media Attached File Attached

Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : 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
Times are displayed in time zone: Greenwich Mean Time : 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
Times are displayed in time zone: Greenwich Mean Time : 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
Times are displayed in time zone: Greenwich Mean Time : 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
Times are displayed in time zone: Greenwich Mean Time : 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
Times are displayed in time zone: Greenwich Mean Time : 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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposiums

Room information: Sala I

Program Display Configuration

Wed 16 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Thu 17 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Fri 18 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Wed 16 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Thu 17 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Fri 18 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Research Papers

Research Papers

Research Papers

Research Papers

Wed 16 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Thu 17 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Fri 18 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change

Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Thu 17 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

Fri 18 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change