Ile de France II (IDF II)

VenueJW Marriott New Orleans

Room nameIle de France II (IDF II)

Floor3

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT-06:00) Saskatchewan, Central America.

Use conference time zone: (GMT-06:00) Saskatchewan, Central AmericaSelect 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 22 Jan
Displayed time zone: Saskatchewan, Central America change

08:45 - 09:00	Welcome + SIGPLAN Award CeremonyResearch Papers at Ile de France II (IDF II) Chair(s): Lars Birkedal Aarhus University, Jens Palsberg University of California, Los Angeles, Brigitte Pientka McGill University

08:45 15m Day opening		Welcome + SIGPLAN Award Ceremony Research Papers Media Attached

09:00 - 10:00	Invited TalkResearch Papers at Ile de France II (IDF II) Chair(s): Brigitte Pientka McGill University

09:00 60m Talk		Can Programming Languages Research impact Deep Learning 2.0?Invited Talk Research Papers Martin Vechev ETH Zürich Media Attached

10:30 - 11:35	Probabilistic ProgrammingResearch Papers at Ile de France II (IDF II) Chair(s): Alexandra Silva University College London

10:30 21m Talk		Towards Verified Stochastic Variational Inference for Probabilistic Programs Research Papers Wonyeol Lee KAIST, Hangyeol Yu KAIST, Xavier Rival INRIA/CNRS/ENS Paris, Hongseok Yang KAIST Link to publication DOI Media Attached
10:51 21m Talk		Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Research Papers Alexander K. Lew Massachusetts Institute of Technology, USA, Marco Cusumano-Towner MIT-CSAIL, Benjamin Sherman Massachusetts Institute of Technology, USA, Michael Carbin Massachusetts Institute of Technology, Vikash K. Mansinghka MIT Link to publication DOI Media Attached
11:13 21m Talk		Semantics of Higher-Order Probabilistic Programs with Conditioning Research Papers Fredrik Dahlqvist University College London, Dexter Kozen Cornell University Link to publication DOI Media Attached File Attached

11:45 - 12:30	Reasoning about Program Complexity/EfficiencyResearch Papers at Ile de France II (IDF II) Chair(s): Thomas Wies New York University

11:45 22m Talk		Recurrence Extraction for Functional Programs through Call-by-Push-Value Research Papers Alex Kavvos Aarhus University, Edward Morehouse Wesleyan University, Daniel R. Licata Wesleyan University, Norman Danner Wesleyan University Link to publication DOI File Attached
12:07 22m Talk		Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell Research Papers Martin Adam Thomas Handley University of Nottingham, Niki Vazou IMDEA Software Institute, Graham Hutton University of Nottingham, UK Link to publication DOI Media Attached File Attached

14:00 - 15:05	Program LogicsResearch Papers at Ile de France II (IDF II) Chair(s): Azalea Raad MPI-SWS, Germany

14:00 21m Talk		The Future is Ours: Prophecy Variables in Separation Logic Research Papers Ralf Jung MPI-SWS, Rodolphe Lepigre MPI-SWS, Gaurav Parthasarathy ETH Zurich, Marianna Rapoport University of Waterloo, Amin Timany imec-Distrinet KU-Leuven, Derek Dreyer MPI-SWS, Bart Jacobs imec-DistriNet, Dept. CS, KU Leuven Link to publication DOI Media Attached
14:21 21m Talk		Spy Game: Verifying a Local Generic Solver in Iris Research Papers Paulo Emílio de Vilhena Inria, François Pottier Inria, France, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud Link to publication DOI Media Attached File Attached
14:43 21m Talk		Actris: Session-Type Based Reasoning in Separation Logic Research Papers Jonas Kastberg Hinrichsen IT University of Copenhagen, Jesper Bengtson IT University of Copenhagen, Robbert Krebbers Delft University of Technology Link to publication DOI Media Attached File Attached

15:35 - 16:40	Automatic Differentiation / Kleene AlgebraResearch Papers at Ile de France II (IDF II) Chair(s): Lars Birkedal Aarhus University

15:35 21m Talk		A Simple Differentiable Programming Language Research Papers Gordon Plotkin Google, Martín Abadi Google Link to publication DOI Media Attached
15:56 21m Talk		Backpropagation in the Simply Typed Lambda-calculus with Linear Negation Research Papers Aloïs Brunel Deepomatic, Damiano Mazza CNRS, Michele Pagani IRIF - Université de Paris Link to publication DOI Media Attached File Attached
16:18 21m Talk		Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear TimeDistinguished Paper Research Papers Steffen Smolka Cornell University, Nate Foster Cornell University, Justin Hsu University of Wisconsin-Madison, USA, Tobias Kappé University College London, Dexter Kozen Cornell University, Alexandra Silva University College London Link to publication DOI Media Attached

16:50 - 17:35	Synthesis and Decision ProceduresResearch Papers at Ile de France II (IDF II) Chair(s): Roopsha Samanta Purdue University

16:50 22m Talk		Visualization by Example Research Papers Chenglong Wang University of Washington, USA, Yu Feng University of California, Santa Barbara, Rastislav Bodík University of Washington, Alvin Cheung University of California, Berkeley, Işıl Dillig University of Texas Austin Link to publication DOI Media Attached
17:12 22m Talk		Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Research Papers Umang Mathur University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign, Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign Link to publication DOI Pre-print Media Attached File Attached

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00	Invited TalkResearch Papers at Ile de France II (IDF II) Chair(s): Brigitte Pientka McGill University

09:00 60m Talk		What is a Secure Programming Language? Invited Talk Research Papers Cristina Cifuentes Oracle Labs Link to publication Media Attached

10:30 - 11:35	Types and EffectsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique Devriese Vrije Universiteit Brussel

10:30 21m Talk		Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers 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
10:51 21m Talk		The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Research Papers Pierre-Marie Pédrot INRIA, Nicolas Tabareau Inria Link to publication DOI Media Attached
11:13 21m Talk		SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References Research Papers Guilhem Jaber LS2N, Université de Nantes Link to publication DOI Media Attached

11:45 - 12:30	Dynamic Program AnalysisResearch Papers at Ile de France II (IDF II) Chair(s): Peter Thiemann University of Freiburg, Germany

11:45 22m Talk		Fast, Sound, and Effectively Complete Dynamic Race Prediction Research Papers Andreas Pavlogiannis Aarhus University Link to publication DOI Media Attached File Attached
12:07 22m Talk		Detecting Floating-Point Errors via Atomic Conditions Research Papers Daming Zou Peking University, Muhan Zeng Peking University, Yingfei Xiong Peking University, Zhoulai Fu IT University of Copenhagen, Denmark, Lu Zhang Peking University, Zhendong Su ETH Zurich Link to publication DOI Media Attached File Attached

14:00 - 15:05	Type SystemsResearch Papers at Ile de France II (IDF II) Chair(s): Peter Thiemann University of Freiburg, Germany

14:00 21m Talk		Undecidability of D<: and Its Decidable FragmentsDistinguished Paper Research Papers Jason Z.S. Hu McGill University, Ondřej Lhoták University of Waterloo Link to publication DOI Media Attached File Attached
14:21 21m Talk		Decidable Subtyping for Path Dependent Types Research Papers Julian Mackay Victoria University of Wellington, Alex Potanin Victoria University of Wellington, Jonathan Aldrich Carnegie Mellon University, Lindsay Groves Victoria University of Wellington Link to publication DOI Media Attached
14:43 21m Talk		Dependent Type Systems as Macros Research Papers Stephen Chang Northeastern University, Michael Ballantyne PLT @ Northeastern University, Milo Turner PLT @ Northeastern University, William J. Bowman University of British Columbia Link to publication DOI Media Attached File Attached

15:35 - 16:40	Program LogicsResearch Papers at Ile de France II (IDF II) Chair(s): Chung-Kil Hur Seoul National University

15:35 21m Talk		Deductive Verification with Ghost Monitors Research Papers Martin Clochard ETH Zürich, Claude Marché Inria Saclay & Université Paris-Saclay, Andrei Paskevich LRI, Université Paris-Sud & CNRS Link to publication DOI Media Attached
15:56 21m Talk		The Next 700 Relational Program Logics Research Papers Kenji Maillard Inria Nantes & University of Chile, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Antoine Van Muylder Inria Paris and Paris 7 Link to publication DOI Media Attached File Attached
16:18 21m Talk		Incorrectness Logic Research Papers Peter O'Hearn Facebook Link to publication DOI Media Attached

16:50 - 18:00	Business Meeting & SRC AwardsResearch Papers at Ile de France II (IDF II)

16:50 70m Meeting		Business Meeting & SRC Awards Research Papers Media Attached

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00	Invited TalkResearch Papers at Ile de France II (IDF II) Chair(s): Lars Birkedal Aarhus University

09:00 60m Talk		Probabilistic ProgrammingInvited Talk Research Papers Hongseok Yang KAIST Media Attached File Attached

10:30 - 11:35	Type SystemsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique Devriese Vrije Universiteit Brussel

10:30 21m Talk		Kind Inference for DatatypesDistinguished Paper Research Papers Ningning Xie University of Toronto, Richard A. Eisenberg Bryn Mawr College, USA, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong Link to publication DOI Media Attached
10:51 21m Talk		Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc Research Papers Mark Jones Portland State University, J. Garrett Morris University of Kansas, USA, Richard A. Eisenberg Bryn Mawr College, USA Link to publication DOI Media Attached File Attached
11:13 21m Talk		Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation Research Papers Roland Meyer TU Braunschweig, Sebastian Wolff TU Braunschweig Link to publication DOI Media Attached File Attached

11:45 - 12:30	Concurrent Programming & Session TypesResearch Papers at Ile de France II (IDF II) Chair(s): Susmit Sarkar University of St. Andrews

11:45 22m Talk		Label-Dependent Session Types Research Papers Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos University of Lisbon, Portugal Link to publication DOI Media Attached
12:07 22m Talk		Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs Research Papers Federico Aschieri TU Wien, Francesco A. Genco IHPST, Université Paris 1 Link to publication DOI Media Attached

14:00 - 15:05	Semantics of Probabilistic & Quantum ProgrammingResearch Papers at Ile de France II (IDF II) Chair(s): Alexandra Silva University College London

14:00 21m Talk		Full Abstraction for the Quantum Lambda-Calculus Research Papers Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS Lyon Link to publication DOI Media Attached File Attached
14:21 21m Talk		Relational Proofs for Quantum Programs Research Papers Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Mingsheng Ying University of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun Yu University of Technology Sydney, Australia, Li Zhou Max Planck Institute for Security and Privacy/Tsinghua University Link to publication DOI Pre-print Media Attached File Attached
14:43 21m Talk		A Probabilistic Separation Logic Research Papers Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Kevin Liao Max Planck Institute for Security and Privacy Link to publication DOI Media Attached

15:35 - 16:40	Semantics & Type TheoryResearch Papers at Ile de France II (IDF II) Chair(s): Arthur Azevedo de Amorim Carnegie Mellon University, USA

15:35 21m Talk		Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper Research Papers Davide Barbarossa Université Paris 13, Giulio Manzonetto Université Paris 13 Link to publication DOI Media Attached File Attached
15:56 21m Talk		Reduction Monads and Their Signatures Research Papers Benedikt Ahrens University of Birmingham, United Kingdom, André Hirschowitz Université Côte d'Azur, Ambroise Lafont Inria, France, Marco Maggesi Università di Firenze Link to publication DOI Media Attached
16:18 21m Talk		Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Research Papers Matthieu Sozeau Inria, Simon Boulier Inria, Yannick Forster Saarland University, Nicolas Tabareau Inria, Théo Winterhalter Inria — LS2N Link to publication DOI Media Attached File Attached

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America 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
Ile de France II (IDF II)										Research Papers Welcome + SIGPLAN Award Ceremony			Research Papers Invited Talk																		Research Papers Probabilistic Programming															Research Papers Reasoning about Program Complexity/Efficiency																											Research Papers Program Logics																			Research Papers Automatic Differentiation / Kleene Algebra															Research Papers Synthesis and Decision Procedures

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America 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
Ile de France II (IDF II)	Research Papers Invited Talk																		Research Papers Types and Effects															Research Papers Dynamic Program Analysis																											Research Papers Type Systems																			Research Papers Program Logics															Research Papers Business Meeting & SRC Awards

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America 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
Ile de France II (IDF II)	Research Papers Invited Talk																		Research Papers Type Systems															Research Papers Concurrent Programming & Session Types																											Research Papers Semantics of Probabilistic & Quantum Programming																			Research Papers Semantics & Type Theory

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America 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
Ile de France II (IDF II)										POPL Research Papers Welcome + SIGPLAN Award Ceremony 08:45 - 09:00			POPL Research PapersInvited Talk Can Programming Languages Research impact Deep Learning 2.0? 09:00 - 10:00																		POPL Research Papers Towards Verified Stochastic Variational Inference for Probabilistic Pro ... 10:30 - 10:51				POPL Research Papers Trace Types and Denotational Semantics for Sound Programmable Inference ... 10:51 - 11:13					POPL Research Papers Semantics of Higher-Order Probabilistic Programs with Conditioning 11:13 - 11:35						POPL Research Papers Recurrence Extraction for Functional Programs through Call-by-Push-Value 11:45 - 12:07				POPL Research Papers Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell 12:07 - 12:30																							POPL Research Papers The Future is Ours: Prophecy Variables in Separation Logic 14:00 - 14:21				POPL Research Papers Spy Game: Verifying a Local Generic Solver in Iris 14:21 - 14:43					POPL Research Papers Actris: Session-Type Based Reasoning in Separation Logic 14:43 - 15:05										POPL Research Papers A Simple Differentiable Programming Language 15:35 - 15:56				POPL Research Papers Backpropagation in the Simply Typed Lambda-calculus with Linear Negation 15:56 - 16:18					POPL Research PapersDistinguished Paper Guarded Kleene Algebra with Tests: Verification of Uninterpreted Progra ... 16:18 - 16:40						POPL Research Papers Visualization by Example 16:50 - 17:12				POPL Research Papers Deciding Memory Safety for Single-Pass Heap-Manipulating Programs 17:12 - 17:35

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America 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
Ile de France II (IDF II)	POPL Research PapersInvited Talk What is a Secure Programming Language? 09:00 - 10:00																		POPL Research Papers Binders by Day, Labels by Night: Effect Instances via Lexically Scoped ... 10:30 - 10:51				POPL Research Papers The Fire Triangle: How to Mix Substitution, Dependent Elimination, and ... 10:51 - 11:13					POPL Research Papers SyTeCi: Automating Contextual Equivalence for Higher-Order Programs wit ... 11:13 - 11:35						POPL Research Papers Fast, Sound, and Effectively Complete Dynamic Race Prediction 11:45 - 12:07				POPL Research Papers Detecting Floating-Point Errors via Atomic Conditions 12:07 - 12:30																							POPL Research PapersDistinguished Paper Undecidability of D<: and Its Decidable Fragments 14:00 - 14:21				POPL Research Papers Decidable Subtyping for Path Dependent Types 14:21 - 14:43					POPL Research Papers Dependent Type Systems as Macros 14:43 - 15:05										POPL Research Papers Deductive Verification with Ghost Monitors 15:35 - 15:56				POPL Research Papers The Next 700 Relational Program Logics 15:56 - 16:18					POPL Research Papers Incorrectness Logic 16:18 - 16:40						POPL Research Papers Business Meeting & SRC Awards 16:50 - 18:00

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America 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
Ile de France II (IDF II)	POPL Research PapersInvited Talk Probabilistic Programming 09:00 - 10:00																		POPL Research PapersDistinguished Paper Kind Inference for Datatypes 10:30 - 10:51				POPL Research Papers Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc 10:51 - 11:13					POPL Research Papers Pointer Life Cycle Types for Lock-Free Data Structures with Memory Recl ... 11:13 - 11:35						POPL Research Papers Label-Dependent Session Types 11:45 - 12:07				POPL Research Papers Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Fu ... 12:07 - 12:30																							POPL Research Papers Full Abstraction for the Quantum Lambda-Calculus 14:00 - 14:21				POPL Research Papers Relational Proofs for Quantum Programs 14:21 - 14:43					POPL Research Papers A Probabilistic Separation Logic 14:43 - 15:05										POPL Research PapersDistinguished Paper Taylor Subsumes Scott, Berry, Kahn and Plotkin 15:35 - 15:56				POPL Research Papers Reduction Monads and Their Signatures 15:56 - 16:18					POPL Research Papers Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq 16:18 - 16:40

Room information: Ile de France II (IDF II)

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: Ile de France II (IDF II)

Program Display Configuration

Wed 22 JanDisplayed time zone: Saskatchewan, Central America change

Thu 23 JanDisplayed time zone: Saskatchewan, Central America change

Fri 24 JanDisplayed time zone: Saskatchewan, Central America change

Wed 22 JanDisplayed time zone: Saskatchewan, Central America change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Thu 23 JanDisplayed time zone: Saskatchewan, Central America change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Fri 24 JanDisplayed time zone: Saskatchewan, Central America change

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Wed 22 JanDisplayed time zone: Saskatchewan, Central America change

Thu 23 JanDisplayed time zone: Saskatchewan, Central America change

Fri 24 JanDisplayed time zone: Saskatchewan, Central America change

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change

Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change

Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change

Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change