Filter Program
Dates
Rooms
Tracks
Badges
Your Program
You're viewing the program in a time zone which is different from your device's time zone change time zone
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 15 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:50 - 10:00
09:00 - 10:00
09:00
60mTalk
Detecting Strict Aliasing Violations in the Wild VMCAI
Pascal Cuoq Trust-in-Soft
File Attached 09:15 - 10:00
09:15
45mTalk
What is Secure Compilation? Part I SCM
Marco Patrignani MPI-SWS, Germany
Link to publication 10:30 - 12:00
11:00
30mTalk
Property Directed Reachability for Proving Absence of Concurrent Modification Errors VMCAI
Asya Frumkin Tel Aviv University, Yotam M. Y. Feldman Tel Aviv University, Ondřej Lhoták University of Waterloo, Canada, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
File Attached 10:30 - 12:00
10:30
50mTalk
Invited Talk -- Type Theory in the Software Analysis Workbench TTT
Aaron Tomb Galois, Inc.
11:40
20mTalk
agdARGS - Declarative Hierarchical Command Line Interfaces TTT
Guillaume Allais Radboud University Nijmegen
10:30 - 12:00
10:30
10mTalk
What is Secure Compilation? Part II (Short talk) SCM
Cătălin Hriţcu Inria Paris
Link to publication 10:40
10mTalk
Can relational logic facilitate secure compilation? (Short talk) SCM
David Naumann Stevens Institute of Technology
File Attached 10:50
10mTalk
Full Abstraction for Language Design (Short talk) SCM
Gabriel Scherer Northeastern University
File Attached 11:00
10mTalk
Cogent: Where we Stand and What Comes Next (Short talk) SCM
Christine Rizkallah University of Pennsylvania, USA
File Attached 14:00 - 15:30
14:00
30mTalk
Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI
15:00
30mTalk
Static Analysis of Communicating Process using Symbolic Transducers VMCAI
Vincent Botbol CEA LIST + LIP6 Université Pierre & Marie Curie, Tristan Le Gall CEA LIST, Emmanuel Chailloux LIP6 - UPMC
Media Attached File Attached 14:00 - 15:30
14:00
50mTalk
Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT
Anders Mörtberg Inria
14:00 - 15:30
14:00
45mTalk
Linking Types: Secure compilation of multi-language programs SCM
Daniel Patterson Northeastern University
File Attached 14:45
45mTalk
Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing SCM
Dominique Devriese iMinds - Distrinet, KU Leuven
File Attached 16:00 - 17:30
Decision proceduresVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
Chair(s): Andreas Podelski University of Freiburg, Germany
16:00
30mTalk
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games VMCAI
Ernst Moritz Hahn State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
File Attached 16:30
30mTalk
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI
Andrew Reynolds EPFL, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Cristina Serban VERIMAG, CNRS, Université Grenoble-Alpes
File Attached 16:00 - 18:00
16:00
50mTalk
Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq TTT
Robbert Krebbers Delft University of Technology, Netherlands
16:50
20mTalk
Introducing MetaCoq: A Safe Tactic Language for Coq TTT
Beta Ziliani FAMAF, UNC (Argentina) / CONICET (Argentina)
16:00 - 17:30
16:45
45mTalk
Security preserving compilation of low-level programs embedded in F* SCM
Jonathan Protzenko Microsoft Research
File Attached Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:50 - 09:00
Opening remarksPADL at Salle 116, Barre 44-54
Chair(s): Yuliya Lierler University of Nebraska, Walid Taha Halmstad University
Chair(s): Yuliya Lierler University of Nebraska, Walid Taha Halmstad University
09:00 - 10:00
09:00 - 10:00
09:00
60mTalk
Porting the HOL Light Analysis Library: Some Lessons CPP
Lawrence Paulson University of Cambridge
File Attached 09:00 - 12:00
09:00
3hTalk
The State of the Art in Gradual Typing Tutorials
Jeremy G. Siek Indiana University Bloomington
09:00 - 12:00
09:00
3hTalk
The Lean Theorem Prover Tutorials
Leonardo de Moura Microsoft Research, Redmond, Gabriel Ebner Vienna University of Technology, Jared Roesch University of Washington, USA, Sebastian Ullrich Karlsruhe Institute of Technology
09:00 - 10:00
09:00 - 12:00
09:00
3hTalk
Fast and Precise Type Checking for JavaScript: Are you in Flow? Tutorials
Avik Chaudhuri Facebook
Media Attached 09:00 - 12:00
09:00
3hTalk
Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins Tutorials
09:00 - 10:00
10:30 - 12:00
10:30
30mTalk
Sound Bit-Precise Numerical Domains VMCAI
Tushar Sharma University of Wisconsin - Madison, USA, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
File Attached 11:00
30mTalk
Efficient Elimination of Redundancies in Polyhedra using Raytracing VMCAI
Media Attached File Attached 11:30
30mTalk
Finding Relevant Templates via the Principal Component Analysis VMCAI
Yassamine Seladji University of Tlemcen
File Attached 10:30 - 12:00
10:30 - 12:00
10:30 - 12:00
10:30
30mTalk
Lowering the learning curve for declarative programming: a Python API for the IDP system PADL
Joost Vennekens KU Leuven
11:00
30mTalk
Extending Answer Set Programs with Interpreted Functions as First-class Citizens PADL
Christoph Redl Vienna University of Technology
14:00 - 15:30
Model-checking and bug findingVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
Chair(s): Andreas Podelski University of Freiburg, Germany
14:00
30mTalk
Effective Bug Finding in C Programs with Shape and Effect Abstraction VMCAI
Iago Abal IT University of Copenhagen, Claus Brabrand IT University of Copenhagen, Denmark, Andrzej Wąsowski IT University of Copenhagen, Denmark
14:30
30mTalk
Reduction of Workflow Nets for Generalised Soundness Verification VMCAI
Hadrien Bride Femto-ST / Université de Franche-Comté, Olga Kouchnarenko Femto-ST / Université de Franche-Comté, Fabien Peureux Femto-ST / Université de Franche-Comté + Smartesting S&S
Media Attached 15:00
30mTalk
Dynamic Reductions for Model Checking Concurrent Software. VMCAI
Henning Günther Technische Universität Wien, Alfons Laarman Vienna University of Technology, Ana Sokolova University of Salzburg, Georg Weissenbacher Technische Universität Wien
File Attached 14:00 - 15:30
14:00 - 17:00
14:00
3hTalk
The State of the Art in Gradual Typing Tutorials
Jeremy G. Siek Indiana University Bloomington
14:00 - 17:00
14:00
3hTalk
The Lean Theorem Prover Tutorials
Leonardo de Moura Microsoft Research, Redmond, Gabriel Ebner Vienna University of Technology, Jared Roesch University of Washington, USA, Sebastian Ullrich Karlsruhe Institute of Technology
14:00 - 15:30
Tutorial (Idris, Inside-Out) and Poster SessionPEPM at Salle 109, Barre 44-54
Chair(s): Ulrik Pagh Schultz University of Southern Denmark, Jeremy Yallop University of Cambridge, UK
Chair(s): Ulrik Pagh Schultz University of Southern Denmark, Jeremy Yallop University of Cambridge, UK
14:00
60mTalk
Idris, Inside-Out: A Tutorial on Extending Idris in Idris PEPM
David Thrane Christiansen Indiana University
15:00
30mTalk
Invited posters PEPM
Nada Amin EPFL, Tiark Rompf Purdue University, Oleg Kiselyov, Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens
14:00 - 17:00
14:00
3hTalk
Fast and Precise Type Checking for JavaScript: Are you in Flow? Tutorials
Avik Chaudhuri Facebook
Media Attached 14:00 - 17:00
14:00
3hTalk
Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins Tutorials
14:00 - 15:30
14:30
30mTalk
Boltzmann Samplers for Closed Simply-Typed Lambda Terms PADL
Maciej Bendkowski Jagiellonian University, Katarzyna Grygiel Jagiellonian University, Paul Tarau University of North Texas
15:00
30mTalk
Selection Equilibria of Higher-Order Games PADL
Paulo Oliva Queen Mary University of London, Jules Hedges University of Oxford, Viktor Winschel ETH Zürich, Philipp Zahn University of St. Gallen, Evguenia Shprits University of Mannheim
16:00 - 17:30
Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44
Chair(s): Constantin Enea LIAFA, Université Paris Diderot
Chair(s): Constantin Enea LIAFA, Université Paris Diderot
16:30
30mTalk
IC3 - Flipping the E in ICE VMCAI
Yakir Vizel, Arie Gurfinkel University of Waterloo, Sharon Shoham Tel Aviv university, Sharad Malik Princeton University
17:00
30mTalk
Counterexample Validation and Interpolation-Based Refinement for Forest Automata VMCAI
Lukáš Holík, Martin Hruska Brno University of Technology , Ondřej Lengál Brno University of Technology , Adam Rogalewicz Brno University of Technology , Tomáš Vojnar Brno University of Technology
16:00 - 18:00
16:30
30mTalk
A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations CPP
17:00
30mTalk
Markov Processes in Isabelle/HOL CPP
Johannes Hölzl Technische Universität München
DOI Pre-print File Attached 16:00 - 17:00
Transformation (part I)PEPM at Salle 109, Barre 44-54
Chair(s): Chung-chieh Shan Indiana University, USA
Chair(s): Chung-chieh Shan Indiana University, USA
16:00
30mTalk
Verification of Code Generators via Higher-Order Model Checking PEPM
Takashi Suwa University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Atsushi Igarashi Kyoto University
16:30
30mTalk
Interactive data representation migration: Exploiting program dependence to aid program transformation PEPM
Krishna Narasimhan Goethe University, Julia Lawall Inria/LIP6, Christoph Reichenbach Goethe University
16:00 - 17:30
16:00
30mTalk
A Domain-Specific Language for Software-Defined Radio PADL
Geoffrey Mainland Drexel University
Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:50 - 09:00
09:00 - 10:00
09:00 - 10:00
09:00
60mTalk
Mechanized verification of preemptive OS kernels CPP
Xinyu Feng University of Science and Technology of China
File Attached 09:00 - 10:00
09:00 - 10:00
09:00
30mTalk
Time management, family and quality of life PLMW
Kathleen Fisher Tufts University
File Attached 09:00 - 10:00
Tutorial: reversible computingPEPM at Salle 109, Barre 44-54
Chair(s): Ulrik Pagh Schultz University of Southern Denmark
Chair(s): Ulrik Pagh Schultz University of Southern Denmark
09:00 - 10:00
09:30
30mTalk
DALI for Cognitive Robotics: Principles and Prototype Implementation PADL
Stefania Costantini Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila, Giovanni De Gasperis Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Giulio Nazzicone Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica
10:30 - 12:00
Model Checking and SynthesisVMCAI at Amphitheater 44
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot
10:30
30mTalk
Reachability for dynamic parametric processes VMCAI
Anca Muscholl Université de Bordeaux / LaBRI, Helmut Seidl Technische Universität München, Igor Walukiewicz CNRS, LaBRI
11:00
30mTalk
Synthesizing Non-Vacuous Systems VMCAI
Roderick Bloem Institute of Software Technology, Graz University of Technology , Hana Chockler, ma e, Ofer Strichman Technion
File Attached 11:30
30mTalk
Solving Nonlinear Integer Arithmetic with MCSat VMCAI
Dejan Jovanović SRI International
10:30 - 12:00
10:30
30mTalk
Verified compilation of CakeML to multiple machine-code targets CPP
Anthony Fox University of Cambridge, UK, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan IHPC at A*STAR, Singapore, Ramana Kumar
11:00
30mTalk
COMPLX: a verification framework for concurrent imperative programs CPP
Sidney Amani UNSW, Australia, June Andronick Data61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin, Corey Lewis, Christine Rizkallah University of Pennsylvania, USA, Joseph Tuong
11:30
30mTalk
Verifying dynamic race detection CPP
William Mansky University of Pennsylvania, Yuanfeng Peng University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Joseph Devietti University of Pennsylvania
10:30 - 12:00
10:30
20mTalk
An application of computable distributions to the semantics of probabilistic programs: part 2 PPS
11:00
20mTalk
Probabilistic programming and a domain theoretic approach to Skorohod's theorem PPS
Michael Mislove Tulane
11:30
20mTalk
Building inference algorithms from monad transformers PPS
Adam Ścibior University of Cambridge, Yufei Cai University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany, Zoubin Ghahramani University of Cambridge
10:30 - 12:00
10:30
30mTalk
What is research and how to do it? Thinking globally and acting locally. PLMW
Michael Hicks University of Maryland at College Park, USA
File Attached 10:30 - 12:00
11:30
30mTalk
Predicting Resource Consumption of Higher-Order Workflows PEPM
Markus Klinik Radboud University Nijmegen, Jurriaan Hage Utrecht University, Jan Martin Jansen Netherlands Defence Academy, Rinus Plasmeijer Radboud University Nijmegen
10:30 - 12:00
11:30
30mTalk
An Overview of PRhoLog PADL
Besik Dundua Institute of Applied Mathematics, Tbilisi State University, Temur Kutsia, Klaus Reisenberger-Hagmayer Johannes Kepler University Linz
14:00 - 15:30
Abstract InterpretationVMCAI at Amphitheater 44
Chair(s): Roberto Giacobazzi University of Verona, Italy
Chair(s): Roberto Giacobazzi University of Verona, Italy
14:30
30mTalk
Structuring Abstract Interpreters through State and Value Abstractions VMCAI
Media Attached 15:00
30mTalk
Conjunctive Abstract Interpretation using Paramodulation VMCAI
Mooly Sagiv Tel Aviv University, A: Or Ozeri Tel Aviv university, Oded Padon Tel Aviv University, Noam Rinetzky Tel Aviv University
Media Attached 14:00 - 15:30
14:00
30mTalk
The HoTT library: a formalization of homotopy type theory in Coq CPP
Andrej Bauer University of Ljubljana, Jason Gross MIT CSAIL, Peter Lefanu Lumsdaine, Michael Shulman, Matthieu Sozeau Inria, Bas Spitters
Pre-print 14:00 - 15:30
14:30
20mTalk
Mathematical structures of probabilistic programming PPS
Ilias Garnier University of Edinburgh, Fredrik Dahlqvist University College London, Florence Clerc McGill University, Vincent Danos ENS Paris/CNRS
14:00 - 15:30
14:00
60mTalk
Student Interaction Activity PLMW
Eva Darulova MPI-SWS, Loris D'Antoni University of Wisconsin–Madison, Alexandra Silva University College London, Dimitrios Vytiniotis Microsoft Research, Cambridge
14:00 - 15:30
Tutorial: Partial Evaluation for Language ImplementationPEPM at Salle 109, Barre 44-54
Chair(s): Jeremy Yallop University of Cambridge, UK
Chair(s): Jeremy Yallop University of Cambridge, UK
15:30 - 16:30
15:30
60mMeeting
Encapsulating models and approximate inference programs in probabilistic modules PPS
15:30
60mMeeting
The extended semantics for probabilistic programming languages PPS
Siddharth Srivastava UTRC Berkeley, Nicholas Hay Vicarious, Yi WU UC Berkeley, Stuart Russell University of California, Berkeley
15:30
60mMeeting
Reasoning about inference in probabilistic programs PPS
Chandrakana Nandi University of Washington, USA, Adrian Sampson Cornell University, Dan Grossman University of Washington, Todd Mytkowicz, Kathryn S McKinley Microsoft Research
15:30
60mMeeting
On computable representations of exchangeable data PPS
Nathanael L. Ackerman Harvard University, Jeremy Avigad Carnegie Mellon University, Cameron Freer Gamalon and Borelian, Daniel Roy, Jason M. Rute Pennsylvania State University
15:30
60mMeeting
Probabilistic logic programs: unifying program trace and possible world semantics PPS
15:30
60mMeeting
Support and influence analysis for visualizing posteriors of probabilistic programs PPS
Long Ouyang Stanford University
15:30
60mMeeting
Efficient exact inference in discrete Anglican programs PPS
Robert Cornish University of Oxford, Frank Wood University of Oxford, Hongseok Yang University of Oxford
16:00 - 17:30
16:00
30mTalk
Using Abstract Interpretation to Correct Synchronization Faults VMCAI
Pietro Ferrara IBM Research, Omer Tripp IBM Thomas J. Watson Research Center, Peng Liu Purdue University, Eric Koskinen Yale University
16:30
30mTalk
Detecting All High-Level Dataraces in an RTOS Kernel. VMCAI
Suvam Mukherjee Indian Institute of Science, Arunkumar S Indian Institute of Science, Deepak D'Souza
16:00 - 17:30
16:00
30mTalk
Type-and-scope safe programs and their proofs CPP
Guillaume Allais Radboud University Nijmegen, James Chapman, Conor McBride, James McKinna University of Edinburgh
16:00 - 18:00
16:00
30mTalk
Machine Learning and Programming Languages: latest directions and research opportunities PLMW
Martin Vechev ETH Zurich
File Attached 17:00
60mTalk
Young Researcher Panel Session PLMW
Roopsha Samanta Purdue University, Nada Amin EPFL, Jonathan Protzenko Microsoft Research, Zachary Kincaid Princeton University
16:00 - 17:00
16:30 - 18:00
16:30
20mTalk
An exponential family basis for probabilistic programming PPS
Chad Scherrer Galois, Inc.
17:00
20mTalk
The semantics of subroutines and iteration in the Bayesian programming language ProBT PPS
Raphaël Laurent ProbaYes, Kamel Mekhnacha ProbaYes, Emmanuel Mazer CNRS/LIG, Pierre Bessière CNRS/ISIR
17:30
20mTalk
Exchangeable random process and data abstraction PPS
Sam Staton University of Oxford, Hongseok Yang University of Oxford, Nathanael L. Ackerman Harvard University, Cameron Freer Gamalon and Borelian, Daniel Roy
18:15 - 19:15
18:15
20mTalk
Reducing probabilistic choice to nondeterministic choice PPS
Ernie Cohen Amazon Web Services
18:45
20mTalk
GraPPa: spanning the expressivity vs. efficiency continuum PPS
Edwin Westbrook Galois, Inc., Chad Scherrer Galois, Inc., Nathan Collins Galois, Inc., Eric Mertens Galois, Inc.
Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 09:05
OpeningPOPL at Auditorium
Chair(s): Giuseppe Castagna Paris Diderot University & CNRS, Andrew D. Gordon Microsoft Research and University of Edinburgh
Chair(s): Giuseppe Castagna Paris Diderot University & CNRS, Andrew D. Gordon Microsoft Research and University of Edinburgh
09:05 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
10:30 - 12:10
Abstract InterpretationPOPL at Amphitheater 44
Chair(s): Isabella Mastroeni University of Verona, Italy
Chair(s): Isabella Mastroeni University of Verona, Italy
10:55
25mTalk
A Posteriori Environment Analysis with Pushdown Delta CFA POPL
Kimball Germane University of Utah, Matthew Might University of Utah; Harvard Medical School; The White House
11:20
25mTalk
Semantic-Directed Clumping of Disjunctive Abstract States POPL
Huisong Li INRIA/CNRS/ENS/PSL*, François Bérenger INRIA/CNRS/ENS/PSL*, Bor-Yuh Evan Chang University of Colorado Boulder, Xavier Rival INRIA/CNRS/ENS Paris
10:30 - 12:10
11:20
25mTalk
Hazelnut: A Bidirectionally Typed Structure Editor Calculus POPL
Cyrus Omar Carnegie Mellon University, Ian Voysey Carnegie Mellon University, Michael Hilton Oregon State University, USA, Jonathan Aldrich Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder
11:45
25mTalk
Modules, Abstraction, and Parametric Polymorphism POPL
Karl Crary Carnegie Mellon University
14:20 - 16:00
14:20
25mTalk
Beginner's Luck: A Language for Property-Based Generators POPL
Leonidas Lampropoulos University of Pennsylvania, Diane Gallois-Wong Inria Paris, ENS Paris, Cătălin Hriţcu Inria Paris, John Hughes Chalmers University of Technology, Benjamin C. Pierce University of Pennsylvania, Li-yao Xia ENS Paris
Pre-print 15:10
25mTalk
Stochastic Invariants for Probabilistic Termination POPL
Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria, Djordje Zikelic University of Cambridge
14:20 - 16:00
14:20
25mTalk
A Promising Semantics for Relaxed-Memory Concurrency POPL
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWS
Link to publication Pre-print Media Attached 14:45
25mTalk
Automatically Comparing Memory Consistency Models POPL
John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UK
Pre-print Media Attached File Attached 15:10
25mTalk
Interactive Proofs in Higher-Order Concurrent Separation Logic POPL
Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus University
DOI Pre-print Media Attached 15:35
25mTalk
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic POPL
Morten Krogh-Jespersen Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University
16:30 - 17:45
16:55
25mTalk
On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic POPL
Naoki Kobayashi University of Tokyo, Japan, Etienne Lozes ENS Cachan, Florian Bruse University of Kassel
17:20
25mTalk
Coming to Terms with Quantified Reasoning POPL
Simon Robillard Chalmers University of Technology, Andrei Voronkov University of Manchester, Laura Kovacs Chalmers University of Technology
16:30 - 17:45
16:55
25mTalk
Stream Fusion, to Completeness POPL
Oleg Kiselyov, Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens
Pre-print Media Attached 17:20
25mTalk
Rigorous Floating-point Mixed Precision Tuning POPL
Wei-Fan Chiang School of Computing, University of Utah, Ganesh Gopalakrishnan University of Utah, Zvonimir Rakamaric University of Utah, Ian Briggs School of Computing, University of Utah, Marek S. Baranowski University of Utah, Alexey Solovyev School of Computing, University of Utah
Pre-print 19:30 - 23:00
Thu 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 09:15
09:15 - 10:00
10:30 - 12:10
10:30
25mTalk
Relational Cost Analysis POPL
Ezgi Çiçek MPI-SWS, Germany, Gilles Barthe IMDEA, Marco Gaboardi SUNY Buffalo, USA, Deepak Garg MPI-SWS, Germany, Jan Hoffmann Carnegie Mellon University
11:20
25mTalk
Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability POPL
11:45
25mTalk
Towards Automatic Resource Bound Analysis for OCaml POPL
Jan Hoffmann Carnegie Mellon University, Ankush Das Carnegie Mellon University, Shu-chun Weng Yale University
10:30 - 12:10
Type Systems 2POPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
10:30
25mTalk
Deciding equivalence with sums and the empty type POPL
Gabriel Scherer Northeastern University
10:55
25mTalk
The exp-log normal form of types: Decomposing extensional equality and representing terms compactly POPL
Danko Ilik Trusted Labs
14:20 - 16:00
14:20
25mTalk
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC POPL
Shaked Flur University of Cambridge, Susmit Sarkar University of St. Andrews, UK, Christopher Pulte University of Cambridge, Kyndylan Nienhuis University of Cambridge, Luc Maranget INRIA Rocquencourt, Kathryn E. Gray University of Cambridge, Ali Sezgin University of Cambridge, Mark Batty University of Kent, Peter Sewell University of Cambridge
15:10
25mTalk
Serializability for Eventual Consistency: Criterion, Analysis and Applications POPL
Lucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH Zurich
Pre-print 15:35
25mTalk
Thread Modularity at Many Levels: a Pearl in Compositional Verification POPL
Jochen Hoenicke Universität Freiburg, Rupak Majumdar MPI-SWS, Andreas Podelski University of Freiburg, Germany
14:20 - 16:00
14:20
25mTalk
Type Directed Compilation of Row-Typed Algebraic Effects POPL
Daan Leijen Microsoft Research
15:10
25mTalk
Dijkstra Monads for Free POPL
Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Guido Martínez CIFASIS-CONICET, Argentina, Gordon Plotkin, Jonathan Protzenko Microsoft Research, Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft Research
Pre-print 16:30 - 17:20
16:30
25mTalk
A Semantic Account of Metric Preservation POPL
Arthur Azevedo de Amorim University of Pennsylvania, USA, Ikram Cherigui ENS Paris, Marco Gaboardi SUNY Buffalo, USA, Justin Hsu, Shin-ya Katsumata Kyoto University
16:55
25mTalk
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks POPL
Steffen Smolka Cornell University, Praveen Kumar Cornell University, Nate Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London
DOI File Attached 16:30 - 17:20
16:30
25mTalk
Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks POPL
Kausik Subramanian University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison, Aditya Akella University of Wisconsin-Madison
17:20 - 18:20
Business meetingPOPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
18:20 - 20:20
Poster SessionStudent Research Competition at Auditorium Hall
Chair(s): Matteo Cimini Indiana University, USA, Kim Nguyễn LRI, Université Paris-Sud, Julien Signoles CEA LIST, Qirun Zhang University of California, Davis
Chair(s): Matteo Cimini Indiana University, USA, Kim Nguyễn LRI, Université Paris-Sud, Julien Signoles CEA LIST, Qirun Zhang University of California, Davis
18:20
10mDemonstration
Naturality despite Nontermination: A Logical Relation for Linear Types and Polymorphism Student Research Competition
Nicholas Rioux Northeastern University
18:30
10mDemonstration
Gradual Type Precision as Retraction Student Research Competition
Max S. New Northeastern University
18:40
10mDemonstration
Linking Types: Specifying Safe Interoperability and Equivalences Student Research Competition
Daniel Patterson Northeastern University
18:50
10mDemonstration
A Monadic Framework for Bidirectional Programming Student Research Competition
Li-yao Xia ENS Paris
19:00
10mDemonstration
Gradual Set-Theoretic Types Student Research Competition
Victor Lanvin ENS Paris-Saclay
19:10
10mDemonstration
Abstract Interpretation of High-Level Transformations Student Research Competition
Ahmad Salim Al-Sibahi IT University of Copenhagen, Denmark
19:20
10mDemonstration
FairSquare: A Static Analysis Tool for Algorithmic Fairness Student Research Competition
Samuel Drews University of Wisconsin-Madison
19:30
10mDemonstration
Toward Type-Preserving Compilation of Coq Student Research Competition
William J. Bowman Northeastern University
19:40
10mDemonstration
A Symbolic Execution Framework for Haskell Student Research Competition
Anton Xue Yale University
19:50
10mDemonstration
Synthesizing Imperative Programs from Examples for Introductory Programming Assignments Student Research Competition
Sunbeom So Korea University
20:00
10mDemonstration
Provenance for Configuration Language Security Student Research Competition
Weili Fu University of Edinburgh
20:10
10mDemonstration
A gradually typed polymorphic lambda calculus Student Research Competition
Yuu Igarashi Kyoto University
Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Fri 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 09:05
Student Competition AwardStudent Research Competition at Auditorium
Chair(s): Kim Nguyễn LRI, Université Paris-Sud
Chair(s): Kim Nguyễn LRI, Université Paris-Sud
09:05 - 10:00
10:30 - 12:10
10:30
25mTalk
Component-Based Synthesis for Complex APIs POPL
Yu Feng University of Texas at Austin, USA, Ruben Martins, Yuepeng Wang University of Texas at Austin, Işıl Dillig UT Austin, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
10:55
25mTalk
Learning nominal automata POPL
Joshua Moerman Radboud University, Matteo Sammartino University College London, Alexandra Silva University College London, Bartek Klin University of Warsaw, Michał Szynwelski University of Warsaw
11:20
25mTalk
On Verifying Causal Consistency POPL
Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea LIAFA, Université Paris Diderot, Rachid Guerraoui, Jad Hamza LIAFA, Université Paris Diderot
11:45
25mTalk
Complexity Verification Using Guided Theorem Enumeration POPL
Akhilesh Srikanth Georgia Institute of Technology, Burak Sahin Georgia Institute of Technology, William Harris
10:30 - 12:10
11:20
25mTalk
Computational Higher-Dimensional Type Theory POPL
Carlo Angiuli Carnegie Mellon University, Robert Harper, Todd Wilson California State University Fresno
11:45
25mTalk
Type Systems as Macros POPL
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University
14:20 - 16:00
14:45
25mTalk
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms POPL
DOI Pre-print 15:10
25mTalk
Analyzing divergence in bisimulation semantics POPL
Xinxin Liu Institute of software, Chinese academy of sciences, Tingting Yu, Wenhui Zhang Institute of software, Chinese academy of sciences
15:35
25mTalk
Fencing off Go: Liveness and Safety for Channel-Based Programming POPL
Julien Lange Imperial College London, Nicholas Ng Imperial College London, Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London, UK
Pre-print 14:20 - 16:00
Gradual Typing and ContractsPOPL at Auditorium
Chair(s): Ronald Garcia University of British Columbia
Chair(s): Ronald Garcia University of British Columbia
14:20
25mTalk
Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System POPL
16:30 - 17:45
16:30
25mTalk
Invariants of Quantum Programs: Characterisations and Generation POPL
Mingsheng Ying University of Technology Sydney, Australia, Shenggang Ying University of Technology Sydney, Australia, Xiaodi Wu University of Oregon, USA
16:55
25mTalk
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects POPL
Ugo Dal Lago University of Bologna, France, Claudia Faggian, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay, Akira Yoshimizu Univ.Tokyo
16:30 - 17:45
16:55
25mTalk
Hypercollecting Semantics and its Application to Static Analysis of Information Flow POPL
Mounir Assaf Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Julien Signoles CEA LIST, Éric Totel CentraleSupélec, Frédéric Tronel CentraleSupélec
17:20
25mTalk
LightDP: Towards Automating Differential Privacy Proofs POPL
Danfeng Zhang Pennsylvania State University, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University
Sat 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sat 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:45 - 09:00
09:00 - 10:00
09:00 - 10:00
09:00 - 10:00
09:00
60mTalk
Keynote talk: Reasoning about Functional Programs: Exploring, Testing and Inductive Proofs. Off the Beaten Track
Moa Johansson Chalmers University of Technology
10:30 - 12:00
10:30 - 12:10
10:55
25mTalk
Logical Relations in Iris CoqPL
Amin Timany imec - Distrinet, KU Leuven, Robbert Krebbers Delft University of Technology, Netherlands, Lars Birkedal Aarhus University
File Attached 11:20
25mTalk
Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting CoqPL
File Attached 10:30 - 12:05
10:35
30mTalk
Simon Moore (Cambridge) Experiences of Formal Modelling in the CHERI Computer Architecture Research Project PiP
10:30 - 12:00
10:30
30mTalk
Verification Challenges in Applications of Blockchain for Business Collaboration RDP
Takaaki Tateishi IBM Research - Tokyo
10:30 - 12:10
10:30
25mTalk
Can we machine-learn programming language semantics? Off the Beaten Track
File Attached 10:55
25mTalk
How Far Apart Should Those Programs Be? Off the Beaten Track
Ugo Dal Lago University of Bologna, France
File Attached 11:45
25mTalk
Understanding the POSIX Shell as a Programming Language Off the Beaten Track
Michael Greenberg Pomona College
File Attached 14:00 - 15:30
Security, Big Code and Synthesis N40AI at Amphitheater 44
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
14:00 - 15:30
14:00 - 15:30
14:00 - 15:30
14:00
45mTalk
Synthesizing Data-parallel Programs RDP
Aws Albarghouthi University of Wisconsin - Madison
14:00 - 15:25
14:00
60mTalk
Keynote talk: Varieties of Programming Experience Off the Beaten Track
Alan Blackwell University of Cambridge
15:00
25mTalk
Bootstrapping the next generation of mathematical social machines Off the Beaten Track
File Attached 16:00 - 18:30
System Verification and Patrick Cousot's KeynoteN40AI at Amphitheater 44
Chair(s): Francesco Ranzato University of Padova
Chair(s): Francesco Ranzato University of Padova
16:30
75mTalk
Keynote: the Next 40 years of Abstract Interpretation N40AI
Patrick Cousot New York University
16:00 - 18:05
16:25
25mTalk
CertiCoq: A verified compiler for Coq CoqPL
Abhishek Anand, Andrew W. Appel Princeton, Greg Morrisett Cornell University, Zoe Paraskevopoulou Princeton University, USA, Randy Pollack Harvard University, Olivier Savary Belanger Princeton University, Matthieu Sozeau Inria, Matthew Weaver Princeton University
File Attached 16:50
25mTalk
CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL CoqPL
Izumi Asakura Tokyo Institute of Technology, Japan, Hidehiko Masuhara Tokyo Institute of Technology, Tomoyuki Aotani Tokyo Institute of Technology
File Attached 17:15
25mTalk
Verification of Implementations of Distributed Systems Under Churn CoqPL
Ryan Doenges University of Washington, James R. Wilcox University of Washington, Doug Woos University of Washington, Zachary Tatlock University of Washington, Seattle, Karl Palmskog
File Attached 16:00 - 18:00
16:00 - 18:00
16:30
30mTalk
Programming Language Ideas Escape the Lab: Declarative Data Description Languages for Managing Ad hoc Data RDP
Kathleen Fisher Tufts University
16:00 - 18:05
16:00
25mTalk
Designing extensible, domain-specific languages for mathematical diagrams Off the Beaten Track
Katherine Ye, Keenan Crane, Jonathan Aldrich Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University
File Attached 17:15
25mTalk
Preventing False Discoveries in Adaptive Data Analysis: a Programming Language approach Off the Beaten Track
Marco Gaboardi SUNY Buffalo, USA
File Attached 17:40
25mTalk
Running Incomplete Programs Off the Beaten Track
Ian Voysey Carnegie Mellon University, Cyrus Omar Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder
File Attached 19:00 - 21:00
iCalendar subscription service for your personal schedule
You first need to have starred events () in order to use the iCalendar subscription service.
Currently Viewed Program
Downloads the currently viewed program (with filters applied) in iCal format
x Sat 5 Sep 08:41