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
Times are displayed in time zone: Saskatchewan, Central America change

08:45 - 09:00
Welcome + SIGPLAN Award CeremonyResearch Papers at Ile de France II (IDF II)
Chair(s): Brigitte PientkaMcGill University, Jens PalsbergUniversity of California, Los Angeles, Lars BirkedalAarhus University
08:45
15m
Day opening
Welcome + SIGPLAN Award Ceremony
Research Papers
Media Attached
11:45 - 12:30
Reasoning about Program Complexity/EfficiencyResearch Papers at Ile de France II (IDF II)
Chair(s): Thomas WiesNew York University
11:45
22m
Talk
Recurrence Extraction for Functional Programs through Call-by-Push-Value
Research Papers
Alex KavvosAarhus University, Edward MorehouseWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan 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 HandleyUniversity of Nottingham, Niki VazouIMDEA Software Institute, Graham HuttonUniversity 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 RaadMPI-SWS, Germany
14:00
21m
Talk
The Future is Ours: Prophecy Variables in Separation Logic
Research Papers
Ralf JungMPI-SWS, Rodolphe LepigreMPI-SWS, Gaurav ParthasarathyETH Zurich, Marianna RapoportUniversity of Waterloo, Amin Timanyimec-Distrinet KU-Leuven, Derek DreyerMPI-SWS, Bart Jacobsimec-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 VilhenaInria, François PottierInria, France, Jacques-Henri JourdanCNRS, 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 HinrichsenIT University of Copenhagen, Jesper BengtsonIT University of Copenhagen, Robbert KrebbersDelft 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 BirkedalAarhus 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 BrunelDeepomatic, Damiano MazzaCNRS, Michele PaganiIRIF - 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 SmolkaCornell University, Nate FosterCornell University, Justin HsuUniversity of Wisconsin-Madison, USA, Tobias KappéUniversity College London, Dexter KozenCornell University, Alexandra SilvaUniversity 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 SamantaPurdue University
16:50
22m
Talk
Visualization by Example
Research Papers
Chenglong WangUniversity of Washington, USA, Yu FengUniversity of California, Santa Barbara, Rastislav BodikUniversity of Washington, Alvin CheungUniversity of California, Berkeley, Isil DilligUniversity 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 MathurUniversity of Illinois at Urbana-Champaign, Adithya MuraliUniversity of Illinois at Urbana-Champaign, Paul KrogmeierUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached File Attached

Thu 23 Jan
Times are displayed in time zone: Saskatchewan, Central America change

11:45 - 12:30
Dynamic Program AnalysisResearch Papers at Ile de France II (IDF II)
Chair(s): Peter ThiemannUniversity of Freiburg, Germany
11:45
22m
Talk
Fast, Sound, and Effectively Complete Dynamic Race Prediction
Research Papers
Andreas PavlogiannisAarhus University
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Detecting Floating-Point Errors via Atomic Conditions
Research Papers
Daming ZouPeking University, Muhan ZengPeking University, Yingfei XiongPeking University, Zhoulai FuIT University of Copenhagen, Denmark, Lu ZhangPeking University, Zhendong SuETH 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 ThiemannUniversity of Freiburg, Germany
14:00
21m
Talk
Undecidability of D<: and Its Decidable FragmentsDistinguished Paper
Research Papers
Jason Z.S. HuMcGill University, Ondřej LhotákUniversity of Waterloo
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Decidable Subtyping for Path Dependent Types
Research Papers
Julian MackayVictoria University of Wellington, Alex PotaninVictoria University of Wellington, Jonathan AldrichCarnegie Mellon University, Lindsay GrovesVictoria University of Wellington
Link to publication DOI Media Attached
14:43
21m
Talk
Dependent Type Systems as Macros
Research Papers
Stephen ChangNortheastern University, Michael BallantynePLT @ Northeastern University, Milo TurnerPLT @ Northeastern University, William J. BowmanUniversity 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 HurSeoul National University
15:35
21m
Talk
Deductive Verification with Ghost Monitors
Research Papers
Martin ClochardETH Zürich, Claude MarchéInria Saclay & Université Paris-Saclay, Andrei PaskevichLRI, Université Paris-Sud & CNRS
Link to publication DOI Media Attached
15:56
21m
Talk
The Next 700 Relational Program Logics
Research Papers
Kenji MaillardInria Nantes & University of Chile, Cătălin HriţcuInria Paris, Exequiel RivasInria Paris, Antoine Van MuylderInria Paris and Paris 7
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Incorrectness Logic
Research Papers
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
Times are displayed in time zone: Saskatchewan, Central America change

09:00 - 10:00
Invited TalkResearch Papers at Ile de France II (IDF II)
Chair(s): Lars BirkedalAarhus University
09:00
60m
Talk
Probabilistic ProgrammingInvited Talk
Research Papers
Media Attached File Attached
11:45 - 12:30
Concurrent Programming & Session TypesResearch Papers at Ile de France II (IDF II)
Chair(s): Susmit SarkarUniversity of St. Andrews
11:45
22m
Talk
Label-Dependent Session Types
Research Papers
Peter ThiemannUniversity of Freiburg, Germany, Vasco T. VasconcelosUniversity 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 AschieriTU Wien, Francesco A. GencoIHPST, 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 SilvaUniversity College London
14:00
21m
Talk
Full Abstraction for the Quantum Lambda-Calculus
Research Papers
Pierre ClairambaultCNRS & ENS Lyon, Marc De VismeENS Lyon
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Relational Proofs for Quantum Programs
Research Papers
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun YuUniversity of Technology Sydney, Australia, Li ZhouMax 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 BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Kevin LiaoMax Planck Institute for Security and Privacy
Link to publication DOI Media Attached

Wed 22 Jan
Times are displayed in time zone: Saskatchewan, Central America change

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