Write a Blog >>
VenueJW Marriott New Orleans
Room nameIle de France II (IDF II)
Floor3
Room InformationNo extra information available
Program

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
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, Dan 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
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 Bodik University of Washington, Alvin Cheung University of California, Berkeley, Isil 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

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
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 The University of Hong Kong, 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

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Ile de France II (IDF II)