Write a Blog >>
VenueJW Marriott New Orleans
Room nameIle de France III (IDF III)
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

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

09:00 - 10:00
Morning 1PLMW at Ile de France III (IDF III)
Chair(s): Stephanie BalzerCarnegie Mellon University, USA
09:00
10m
Day opening
Opening
PLMW
Brigitte PientkaMcGill University
09:10
50m
Talk
How to Write Papers So People Can Read ThemMentoring Event
PLMW
File Attached
14:00 - 15:05
Afternoon 1PLMW at Ile de France III (IDF III)
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA
14:00
65m
Talk
PanelMentoring Event
PLMW
William J. BowmanUniversity of British Columbia, Kenny FonerGalois, Andrew HirschMax Planck Institute for Software Systems, Taro SekiyamaNational Institute of Informatics, Juliana FrancoMicrosoft Research, Cambridge, Hannah GommerstadtVassar College
Media Attached

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

10:30 - 11:35
Complexity / Decision ProceduresResearch Papers at Ile de France III (IDF III)
Chair(s): Roopsha SamantaPurdue University
10:30
21m
Talk
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
Research Papers
Yannick ForsterSaarland University, Fabian KunzeSaarland University, Marc RothSaarland University and MMCI and Merton College, Oxford University
Link to publication DOI Pre-print Media Attached
10:51
21m
Talk
Complexity and Information in Invariant Inference
Research Papers
Yotam M. Y. FeldmanTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
Link to publication DOI Media Attached
11:13
21m
Talk
Parameterized Verification under TSO is PSPACE-Complete
Research Papers
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Rojin RezvanSharif University
Link to publication DOI
11:45 - 12:30
SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen LesaniUniversity of California, Riverside
11:45
22m
Talk
Program Synthesis by Type-Guided Abstraction Refinement
Research Papers
Zheng GuoUniversity of California, San Diego, Michael B. JamesUniversity of California, San Diego, David JustoUniversity of California, San Diego, Jiaxiao ZhouUniversity of California, San Diego, Ziteng WangUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Synthesizing Replacement Classes
Research Papers
Malavika SamakCSAIL, MIT, Deokhwan KimCSAIL, MIT, Martin RinardMIT
Link to publication DOI Media Attached File Attached
14:00 - 15:05
Gradual Typing / Language DesignResearch Papers at Ile de France III (IDF III)
Chair(s): Jeremy G. SiekIndiana University, USA
14:00
21m
Talk
What is Decidable about Gradual Types?
Research Papers
Zeina MigeedUniversity of California, Los Angeles, Jens PalsbergUniversity of California, Los Angeles
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Graduality and Parametricity: Together Again for the First Time
Research Papers
Max NewNortheastern University, Dustin JamnerNortheastern University, USA, Amal AhmedNortheastern University, USA
Link to publication DOI Media Attached
14:43
21m
Talk
Does Blame Shifting Work?
Research Papers
Lukas LazarekNorthwestern University, Alexis KingNorthwestern University, Samanvitha SundarNorthwestern University, Robby FindlerNorthwestern University, USA, Christos DimoulasPLT @ Northwestern University
Link to publication DOI Media Attached
15:35 - 16:40
Concurrency / MemoryResearch Papers at Ile de France III (IDF III)
Chair(s): Susmit SarkarUniversity of St. Andrews
15:35
21m
Talk
Persistency Semantics of the Intel-x86 Architecture
Research Papers
Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Gil NeigerIntel Corporation, Viktor VafeiadisMPI-SWS, Germany
Link to publication DOI Media Attached
15:56
21m
Talk
Reductions for Safety Proofs
Research Papers
Azadeh FarzanUniversity of Toronto, Anthony VandikasUniversity of Toronto
Link to publication DOI Media Attached
16:18
21m
Talk
RustBelt Meets Relaxed Memory
Research Papers
Hoang-Hai DangMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Jan-Oliver KaiserMPI-SWS, Derek DreyerMPI-SWS
Link to publication DOI Media Attached

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

10:30 - 11:35
SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen LesaniUniversity of California, Riverside
10:30
21m
Talk
Synthesis of Coordination Programs from Linear Temporal Specifications
Research Papers
Suguman BansalRice University, USA, Kedar NamjoshiBell Labs, Nokia, Yaniv Sa'arNokia Bell Labs, Kfar Saba, Israel
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
Augmented Example-based Synthesis using Relational Perturbation Properties
Research Papers
Shengwei AnPurdue University, Rishabh SinghGoogle Brain, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Roopsha SamantaPurdue University
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Provenance-Guided Synthesis of Datalog Programs
Research Papers
Mukund RaghothamanUniversity of Southern California, Jonathan MendelsonUniversity of Pennsylvania, David ZhaoThe University of Sydney, Mayur NaikUniversity of Pennsylvania, Bernhard ScholzUniversity of Sydney, Australia
Link to publication DOI Media Attached File Attached
11:45 - 12:30
Datalog, OO + Functional ProgrammingResearch Papers at Ile de France III (IDF III)
Chair(s): Brigitte PientkaMcGill University
11:45
22m
Talk
Seminaïve Evaluation for a Higher-Order Functional LanguageDistinguished Paper
Research Papers
Neel KrishnaswamiComputer Laboratory, University of Cambridge, Michael ArntzeniusUniversity of Birmingham, UK
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Decomposition Diversity with Symmetric Data and Codata
Research Papers
David BinderUniversity of Tübingen, Julian JabsUniversity of Tübingen, Ingo SkupinUniversity of Tübingen, Klaus OstermannUniversity of Tübingen, Germany
Link to publication DOI Media Attached
14:00 - 15:05
Abstract InterpretationResearch Papers at Ile de France III (IDF III)
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris
14:00
21m
Talk
Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Research Papers
Roberto BruniUniversity of Pisa, Roberto GiacobazziUniversity of Verona and IMDEA Software Institute, Roberta GoriUniversity of Pisa, Isabel Garcia-ContrerasIMDEA Software Institute, Dusko PavlovicUniversity of Hawaii
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Abstract Interpretation of Distributed Network Control Planes
Research Papers
Ryan BeckettMicrosoft Research, Aarti GuptaPrinceton University, Ratul MahajanUniversity of Washington, Intentionet, David WalkerPrinceton University
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Deterministic Parallel Fixpoint Computation
Research Papers
Sung Kook KimUniversity of California, Davis, Arnaud J. VenetFacebook, Aditya V. ThakurUniversity of California, Davis
Link to publication DOI Pre-print Media Attached File Attached
15:35 - 16:40
Probabilistic ProgrammingResearch Papers at Ile de France III (IDF III)
Chair(s): Ohad KammarUniversity of Edinburgh
15:35
21m
Talk
A Language for Probabilistically Oblivious Computation
Research Papers
David DaraisUniversity of Vermont, Ian SweetUniversity of Maryland, Chang LiuCitadel Securities, Michael HicksUniversity of Maryland
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
PλωNK: Functional Probabilistic NetKAT
Research Papers
Alexander VandenbrouckeKU Leuven, Belgium, Tom SchrijversKU Leuven
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Optimal Approximate Sampling From Discrete Probability Distributions
Research Papers
Feras SaadMassachusetts Institute of Technology, Cameron FreerMassachusetts Institute of Technology, Martin RinardMIT, Vikash MansinghkaMIT
Link to publication DOI Media Attached File Attached

Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change

10:30 - 11:35
Verification in Proof AssistantsResearch Papers at Ile de France III (IDF III)
Chair(s): Sandrine BlazyUniv Rennes- IRISA
10:30
21m
Talk
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Research Papers
Mengqi LiuYale University, Lionel RiegVerimag, Zhong ShaoYale University, Ronghui GuColumbia University, David CostanzoYale University, Jung-Eun KimYale University, Man-Ki YoonYale University
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
The High-Level Benefits of Low-Level Sandboxing
Research Papers
Michael SammlerMPI-SWS, Deepak GargMax Planck Institute for Software Systems, Derek DreyerMPI-SWS, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8
Link to publication DOI Media Attached
11:13
21m
Talk
Interaction Trees: Representing Recursive and Impure Programs in CoqDistinguished Paper
Research Papers
Li-yao XiaUniversity of Pennsylvania, Yannick ZakowskiUniversity of Pennsylvania, Paul HeUniversity of Pennsylvania, Chung-Kil HurSeoul National University, Gregory MalechaBedRock Systems, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
Link to publication DOI Media Attached File Attached
11:45 - 12:30
Probabilistic Reasoning and VerificationResearch Papers at Ile de France III (IDF III)
Chair(s): Arthur Azevedo de AmorimCarnegie Mellon University, USA
11:45
22m
Talk
Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Research Papers
Peixin WangShanghai Jiao Tong University, Hongfei FuShanghai Jiao Tong University, Krishnendu ChatterjeeIST Austria, Yuxin DengEast China Normal University, Ming XuEast China Normal University
Link to publication DOI Media Attached
12:07
22m
Talk
Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification
Research Papers
Marcel HarkRWTH Aachen University, Germany, Benjamin Lucien KaminskiRWTH Aachen University, Germany, Jürgen GieslRWTH Aachen University, Joost-Pieter KatoenRWTH Aachen University
Link to publication DOI Media Attached File Attached
14:00 - 15:05
Language DesignResearch Papers at Ile de France III (IDF III)
Chair(s): Amin Timanyimec-Distrinet KU-Leuven
14:00
21m
Talk
Stacked Borrows: An Aliasing Model for Rust
Research Papers
Ralf JungMPI-SWS, Hoang-Hai DangMPI-SWS, Jeehoon KangKAIST, Derek DreyerMPI-SWS
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Executable Formal Semantics for the POSIX Shell
Research Papers
Michael GreenbergPomona College, Austin J. BlattPuppet Labs
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Disentanglement in Nested-Parallel Programs
Research Papers
Sam WestrickCarnegie Mellon University, Rohan YadavCarnegie Mellon University, Matthew FluetRochester Institute of Technology, Umut A. AcarCarnegie Mellon University
Link to publication DOI Media Attached File Attached
15:35 - 16:40
Verified & Secure CompilationResearch Papers at Ile de France III (IDF III)
Chair(s): Andrew AppelPrinceton
15:35
21m
Talk
Formal Verification of a Constant-Time Preserving C Compiler
Research Papers
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine BlazyUniv Rennes- IRISA, Benjamin GregoireINRIA, Rémi HutinIRISA / ENS Rennes, Vincent LaporteInria, David PichardieUniv Rennes, ENS Rennes, IRISA, Alix TrieuAarhus University
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Research Papers
Youngju SongSeoul National University, Minki ChoSeoul National University, Dongjoo KimSeoul National University, Yonghyun KimSeoul National University, South Korea, Jeehoon KangKAIST, Chung-Kil HurSeoul National University
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Research Papers
Timothy BourkeInria / École normale supérieure, Lélio BrunENS/Inria, Marc PouzetÉcole normale supérieure
Link to publication DOI Media Attached File Attached

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Ile de France III (IDF III)

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

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