Filter Program
Dates
Rooms
Tracks
Badges
Your Program
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 | |||
08:50 10mDay opening | Welcome TTT | ||
09:00 20mTalk | A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method TTT | ||
09:20 20mTalk | Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT | ||
09:40 20mTalk | Equivalence of System F and λ2 in Abella TTT | ||
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:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:00 | |||
10:30 30mTalk | Partitioned Memory Models for Program Analysis. VMCAI File Attached | ||
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 | ||
11:30 30mTalk | Stabilizing Floating-Point Programs using Provenance Analysis VMCAI | ||
10:30 - 12:00 | |||
10:30 50mTalk | Invited Talk -- Type Theory in the Software Analysis Workbench TTT Aaron Tomb Galois, Inc. | ||
11:20 20mTalk | Modelling Program Behaviour within Software Verification Tool LAV TTT | ||
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 | ||
11:15 45mTalk | Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities SCM File Attached | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 30mTalk | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI | ||
14:30 30mTalk | Independence Abstractions and Models of Concurrency 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:50 20mTalk | Equations: a tool for dependent pattern-matching TTT File Attached | ||
15:10 20mTalk | Coq's Prolog and application to defining semi-automatic tactics TTT File Attached | ||
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 | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Decision proceduresVMCAI at Amphitheater 44 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 | ||
17:00 30mTalk | Matching multiplications in Bit-Vector formulas VMCAI 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) | ||
17:10 50mOther | COST EUTypes session TTT | ||
16:00 - 17:30 | |||
16:00 45mTalk | Software Fault Isolation avec CompCert SCM File Attached | ||
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 | ||
08:50 10mTalk | Opening remarks PADL | ||
09:00 - 10:00 | |||
09:00 60mTalk | Verified Concurrent Code: Tricks of the Trade VMCAI | ||
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 60mTalk | Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk) PEPM DOI | ||
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 | |||
09:00 60mTalk | Proof checking and logic programming PADL Dale Miller INRIA Saclay and LIX | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
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 30mTalk | Verifying a hash table and its iterators in higher-order separation logic CPP | ||
11:00 30mTalk | A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm CPP | ||
11:30 30mTalk | Formal foundations of 3D geometry for modeling robot manipulators CPP | ||
10:30 - 12:00 | |||
10:30 30mTalk | Lightweight Soundness for Towers of Language Extensions PEPM | ||
11:00 30mTalk | Detecting code clones with gaps by function applications PEPM | ||
11:30 30mTalk | PEG Parsing in Less Space Using Progressive Tabling and Dynamic AnalysisBest Paper PEPM | ||
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 | ||
11:30 30mTalk | Integrating Answer Set Programming with Object-oriented Languages PADL | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch Catering | ||
14:00 - 15:30 | Model-checking and bug findingVMCAI at Amphitheater 44 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 30mTalk | BliStrTune: Hierarchical Invention of Theorem Proving Strategies CPP | ||
14:30 30mTalk | Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic CPP | ||
15:00 30mTalk | Formalization of Karp-Miller Tree Construction on Petri Nets CPP | ||
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 | ||
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 | ||
15:00 30mTalk | Language-integrated Query with Ordering, Grouping and Outer Joins (poster) PEPM | ||
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:00 30mTalk | Failing Faster: Overlapping Patterns for Property-Based Testing PADL | ||
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 | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44 Chair(s): Constantin Enea LIAFA, Université Paris Diderot | ||
16:00 30mTalk | Block-wise abstract interpretation by combining abstract domains with SMT VMCAI | ||
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:00 30mTalk | A Coq Formal Proof of the Lax–Milgram theorem CPP | ||
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 | ||
17:30 30mTalk | Formalising Real Numbers in Homotopy Type Theory CPP | ||
16:00 - 17:00 | Transformation (part I)PEPM at Salle 109, Barre 44-54 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 | ||
16:30 30mTalk | A Declarative DSL for Customized Rendering of Text-Based Art PADL | ||
17:00 30mTalk | Using Iterative Deepening for Probabilistic Logic Inference PADL | ||
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 | |||
08:50 10mDay opening | Welcome Sesssion PLMW | ||
09:00 - 10:00 | |||
09:00 60mTalk | Verification of Cancer Programs VMCAI Jasmin Fisher Microsoft Research | ||
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 60mTalk | Towards a metric semantics for probabilistic programming (invited talk) PPS | ||
09:00 - 10:00 | |||
09:00 30mTalk | Time management, family and quality of life PLMW Kathleen Fisher Tufts University File Attached | ||
09:30 30mTalk | Abductive Reasoning in Deductive Verification PLMW Işıl Dillig UT Austin File Attached | ||
09:00 - 10:00 | Tutorial: reversible computingPEPM at Salle 109, Barre 44-54 Chair(s): Ulrik Pagh Schultz University of Southern Denmark | ||
09:00 60mTalk | Reversible computing from a programming language perspective PEPM | ||
09:00 - 10:00 | |||
09:00 30mTalk | Funky Grooves: Declarative Programming of Full-Fledged Musical Applications PADL | ||
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:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:00 | Model Checking and SynthesisVMCAI at Amphitheater 44 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 | ||
10:50 10mMeeting | Discussion 1 PPS | ||
11:00 20mTalk | Probabilistic programming and a domain theoretic approach to Skorohod's theorem PPS Michael Mislove Tulane | ||
11:20 10mMeeting | Discussion 2 PPS | ||
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 | ||
11:50 10mMeeting | Discussion 3 PPS | ||
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 | ||
11:00 30mTalk | Mechanizing Meta-Theory in Beluga PLMW Brigitte Pientka McGill University File Attached | ||
11:30 30mTalk | Research: The Industrial Culture PLMW Nikhil Swamy Microsoft Research File Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Cost versus Precision for Approximate Typing for Python PEPM | ||
11:00 30mTalk | Refining types using type guards in TypeScript PEPM | ||
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 | |||
10:30 30mTalk | Improving Non-deterministic Computations in Functional Logic Programs PADL | ||
11:00 30mTalk | Canonicalizing High-Level Constructs in Picat PADL | ||
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 | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch Catering | ||
14:00 - 15:30 | Abstract InterpretationVMCAI at Amphitheater 44 Chair(s): Roberto Giacobazzi University of Verona, Italy | ||
14:00 30mTalk | Complete Abstractions and Subclassical Modal Logics VMCAI | ||
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:30 30mTalk | Lifting proof-relevant unification to higher dimensions CPP | ||
15:00 30mTalk | The Next 700 Syntactical models of type theory CPP | ||
14:00 - 15:30 | |||
14:00 20mTalk | Commutativity logic for probabilistic trace equivalence: complete or not? PPS | ||
14:20 10mMeeting | Discussion 4 PPS | ||
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:50 10mMeeting | Discussion 5 PPS | ||
15:00 20mTalk | A weakest pre-expectation semantics for mixed-sign expectations PPS | ||
15:20 10mMeeting | Discussion 6 PPS | ||
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 | ||
15:00 30mTalk | How to Give Talks That People Can Follow PLMW Derek Dreyer MPI-SWS File Attached | ||
14:00 - 15:30 | Tutorial: Partial Evaluation for Language ImplementationPEPM at Salle 109, Barre 44-54 Chair(s): Jeremy Yallop University of Cambridge, UK | ||
14:00 90mTalk | Practical Partial Evaluation for Language Implementation with Graal & Truffle PEPM | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
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 | ||
17:00 30mTalk | Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions VMCAI | ||
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:30 30mTalk | Formally verified differential dynamic logic CPP | ||
17:00 30mTalk | Equivalence of System F and λ2 in Coq based on context morphism lemmas CPP | ||
16:00 - 18:00 | |||
16:00 30mTalk | Machine Learning and Programming Languages: latest directions and research opportunities PLMW Martin Vechev ETH Zurich File Attached | ||
16:30 30mTalk | The Curse of Knowledge PLMW Benjamin C. Pierce University of Pennsylvania 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:00 30mTalk | Functional Parallels of Sequential Imperatives PEPM | ||
16:30 30mTalk | A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction PEPM | ||
16:30 - 18:00 | |||
16:30 20mTalk | An exponential family basis for probabilistic programming PPS Chad Scherrer Galois, Inc. | ||
16:50 10mMeeting | Discussion 7 PPS | ||
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:20 10mMeeting | Discussion 8 PPS | ||
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 | ||
17:50 10mMeeting | Discussion 9 PPS | ||
18:15 - 19:15 | |||
18:15 20mTalk | Reducing probabilistic choice to nondeterministic choice PPS Ernie Cohen Amazon Web Services | ||
18:35 10mMeeting | Discussion 10 PPS | ||
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. | ||
19:05 10mMeeting | Discussion 11 PPS | ||
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 | ||
09:00 5mDay opening | Opening POPL | ||
09:05 - 10:00 | Invited speakerPOPL at Auditorium Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
09:05 55mTalk | The Influence of Dependent Types POPL Stephanie Weirich University of Pennsylvania | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:10 | Abstract InterpretationPOPL at Amphitheater 44 Chair(s): Isabella Mastroeni University of Verona, Italy | ||
10:30 25mTalk | Ogre and Pythia, An invariance proof method for weak consistency models POPL | ||
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 | ||
11:45 25mTalk | Fast Polyhedra Abstract Domain POPL | ||
10:30 - 12:10 | |||
10:30 25mTalk | Polymorphism, subtyping and type inference in MLsub POPL | ||
10:55 25mTalk | Java generics are Turing complete POPL Radu Grigore University of Kent | ||
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 | ||
12:10 - 14:20 | |||
12:10 2h10mLunch | Lunch Catering | ||
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 | ||
14:45 25mTalk | Exact Bayesian Inference by Symbolic Disintegration POPL Pre-print | ||
15:10 25mTalk | Stochastic Invariants for Probabilistic Termination POPL Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria, Djordje Zikelic University of Cambridge | ||
15:35 25mTalk | Coupling proofs are probabilistic product programs POPL | ||
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:00 - 16:30 | |||
16:00 30mCoffee break | Break Catering | ||
16:30 - 17:45 | |||
16:30 25mTalk | Monadic second-order logic on finite sequences POPL | ||
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:30 25mTalk | A Program Optimization for Automatic Database Result Caching POPL | ||
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 | |||
19:30 3h30mDinner | Social dinner Catering | ||
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:00 5mAwards | Turing Award Video POPL | ||
09:05 5mAwards | Most Influential Paper Award POPL | ||
09:10 5mAwards | Reynolds Doctoral Dissertation Award POPL | ||
09:15 - 10:00 | |||
09:15 45mTalk | 40 Years of Abstract Interpretation — An Interview with Patrick Cousot POPL | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
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 | ||
10:55 25mTalk | Contract-based Resource Verification for Higher-order Functions with Memoization POPL | ||
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 | ||
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 | ||
11:20 25mTalk | Contextual isomorphisms POPL | ||
11:45 25mTalk | Typed Self-Evaluation via Intensional Type Functions POPL | ||
12:10 - 14:20 | |||
12:10 2h10mLunch | Lunch Catering | ||
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 | ||
14:45 25mTalk | Dynamic Race Detection For C++11 POPL | ||
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 | ||
14:45 25mTalk | Do be do be do POPL | ||
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 | ||
15:35 25mTalk | Stateful Manifest Contracts POPL | ||
16:00 - 16:30 | |||
16:00 30mCoffee break | Break Catering | ||
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 | ||
16:55 25mTalk | LOIS: syntax and semantics POPL | ||
17:20 - 18:20 | Business meetingPOPL at Auditorium Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
17:20 20mTalk | PC Chair report POPL Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
17:40 10mTalk | POPL 2018 presentation POPL | ||
17:50 30mMeeting | SIGPLAN business meeting POPL | ||
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 | ||
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 | ||
09:00 5mAwards | Student Competition Award Student Research Competition | ||
09:05 - 10:00 | |||
09:05 55mTalk | Rust: from POPL to practice POPL Aaron Turon MPI-SWS | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
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 | |||
10:30 25mTalk | Intersection Type Calculi of Bounded Dimension POPL | ||
10:55 25mTalk | Type Soundness Proofs with Definitional Interpreters POPL | ||
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 | ||
12:10 - 14:20 | |||
12:10 2h10mLunch | Lunch Catering | ||
14:20 - 16:00 | |||
14:20 25mTalk | Parallel Functional Arrays POPL | ||
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 | ||
14:20 25mTalk | Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System POPL | ||
14:45 25mTalk | Gradual Refinement Types POPL Link to publication DOI Pre-print | ||
15:10 25mTalk | Automatically Generating the Dynamic Semantics of Gradually Typed Languages POPL | ||
15:35 25mTalk | Sums of Uncertainty: Refinements go gradual POPL | ||
16:00 - 16:30 | |||
16:00 30mCoffee break | Break Catering | ||
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 | ||
17:20 25mTalk | QWIRE: A Core Language for Quantum Circuits POPL Jennifer Paykin , Robert Rand University of Pennsylvania, Steve Zdancewic University of Pennsylvania | ||
16:30 - 17:45 | |||
16:30 25mTalk | LMS-Verify: Abstraction Without Regret for Verified Systems Programming POPL | ||
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 | |||
08:45 15mDay opening | Opening N40AI | ||
08:55 - 09:00 | |||
08:55 5mTalk | Welcome PiP | ||
09:00 - 10:00 | |||
09:00 30mTalk | Abstract Interpretation in Absint N40AI Christian Ferdinand AbsInt | ||
09:30 30mTalk | Abstract Interpretation in Facebook N40AI Francesco Logozzo Facebook | ||
09:00 - 10:00 | |||
09:00 60mTalk | Invited Talk -- Demonstration of the Iris separation logic in Coq CoqPL | ||
09:00 - 10:00 | |||
09:00 30mTalk | Andrew Kennedy (Facebook) Static type checking for PHP PiP | ||
09:30 30mTalk | Jean-Louis Colaco (Ansys - Esterel Technologies) A brief history of the Scade language PiP | ||
09:00 - 10:00 | |||
09:00 15mTalk | Welcome RDP | ||
09:15 45mTalk | Automatic Verification of Database-Centric Workflows RDP | ||
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:00 - 10:30 | |||
10:00 30mCoffee break | Break Catering | ||
10:30 - 12:00 | |||
10:30 30mTalk | Abstract Interpretation in Amazon N40AI Byron Cook Amazon | ||
11:00 30mTalk | Abstract Interpretation at Galois N40AI Aaron Tomb Galois, Inc. | ||
11:30 30mTalk | Systems biology N40AI Vincent Danos ENS Paris/CNRS | ||
10:30 - 12:10 | |||
10:30 25mTalk | IxFree: Step-Indexed Logical Relations in Coq CoqPL File Attached | ||
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 | ||
11:45 25mTalk | ppsimpl: a reflexive Coq tactic for canonising goals CoqPL File Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Verification Challenges in Applications of Blockchain for Business Collaboration RDP Takaaki Tateishi IBM Research - Tokyo | ||
11:00 30mTalk | Fiat: A New Take on Domain-Specific Languages by Programming with Specifications RDP Adam Chlipala MIT | ||
11:30 30mTalk | Parallel-Correctness and Transferability for Conjunctive Queries RDP | ||
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:20 25mTalk | Programming Quantum Annealers Off the Beaten Track File Attached | ||
11:45 25mTalk | Understanding the POSIX Shell as a Programming Language Off the Beaten Track Michael Greenberg Pomona College File Attached | ||
12:00 - 14:00 | |||
12:00 2hLunch | Lunch Catering | ||
14:00 - 15:30 | Security, Big Code and Synthesis N40AI at Amphitheater 44 Chair(s): Xavier Rival INRIA/CNRS/ENS Paris | ||
14:00 30mTalk | Security N40AI Michael Hicks University of Maryland at College Park, USA | ||
14:30 30mTalk | Big Code N40AI Bor-Yuh Evan Chang University of Colorado Boulder | ||
15:00 30mTalk | Program synthesis N40AI Eran Yahav Technion | ||
14:00 - 15:30 | |||
14:00 60mTalk | Invited Talk -- Managing Logical and Computational Complexity using Program Transformations CoqPL | ||
15:00 30mDemonstration | Session with the Coq Development Team CoqPL Matthieu Sozeau Inria | ||
14:00 - 15:30 | |||
14:00 30mTalk | John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten years of QuickCheck PiP | ||
14:30 30mTalk | Byron Cook (Amazon) Automated Reasoning about AWS PiP | ||
15:00 30mTalk | Steve Zdancewic (U.Penn) Vellvm2: Semantics and Verification for LLVM PiP | ||
14:00 - 15:30 | |||
14:00 45mTalk | Synthesizing Data-parallel Programs RDP Aws Albarghouthi University of Wisconsin - Madison | ||
14:45 45mTalk | Cosette: A Solver for SQL Equivalences RDP Alvin Cheung University of Washington | ||
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 | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 18:30 | System Verification and Patrick Cousot's KeynoteN40AI at Amphitheater 44 Chair(s): Francesco Ranzato University of Padova | ||
16:00 30mTalk | System verification N40AI Arie Gurfinkel University of Waterloo | ||
16:30 75mTalk | Keynote: the Next 40 years of Abstract Interpretation N40AI Patrick Cousot New York University | ||
17:45 45mSocial Event | Concrete Cheese and Wine N40AI | ||
16:00 - 18:00 | |||
16:00 30mTalk | Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models PiP | ||
16:30 60mTalk | Discussion: Methods and Tools for large-scale semantics PiP | ||
16:00 - 18:00 | |||
16:00 30mTalk | Building performance-sensitive systems in high-level languages RDP | ||
16:30 30mTalk | Programming Language Ideas Escape the Lab: Declarative Data Description Languages for Managing Ad hoc Data RDP Kathleen Fisher Tufts University | ||
17:00 30mTalk | Computation with Atoms RDP | ||
17:30 30mTalk | Discussion RDP | ||
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 | ||
16:25 25mTalk | Laziness Boxes You In Off the Beaten Track File Attached | ||
16:50 25mTalk | Programming with Epistemic Logic Off the Beaten Track 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 | |||
19:00 2hSocial Event | CoqPL Social Event CoqPL | ||