You're viewing a filtered program.
Do you want to keep these filters active in the new view?
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
08:50 - 10:00 | First Morning SessionTTT at Salle 105, Barre 44-54 | ||
08:50 10m Day opening | Welcome TTT | ||
09:00 20m Talk | A Case Study in Programming Coinductive Proofs in Beluga: Howe's Method TTT David Thibodeau McGill University, Canada, Alberto Momigliano , Brigitte Pientka McGill University | ||
09:20 20m Talk | Needle & Knot: A Framework for Meta-Theoretical Specifications with Binding TTT Steven Keuchel , Koar Marntirosian , Tom Schrijvers KU Leuven | ||
09:40 20m Talk | Equivalence of System F and λ2 in Abella TTT Jonas Kaiser , Gert Smolka Saarland University | ||
09:00 - 10:00 | Invited talk 1VMCAI at Amphitheater 44 | ||
09:00 60m Talk | Detecting Strict Aliasing Violations in the Wild VMCAI Pascal Cuoq Trust-in-Soft | ||
09:15 - 10:00 | Session ISCM at Salle 109, Barre 44-54 | ||
09:15 45m Talk | What is Secure Compilation? Part I SCM Marco Patrignani MPI-SWS, Germany | ||
10:00 - 10:30 | Coffee breakCatering at Catering area | ||
10:00 30m Coffee break | Break Catering | ||
10:30 - 12:00 | Program AnalysisVMCAI at Amphitheater 44 | ||
10:30 30m Talk | Partitioned Memory Models for Program Analysis. VMCAI Wei Wang Google, Inc., Clark Barrett Stanford University, Thomas Wies New York University | ||
11:00 30m Talk | 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 | ||
11:30 30m Talk | Stabilizing Floating-Point Programs using Provenance Analysis VMCAI Yijia Gu Northeastern University, Thomas Wahl Northeastern University | ||
10:30 - 12:00 | Second Morning SessionTTT at Salle 105, Barre 44-54 | ||
10:30 50m Talk | Invited Talk -- Type Theory in the Software Analysis Workbench TTT Aaron Tomb Galois, Inc. | ||
11:20 20m Talk | Modelling Program Behaviour within Software Verification Tool LAV TTT | ||
11:40 20m Talk | agdARGS - Declarative Hierarchical Command Line Interfaces TTT Guillaume Allais Radboud University Nijmegen | ||
10:30 - 12:00 | Session IISCM at Salle 109, Barre 44-54 | ||
10:30 10m Talk | What is Secure Compilation? Part II (Short talk) SCM Cătălin Hriţcu Inria Paris | ||
10:40 10m Talk | Can relational logic facilitate secure compilation? (Short talk) SCM David Naumann Stevens Institute of Technology | ||
10:50 10m Talk | Full Abstraction for Language Design (Short talk) SCM Gabriel Scherer Northeastern University | ||
11:00 10m Talk | Cogent: Where we Stand and What Comes Next (Short talk) SCM Christine Rizkallah University of Pennsylvania, USA | ||
11:15 45m Talk | Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities SCM File Attached | ||
12:00 - 14:00 | BuffetCatering at Catering area | ||
12:00 2h Lunch | Lunch Catering | ||
14:00 - 15:30 | Concurrency 1VMCAI at Amphitheater 44 | ||
14:00 30m Talk | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms VMCAI Igor Konnov TU Wien, Josef Widder TU Wien, Francesco Spegni , Luca Spalazzi | ||
14:30 30m Talk | Independence Abstractions and Models of Concurrency VMCAI Vijay D'Silva Google Inc., Daniel Kroening University of Oxford, Marcelo Sousa University of Oxford | ||
15:00 30m Talk | 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 | ||
14:00 - 15:30 | First Afternoon SessionTTT at Salle 105, Barre 44-54 | ||
14:00 50m Talk | Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders Mörtberg Inria | ||
14:50 20m Talk | Equations: a tool for dependent pattern-matching TTT Cyprien Mangin , Matthieu Sozeau Inria | ||
15:10 20m Talk | Coq's Prolog and application to defining semi-automatic tactics TTT Théo Zimmermann IRIF, Université Paris Diderot, Hugo Herbelin | ||
14:00 - 15:30 | Session IIISCM at Salle 109, Barre 44-54 | ||
14:00 45m Talk | Linking Types: Secure compilation of multi-language programs SCM Daniel Patterson Northeastern University | ||
14:45 45m Talk | Fully-Abstract Compilation of Parametric Polymorphism into Dynamic Sealing SCM Dominique Devriese iMinds - Distrinet, KU Leuven | ||
15:30 - 16:00 | Coffee breakCatering at Catering area | ||
15:30 30m Coffee break | Break Catering | ||
16:00 - 17:30 | Decision proceduresVMCAI at Amphitheater 44 | ||
16:00 30m Talk | 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 30m Talk | 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 | ||
17:00 30m Talk | Matching multiplications in Bit-Vector formulas VMCAI Supratik Chakraborty IIT Bombay, Ashutosh Gupta , Rahul Jain Tata Institute of Fundamental Research | ||
16:00 - 18:00 | Second Afternoon SessionTTT at Salle 105, Barre 44-54 | ||
16:00 50m Talk | Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq TTT Robbert Krebbers Delft University of Technology, Netherlands | ||
16:50 20m Talk | Introducing MetaCoq: A Safe Tactic Language for Coq TTT Beta Ziliani FAMAF, UNC (Argentina) / CONICET (Argentina) | ||
17:10 50m Other | COST EUTypes session TTT | ||
16:00 - 17:30 | Session IVSCM at Salle 109, Barre 44-54 | ||
16:00 45m Talk | Software Fault Isolation avec CompCert SCM File Attached | ||
16:45 45m Talk | Security preserving compilation of low-level programs embedded in F* SCM Jonathan Protzenko Microsoft Research | ||
08:50 - 09:00 | Opening remarksPADL at Salle 116, Barre 44-54 | ||
08:50 10m Talk | Opening remarks PADL | ||
09:00 - 10:00 | Invited talk 2VMCAI at Amphitheater 44 | ||
09:00 60m Talk | Verified Concurrent Code: Tricks of the Trade VMCAI A: Ernie Cohen Amazon Web Services | ||
09:00 - 10:00 | Invited TalkCPP at Auditorium | ||
09:00 60m Talk | Porting the HOL Light Analysis Library: Some Lessons CPP Lawrence Paulson University of Cambridge | ||
09:00 - 12:00 | Gradual Typing (AM)Tutorials at Salle 105, Barre 44-54 | ||
09:00 3h Talk | The State of the Art in Gradual Typing Tutorials Jeremy G. Siek Indiana University Bloomington | ||
09:00 - 12:00 | Lean (AM)Tutorials at Salle 107, Barre 44-54 | ||
09:00 3h Talk | 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 | KeynotePEPM at Salle 109, Barre 44-54 | ||
09:00 60m Talk | Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation (Invited Talk) PEPM Daniil Berezun JetBrains, Russia, Neil D. Jones University of Copenhagen, Danmark | ||
09:00 - 12:00 | Flow (AM)Tutorials at Salle 112, Barre 44-54 | ||
09:00 3h Talk | Fast and Precise Type Checking for JavaScript: Are you in Flow? Tutorials Avik Chaudhuri Facebook | ||
09:00 - 12:00 | Frama-C (AM)Tutorials at Salle 114, Barre 44-54 | ||
09:00 3h Talk | Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins Tutorials François Bobot CEA, Loïc Correnson , Boris Yakobowski CEA - LIST | ||
09:00 - 10:00 | Invited TalkPADL at Salle 116, Barre 44-54 | ||
09:00 60m Talk | Proof checking and logic programming PADL Dale Miller INRIA Saclay and LIX | ||
10:00 - 10:30 | Coffee breakCatering at Auditorium Hall | ||
10:00 30m Coffee break | Break Catering | ||
10:30 - 12:00 | Numerical domainsVMCAI at Amphitheater 44 | ||
10:30 30m Talk | 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 30m Talk | Efficient Elimination of Redundancies in Polyhedra using Raytracing VMCAI Media Attached File Attached | ||
11:30 30m Talk | Finding Relevant Templates via the Principal Component Analysis VMCAI Yassamine Seladji University of Tlemcen | ||
10:30 - 12:00 | Algorithm and library verificationCPP at Auditorium | ||
10:30 30m Talk | Verifying a hash table and its iterators in higher-order separation logic CPP | ||
11:00 30m Talk | A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm CPP Jose Divasón , Sebastiaan Joosten , René Thiemann University of Innsbruck, Akihisa Yamada | ||
11:30 30m Talk | Formal foundations of 3D geometry for modeling robot manipulators CPP Reynald Affeldt AIST, Japan, Cyril Cohen | ||
10:30 - 12:00 | Programming languagesPEPM at Salle 109, Barre 44-54 | ||
10:30 30m Talk | Lightweight Soundness for Towers of Language Extensions PEPM Alejandro Serrano Utrecht University, Jurriaan Hage Utrecht University | ||
11:00 30m Talk | Detecting code clones with gaps by function applications PEPM Tsubasa Matsushita Shibaura Institute of Technology, Isao Sasano Shibaura Institute of Technology | ||
11:30 30m Talk | PEG Parsing in Less Space Using Progressive Tabling and Dynamic AnalysisBest Paper PEPM Fritz Henglein DIKU, Denmark, Ulrik Terp Rasmussen DIKU, University of Copenhagen | ||
10:30 - 12:00 | Answer Set ProgrammingPADL at Salle 116, Barre 44-54 | ||
10:30 30m Talk | Lowering the learning curve for declarative programming: a Python API for the IDP system PADL Joost Vennekens KU Leuven | ||
11:00 30m Talk | Extending Answer Set Programs with Interpreted Functions as First-class Citizens PADL Christoph Redl Vienna University of Technology | ||
11:30 30m Talk | Integrating Answer Set Programming with Object-oriented Languages PADL Jakob Rath Vienna University of Technology, Christoph Redl Vienna University of Technology | ||
12:00 - 14:00 | BuffetCatering at Catering area | ||
12:00 2h Lunch | Lunch Catering | ||
14:00 - 15:30 | Model-checking and bug findingVMCAI at Amphitheater 44 | ||
14:00 30m Talk | 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 30m Talk | 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 30m Talk | 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 | ||
14:00 - 15:30 | Automated proof and its verificationCPP at Auditorium | ||
14:00 30m Talk | BliStrTune: Hierarchical Invention of Theorem Proving Strategies CPP | ||
14:30 30m Talk | Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic CPP Reuben Rowe University College London, James Brotherston | ||
15:00 30m Talk | Formalization of Karp-Miller Tree Construction on Petri Nets CPP | ||
14:00 - 17:00 | Gradual Typing (PM)Tutorials at Salle 105, Barre 44-54 | ||
14:00 3h Talk | The State of the Art in Gradual Typing Tutorials Jeremy G. Siek Indiana University Bloomington | ||
14:00 - 17:00 | Lean (PM)Tutorials at Salle 107, Barre 44-54 | ||
14:00 3h Talk | 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 | ||
14:00 60m Talk | Idris, Inside-Out: A Tutorial on Extending Idris in Idris PEPM David Thrane Christiansen Indiana University | ||
15:00 30m Talk | 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 30m Talk | Language-integrated Query with Ordering, Grouping and Outer Joins (poster) PEPM Tatsuya Katsushima Tohoku University, Japan, Oleg Kiselyov | ||
14:00 - 17:00 | Flow (PM)Tutorials at Salle 112, Barre 44-54 | ||
14:00 3h Talk | Fast and Precise Type Checking for JavaScript: Are you in Flow? Tutorials Avik Chaudhuri Facebook | ||
14:00 - 17:00 | Frama-C (PM)Tutorials at Salle 114, Barre 44-54 | ||
14:00 3h Talk | Let's Implement Your New Analysis using Industrially Strengthened Frama-C Plugins Tutorials François Bobot CEA, Loïc Correnson , Boris Yakobowski CEA - LIST | ||
14:00 - 15:30 | Testing and GamesPADL at Salle 116, Barre 44-54 | ||
14:00 30m Talk | Failing Faster: Overlapping Patterns for Property-Based Testing PADL Jonathan Fowler University of Nottingham, Graham Hutton University of Nottingham | ||
14:30 30m Talk | 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 30m Talk | 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 | Coffee breakCatering at Auditorium Hall | ||
15:30 30m Coffee break | Break Catering | ||
16:00 - 17:30 | Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44 | ||
16:00 30m Talk | Block-wise abstract interpretation by combining abstract domains with SMT VMCAI | ||
16:30 30m Talk | 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 30m Talk | 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 | Formalized mathematics with numerical computationsCPP at Auditorium | ||
16:00 30m Talk | A Coq Formal Proof of the Lax–Milgram theorem CPP | ||
16:30 30m Talk | A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations CPP Erik Martin-Dorel IRIT, Université Paul Sabatier, Pierre Roux | ||
17:00 30m Talk | Markov Processes in Isabelle/HOL CPP Johannes Hölzl Technische Universität München | ||
17:30 30m Talk | Formalising Real Numbers in Homotopy Type Theory CPP | ||
16:00 - 17:00 | Transformation (part I)PEPM at Salle 109, Barre 44-54 | ||
16:00 30m Talk | 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 30m Talk | 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 | Applications I and InferencePADL at Salle 116, Barre 44-54 | ||
16:00 30m Talk | A Domain-Specific Language for Software-Defined Radio PADL Geoffrey Mainland Drexel University | ||
16:30 30m Talk | A Declarative DSL for Customized Rendering of Text-Based Art PADL | ||
17:00 30m Talk | Using Iterative Deepening for Probabilistic Logic Inference PADL Theofrastos Mantadelis Universidade do Porto, Ricardo Rocha | ||
08:50 - 09:00 | Welcome SessionPLMW at Salle 107, Barre 44-54 | ||
08:50 10m Day opening | Welcome Sesssion PLMW | ||
09:00 - 10:00 | Invited talk 3VMCAI at Amphitheater 44 | ||
09:00 60m Talk | Verification of Cancer Programs VMCAI Jasmin Fisher Microsoft Research | ||
09:00 - 10:00 | Invited TalkCPP at Auditorium | ||
09:00 60m Talk | Mechanized verification of preemptive OS kernels CPP Xinyu Feng University of Science and Technology of China File Attached | ||
09:00 - 10:00 | Session 1 PPS at Salle 105, Barre 44-54 | ||
09:00 60m Talk | Towards a metric semantics for probabilistic programming (invited talk) PPS | ||
09:00 - 10:00 | Session IPLMW at Salle 107, Barre 44-54 | ||
09:00 30m Talk | Time management, family and quality of life PLMW Kathleen Fisher Tufts University | ||
09:30 30m Talk | Abductive Reasoning in Deductive Verification PLMW Işıl Dillig UT Austin | ||
09:00 - 10:00 | Tutorial: reversible computingPEPM at Salle 109, Barre 44-54 | ||
09:00 60m Talk | Reversible computing from a programming language perspective PEPM | ||
09:00 - 10:00 | Applications IIPADL at Salle 116, Barre 44-54 | ||
09:00 30m Talk | Funky Grooves: Declarative Programming of Full-Fledged Musical Applications PADL Henrik Nilsson , Guerric Chupin ENSTA ParisTech | ||
09:30 30m Talk | 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 | Coffee breakCatering at Auditorium Hall | ||
10:00 30m Coffee break | Break Catering | ||
10:30 - 12:00 | Model Checking and SynthesisVMCAI at Amphitheater 44 | ||
10:30 30m Talk | 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 30m Talk | Synthesizing Non-Vacuous Systems VMCAI Roderick Bloem Institute of Software Technology, Graz University of Technology , Hana Chockler , ma e , Ofer Strichman Technion | ||
11:30 30m Talk | Solving Nonlinear Integer Arithmetic with MCSat VMCAI Dejan Jovanović SRI International | ||
10:30 - 12:00 | Verified programming toolsCPP at Auditorium | ||
10:30 30m Talk | 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 30m Talk | 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 30m Talk | 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 | Session 2 PPS at Salle 105, Barre 44-54 | ||
10:30 20m Talk | An application of computable distributions to the semantics of probabilistic programs: part 2 PPS Daniel Huang Harvard University, Greg Morrisett Cornell University | ||
10:50 10m Meeting | Discussion 1 PPS | ||
11:00 20m Talk | Probabilistic programming and a domain theoretic approach to Skorohod's theorem PPS Michael Mislove Tulane | ||
11:20 10m Meeting | Discussion 2 PPS | ||
11:30 20m Talk | 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 10m Meeting | Discussion 3 PPS | ||
10:30 - 12:00 | Session IIPLMW at Salle 107, Barre 44-54 | ||
10:30 30m Talk | 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 30m Talk | Mechanizing Meta-Theory in Beluga PLMW Brigitte Pientka McGill University | ||
11:30 30m Talk | Research: The Industrial Culture PLMW Nikhil Swamy Microsoft Research | ||
10:30 - 12:00 | TypesPEPM at Salle 109, Barre 44-54 | ||
10:30 30m Talk | Cost versus Precision for Approximate Typing for Python PEPM Levin Fritz Utrecht University, Jurriaan Hage Utrecht University | ||
11:00 30m Talk | Refining types using type guards in TypeScript PEPM Ivo Gabe de Wolff Utrecht University, Jurriaan Hage Utrecht University | ||
11:30 30m Talk | 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 | Programming LanguagesPADL at Salle 116, Barre 44-54 | ||
10:30 30m Talk | Improving Non-deterministic Computations in Functional Logic Programs PADL Sergio Antoy Kiel University, Michael Hanus Kiel University | ||
11:00 30m Talk | Canonicalizing High-Level Constructs in Picat PADL Neng-Fa Zhou CUNY Brooklyn College and Graduate Center, Jonathan Fruhman CUNY Brooklyn College | ||
11:30 30m Talk | 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 | BuffetCatering at Catering area | ||
12:00 2h Lunch | Lunch Catering | ||
14:00 - 15:30 | Abstract InterpretationVMCAI at Amphitheater 44 | ||
14:00 30m Talk | Complete Abstractions and Subclassical Modal Logics VMCAI Vijay D'Silva Google, Marcelo Sousa University of Oxford | ||
14:30 30m Talk | Structuring Abstract Interpreters through State and Value Abstractions VMCAI David Bühler CEA LIST, Boris Yakobowski CEA - LIST, Sandrine Blazy University of Rennes 1, France | ||
15:00 30m Talk | 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 | ||
14:00 - 15:30 | Homotopy type theoryCPP at Auditorium | ||
14:00 30m Talk | 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 | ||
14:30 30m Talk | Lifting proof-relevant unification to higher dimensions CPP Jesper Cockx iMinds, Belgium, Dominique Devriese iMinds - Distrinet, KU Leuven | ||
15:00 30m Talk | The Next 700 Syntactical models of type theory CPP Simon Boulier , Pierre-Marie Pédrot , Nicolas Tabareau Inria, France | ||
14:00 - 15:30 | Session 3 PPS at Salle 105, Barre 44-54 | ||
14:00 20m Talk | Commutativity logic for probabilistic trace equivalence: complete or not? PPS Paul Blain Levy , Nathan Bowler Universität Hamburg | ||
14:20 10m Meeting | Discussion 4 PPS | ||
14:30 20m Talk | 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 10m Meeting | Discussion 5 PPS | ||
15:00 20m Talk | A weakest pre-expectation semantics for mixed-sign expectations PPS Benjamin Lucien Kaminski RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University | ||
15:20 10m Meeting | Discussion 6 PPS | ||
14:00 - 15:30 | Session IIIPLMW at Salle 107, Barre 44-54 | ||
14:00 60m Talk | 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 30m Talk | How to Give Talks That People Can Follow PLMW Derek Dreyer MPI-SWS | ||
14:00 - 15:30 | Tutorial: Partial Evaluation for Language ImplementationPEPM at Salle 109, Barre 44-54 | ||
14:00 90m Talk | Practical Partial Evaluation for Language Implementation with Graal & Truffle PEPM | ||
15:30 - 16:00 | Coffee breakCatering at Auditorium Hall | ||
15:30 30m Coffee break | Break Catering | ||
16:00 - 17:30 | Concurrency 2VMCAI at Amphitheater 44 | ||
16:00 30m Talk | 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 30m Talk | 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 30m Talk | Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions VMCAI Raphaël Monat Ecole Normale Supérieure de Lyon, Antoine Miné UPMC, France | ||
16:00 - 17:30 | Formal verification of programming language foundationsCPP at Auditorium | ||
16:00 30m Talk | 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 30m Talk | Formally verified differential dynamic logic CPP | ||
17:00 30m Talk | Equivalence of System F and λ2 in Coq based on context morphism lemmas CPP Jonas Kaiser , Tobias Tebbi , Gert Smolka Saarland University | ||
16:00 - 18:00 | Session IVPLMW at Salle 107, Barre 44-54 | ||
16:00 30m Talk | Machine Learning and Programming Languages: latest directions and research opportunities PLMW Martin Vechev ETH Zurich | ||
16:30 30m Talk | The Curse of Knowledge PLMW Benjamin C. Pierce University of Pennsylvania | ||
17:00 60m Talk | Young Researcher Panel Session PLMW Roopsha Samanta Purdue University, Nada Amin EPFL, Jonathan Protzenko Microsoft Research, Zachary Kincaid Princeton University | ||
16:00 - 17:00 | Transformation (part II)PEPM at Salle 109, Barre 44-54 | ||
16:00 30m Talk | Functional Parallels of Sequential Imperatives PEPM Tiark Rompf Purdue University, Kevin J. Brown Stanford University | ||
16:30 30m Talk | A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction PEPM Kazutaka Matsuda , Kazuyuki Asada University of Tokyo | ||
16:30 - 18:00 | Session 5 PPS at Salle 105, Barre 44-54 | ||
16:30 20m Talk | An exponential family basis for probabilistic programming PPS Chad Scherrer Galois, Inc. | ||
16:50 10m Meeting | Discussion 7 PPS | ||
17:00 20m Talk | 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 10m Meeting | Discussion 8 PPS | ||
17:30 20m Talk | 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 10m Meeting | Discussion 9 PPS | ||
18:15 - 19:15 | Session 6 PPS at Salle 105, Barre 44-54 | ||
18:15 20m Talk | Reducing probabilistic choice to nondeterministic choice PPS Ernie Cohen Amazon Web Services | ||
18:35 10m Meeting | Discussion 10 PPS | ||
18:45 20m Talk | 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 10m Meeting | Discussion 11 PPS | ||
09:00 - 09:05 | OpeningPOPL at Auditorium | ||
09:00 5m Day opening | Opening POPL | ||
09:05 - 10:00 | Invited speakerPOPL at Auditorium | ||
09:05 55m Talk | The Influence of Dependent Types POPL Stephanie Weirich University of Pennsylvania | ||
10:00 - 10:30 | Coffee breakCatering at Auditorium Hall | ||
10:00 30m Coffee break | Break Catering | ||
10:30 - 12:10 | Abstract InterpretationPOPL at Amphitheater 44 | ||
10:30 25m Talk | Ogre and Pythia, An invariance proof method for weak consistency models POPL Jade Alglave University College London, Patrick Cousot New York University | ||
10:55 25m Talk | 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 25m Talk | 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 25m Talk | Fast Polyhedra Abstract Domain POPL Gagandeep Singh ETH Zurich, Switzerland, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich | ||
10:30 - 12:10 | Type Systems 1POPL at Auditorium | ||
10:30 25m Talk | Polymorphism, subtyping and type inference in MLsub POPL Stephen Dolan , Alan Mycroft University of Cambridge | ||
10:55 25m Talk | Java generics are Turing complete POPL Radu Grigore University of Kent | ||
11:20 25m Talk | 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 25m Talk | Modules, Abstraction, and Parametric Polymorphism POPL Karl Crary Carnegie Mellon University | ||
12:10 - 14:20 | BuffetCatering at Catering area | ||
12:10 2h10m Lunch | Lunch Catering | ||
14:20 - 16:00 | Probabilistic ProgrammingPOPL at Amphitheater 44 | ||
14:20 25m Talk | 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 | ||
14:45 25m Talk | Exact Bayesian Inference by Symbolic Disintegration POPL Chung-chieh Shan Indiana University, USA, Norman Ramsey | ||
15:10 25m Talk | Stochastic Invariants for Probabilistic Termination POPL Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria, Djordje Zikelic University of Cambridge | ||
15:35 25m Talk | Coupling proofs are probabilistic product programs POPL Gilles Barthe IMDEA, Benjamin Gregoire INRIA, Justin Hsu , Pierre-Yves Strub École Polytechnique | ||
16:00 - 16:30 | Coffee breakCatering at Auditorium Hall | ||
16:00 30m Coffee break | Break Catering | ||
16:30 - 17:45 | LogicPOPL at Amphitheater 44 | ||
16:30 25m Talk | Monadic second-order logic on finite sequences POPL Loris D'Antoni University of Wisconsin–Madison, Margus Veanes Microsoft Research | ||
16:55 25m Talk | 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 25m Talk | 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 | Compiler OptimisationPOPL at Auditorium | ||
16:30 25m Talk | A Program Optimization for Automatic Database Result Caching POPL Ziv Scully Carnegie Mellon University, Adam Chlipala MIT | ||
16:55 25m Talk | Stream Fusion, to Completeness POPL Oleg Kiselyov , Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens | ||
17:20 25m Talk | 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 | ||
19:30 - 23:00 | Social dinnerCatering at Musée des Arts Forains | ||
19:30 3h30m Dinner | Social dinner Catering | ||
09:00 - 09:15 | ACM and SIGPLAN AwardsPOPL at Auditorium | ||
09:00 5m Awards | Turing Award Video POPL | ||
09:05 5m Awards | Most Influential Paper Award POPL | ||
09:10 5m Awards | Reynolds Doctoral Dissertation Award POPL | ||
09:15 - 10:00 | Invited speakerPOPL at Auditorium | ||
09:15 45m Talk | 40 Years of Abstract Interpretation — An Interview with Patrick Cousot POPL Patrick Cousot New York University, Roberto Giacobazzi University of Verona, Italy | ||
10:00 - 10:30 | Coffee breakCatering at Auditorium Hall | ||
10:00 30m Coffee break | Break Catering | ||
10:30 - 12:10 | Program AnalysisPOPL at Amphitheater 44 | ||
10:30 25m Talk | 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 25m Talk | Contract-based Resource Verification for Higher-order Functions with Memoization POPL Ravichandhran Madhavan EPFL, Sumith Kulal IIT Bombay, Viktor Kunčak EPFL, Switzerland | ||
11:20 25m Talk | Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability POPL Qirun Zhang University of California, Davis, Zhendong Su University of California, Davis | ||
11:45 25m Talk | 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 | ||
10:30 25m Talk | Deciding equivalence with sums and the empty type POPL Gabriel Scherer Northeastern University | ||
10:55 25m Talk | The exp-log normal form of types: Decomposing extensional equality and representing terms compactly POPL Danko Ilik Trusted Labs | ||
11:20 25m Talk | Contextual isomorphisms POPL | ||
11:45 25m Talk | Typed Self-Evaluation via Intensional Type Functions POPL Matt Brown UCLA, Jens Palsberg University of California, Los Angeles | ||
12:10 - 14:20 | BuffetCatering at Catering area | ||
12:10 2h10m Lunch | Lunch Catering | ||
14:20 - 16:00 | Concurrency 2POPL at Amphitheater 44 | ||
14:20 25m Talk | 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 25m Talk | Dynamic Race Detection For C++11 POPL Christopher Lidbury Imperial College London, Alastair F. Donaldson Imperial College London | ||
15:10 25m Talk | 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 | ||
15:35 25m Talk | 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 | Functional Programming with EffectsPOPL at Auditorium | ||
14:20 25m Talk | Type Directed Compilation of Row-Typed Algebraic Effects POPL Daan Leijen Microsoft Research | ||
14:45 25m Talk | Do be do be do POPL Sam Lindley University of Edinburgh, Conor McBride , Craig McLaughlin The University of Edinburgh | ||
15:10 25m Talk | 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 | ||
15:35 25m Talk | Stateful Manifest Contracts POPL Taro Sekiyama , Atsushi Igarashi Kyoto University | ||
16:00 - 16:30 | Coffee breakCatering at Auditorium Hall | ||
16:00 30m Coffee break | Break Catering | ||
16:30 - 17:20 | Semantic FoundationsPOPL at Amphitheater 44 | ||
16:30 25m Talk | 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 25m Talk | 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 | ||
16:30 - 17:20 | Logic and ProgrammingPOPL at Auditorium | ||
16:30 25m Talk | 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 25m Talk | LOIS: syntax and semantics POPL | ||
17:20 - 18:20 | Business meetingPOPL at Auditorium | ||
17:20 20m Talk | PC Chair report POPL Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
17:40 10m Talk | POPL 2018 presentation POPL Andrew Myers Cornell University, Ranjit Jhala University of California, San Diego | ||
17:50 30m Meeting | SIGPLAN business meeting POPL C: Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
18:20 - 20:20 | Poster SessionStudent Research Competition at Auditorium Hall | ||
18:20 10m Demonstration | Naturality despite Nontermination: A Logical Relation for Linear Types and Polymorphism Student Research Competition Nicholas Rioux Northeastern University | ||
18:30 10m Demonstration | Gradual Type Precision as Retraction Student Research Competition Max S. New Northeastern University | ||
18:40 10m Demonstration | Linking Types: Specifying Safe Interoperability and Equivalences Student Research Competition Daniel Patterson Northeastern University | ||
18:50 10m Demonstration | A Monadic Framework for Bidirectional Programming Student Research Competition Li-yao Xia ENS Paris | ||
19:00 10m Demonstration | Gradual Set-Theoretic Types Student Research Competition Victor Lanvin ENS Paris-Saclay | ||
19:10 10m Demonstration | Abstract Interpretation of High-Level Transformations Student Research Competition Ahmad Salim Al-Sibahi IT University of Copenhagen, Denmark | ||
19:20 10m Demonstration | FairSquare: A Static Analysis Tool for Algorithmic Fairness Student Research Competition Samuel Drews University of Wisconsin-Madison | ||
19:30 10m Demonstration | Toward Type-Preserving Compilation of Coq Student Research Competition William J. Bowman Northeastern University | ||
19:40 10m Demonstration | A Symbolic Execution Framework for Haskell Student Research Competition Anton Xue Yale University | ||
19:50 10m Demonstration | Synthesizing Imperative Programs from Examples for Introductory Programming Assignments Student Research Competition Sunbeom So Korea University | ||
20:00 10m Demonstration | Provenance for Configuration Language Security Student Research Competition Weili Fu University of Edinburgh | ||
20:10 10m Demonstration | A gradually typed polymorphic lambda calculus Student Research Competition Yuu Igarashi Kyoto University | ||
09:00 - 09:05 | Student Competition AwardStudent Research Competition at Auditorium | ||
09:00 5m Awards | Student Competition Award Student Research Competition | ||
09:05 - 10:00 | Invited speakerPOPL at Auditorium | ||
09:05 55m Talk | Rust: from POPL to practice POPL Aaron Turon MPI-SWS | ||
10:00 - 10:30 | Coffee breakCatering at Auditorium Hall | ||
10:00 30m Coffee break | Break Catering | ||
10:30 - 12:10 | Verification and SynthesisPOPL at Amphitheater 44 | ||
10:30 25m Talk | 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 25m Talk | 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 25m Talk | 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 25m Talk | 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 | Type Systems 3POPL at Auditorium | ||
10:30 25m Talk | Intersection Type Calculi of Bounded Dimension POPL Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund | ||
10:55 25m Talk | Type Soundness Proofs with Definitional Interpreters POPL Nada Amin EPFL, Tiark Rompf Purdue University | ||
11:20 25m Talk | Computational Higher-Dimensional Type Theory POPL Carlo Angiuli Carnegie Mellon University, Robert Harper , Todd Wilson California State University Fresno | ||
11:45 25m Talk | Type Systems as Macros POPL Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University | ||
12:10 - 14:20 | BuffetCatering at Catering area | ||
12:10 2h10m Lunch | Lunch Catering | ||
14:20 - 16:00 | Concurrency 3POPL at Amphitheater 44 | ||
14:20 25m Talk | Parallel Functional Arrays POPL Ananya Kumar , Guy E. Blelloch Carnegie Mellon University, Robert Harper | ||
14:45 25m Talk | A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms POPL Igor Konnov TU Wien, Marijana Lazić TU Wien, Helmut Veith TU Wien, Josef Widder TU Wien | ||
15:10 25m Talk | 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 25m Talk | 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 | ||
14:20 - 16:00 | Gradual Typing and ContractsPOPL at Auditorium | ||
14:20 25m Talk | Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System POPL Michael Vitousek , Cameron Swords Indiana University, Jeremy G. Siek Indiana University Bloomington | ||
14:45 25m Talk | Gradual Refinement Types POPL Nico Lehmann , Éric Tanter University of Chile, Chile | ||
15:10 25m Talk | Automatically Generating the Dynamic Semantics of Gradually Typed Languages POPL Matteo Cimini Indiana University, USA, Jeremy G. Siek Indiana University Bloomington | ||
15:35 25m Talk | Sums of Uncertainty: Refinements go gradual POPL Khurram A. Jafery University of British Columbia, Jana Dunfield University of British Columbia | ||
16:00 - 16:30 | Coffee breakCatering at Auditorium Hall | ||
16:00 30m Coffee break | Break Catering | ||
16:30 - 17:45 | QuantumPOPL at Amphitheater 44 | ||
16:30 25m Talk | 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 25m Talk | 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 25m Talk | QWIRE: A Core Language for Quantum Circuits POPL Jennifer Paykin , Robert Rand University of Pennsylvania, Steve Zdancewic University of Pennsylvania | ||
16:30 - 17:45 | Security and PrivacyPOPL at Auditorium | ||
16:30 25m Talk | LMS-Verify: Abstraction Without Regret for Verified Systems Programming POPL Nada Amin EPFL, Tiark Rompf Purdue University | ||
16:55 25m Talk | 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 25m Talk | LightDP: Towards Automating Differential Privacy Proofs POPL Danfeng Zhang Pennsylvania State University, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University | ||
08:45 - 09:00 | OpeningN40AI at Amphitheater 44 | ||
08:45 15m Day opening | Opening N40AI | ||
08:55 - 09:00 | WelcomePiP at Salle 105, Barre 44-54 | ||
08:55 5m Talk | Welcome PiP | ||
09:00 - 10:00 | Industrial Panel 1N40AI at Amphitheater 44 | ||
09:00 30m Talk | Abstract Interpretation in Absint N40AI Christian Ferdinand AbsInt | ||
09:30 30m Talk | Abstract Interpretation in Facebook N40AI Francesco Logozzo Facebook | ||
09:00 - 10:00 | Opening SessionCoqPL at Auditorium | ||
09:00 60m Talk | Invited Talk -- Demonstration of the Iris separation logic in Coq CoqPL I: Robbert Krebbers Delft University of Technology, Netherlands | ||
09:00 - 10:00 | Session 1PiP at Salle 105, Barre 44-54 | ||
09:00 30m Talk | Andrew Kennedy (Facebook) Static type checking for PHP PiP | ||
09:30 30m Talk | Jean-Louis Colaco (Ansys - Esterel Technologies) A brief history of the Scade language PiP | ||
09:00 - 10:00 | Session IRDP at Salle 107, Barre 44-54 | ||
09:00 15m Talk | Welcome RDP Nate Foster Cornell University, Mooly Sagiv Tel Aviv University, Victor Vianu UC San Diego | ||
09:15 45m Talk | Automatic Verification of Database-Centric Workflows RDP | ||
09:00 - 10:00 | Session OneOff the Beaten Track at Salle 109, Barre 44-54 | ||
09:00 60m Talk | 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 | Coffee breakCatering at Auditorium Hall | ||
10:00 30m Coffee break | Break Catering | ||
10:30 - 12:00 | Industrial Panel 2 & Systems BiologyN40AI at Amphitheater 44 | ||
10:30 30m Talk | Abstract Interpretation in Amazon N40AI Byron Cook Amazon | ||
11:00 30m Talk | Abstract Interpretation at Galois N40AI Aaron Tomb Galois, Inc. | ||
11:30 30m Talk | Systems biology N40AI Vincent Danos ENS Paris/CNRS | ||
10:30 - 12:10 | Morning SessionCoqPL at Auditorium | ||
10:30 25m Talk | IxFree: Step-Indexed Logical Relations in Coq CoqPL File Attached | ||
10:55 25m Talk | Logical Relations in Iris CoqPL Amin Timany imec - Distrinet, KU Leuven, Robbert Krebbers Delft University of Technology, Netherlands, Lars Birkedal Aarhus University | ||
11:20 25m Talk | Predicate Monads: A Framework for Proving Generic Properties of Monadic Programs via Rewriting CoqPL Edwin Westbrook Galois, Inc., Gregory Malecha UCSD | ||
11:45 25m Talk | ppsimpl: a reflexive Coq tactic for canonising goals CoqPL File Attached | ||
10:30 - 12:00 | Session IIRDP at Salle 107, Barre 44-54 | ||
10:30 30m Talk | Verification Challenges in Applications of Blockchain for Business Collaboration RDP Takaaki Tateishi IBM Research - Tokyo | ||
11:00 30m Talk | Fiat: A New Take on Domain-Specific Languages by Programming with Specifications RDP Adam Chlipala MIT | ||
11:30 30m Talk | Parallel-Correctness and Transferability for Conjunctive Queries RDP | ||
10:30 - 12:10 | Session TwoOff the Beaten Track at Salle 109, Barre 44-54 | ||
10:30 25m Talk | Can we machine-learn programming language semantics? Off the Beaten Track Dan Ghica University of Birmingham, Khulood Alyahya , Victor Patentasu | ||
10:55 25m Talk | How Far Apart Should Those Programs Be? Off the Beaten Track Ugo Dal Lago University of Bologna, France | ||
11:20 25m Talk | Programming Quantum Annealers Off the Beaten Track File Attached | ||
11:45 25m Talk | Understanding the POSIX Shell as a Programming Language Off the Beaten Track Michael Greenberg Pomona College | ||
12:00 - 14:00 | BuffetCatering at Catering area | ||
12:00 2h Lunch | Lunch Catering | ||
14:00 - 15:30 | Security, Big Code and Synthesis N40AI at Amphitheater 44 | ||
14:00 30m Talk | Security N40AI Michael Hicks University of Maryland at College Park, USA | ||
14:30 30m Talk | Big Code N40AI Bor-Yuh Evan Chang University of Colorado Boulder | ||
15:00 30m Talk | Program synthesis N40AI Eran Yahav Technion | ||
14:00 - 15:30 | Midday SessionCoqPL at Auditorium | ||
14:00 60m Talk | Invited Talk -- Managing Logical and Computational Complexity using Program Transformations CoqPL I: Nicolas Tabareau Inria, France | ||
15:00 30m Demonstration | Session with the Coq Development Team CoqPL Matthieu Sozeau Inria | ||
14:00 - 15:30 | Session 3PiP at Salle 105, Barre 44-54 | ||
14:00 30m Talk | John Hughes (Quviq/Chalmers) Properties in practice: lessons from ten years of QuickCheck PiP | ||
14:30 30m Talk | Byron Cook (Amazon) Automated Reasoning about AWS PiP | ||
15:00 30m Talk | Steve Zdancewic (U.Penn) Vellvm2: Semantics and Verification for LLVM PiP | ||
14:00 - 15:30 | Session IIIRDP at Salle 107, Barre 44-54 | ||
14:00 45m Talk | Synthesizing Data-parallel Programs RDP Aws Albarghouthi University of Wisconsin - Madison | ||
14:45 45m Talk | Cosette: A Solver for SQL Equivalences RDP Alvin Cheung University of Washington | ||
14:00 - 15:25 | Session ThreeOff the Beaten Track at Salle 109, Barre 44-54 | ||
14:00 60m Talk | Keynote talk: Varieties of Programming Experience Off the Beaten Track Alan Blackwell University of Cambridge | ||
15:00 25m Talk | Bootstrapping the next generation of mathematical social machines Off the Beaten Track File Attached | ||
15:30 - 16:00 | Coffee breakCatering at Auditorium Hall | ||
15:30 30m Coffee break | Break Catering | ||
16:00 - 18:30 | System Verification and Patrick Cousot's KeynoteN40AI at Amphitheater 44 | ||
16:00 30m Talk | System verification N40AI Arie Gurfinkel University of Waterloo | ||
16:30 75m Talk | Keynote: the Next 40 years of Abstract Interpretation N40AI Patrick Cousot New York University | ||
17:45 45m Social Event | Concrete Cheese and Wine N40AI | ||
16:00 - 18:00 | Session 4PiP at Salle 105, Barre 44-54 | ||
16:00 30m Talk | Christopher Pulte/Kathryn Gray (Cambridge) REMS machine models PiP | ||
16:30 60m Talk | Discussion: Methods and Tools for large-scale semantics PiP | ||
16:00 - 18:00 | Session IVRDP at Salle 107, Barre 44-54 | ||
16:00 30m Talk | Building performance-sensitive systems in high-level languages RDP | ||
16:30 30m Talk | Programming Language Ideas Escape the Lab: Declarative Data Description Languages for Managing Ad hoc Data RDP Kathleen Fisher Tufts University | ||
17:00 30m Talk | Computation with Atoms RDP | ||
17:30 30m Talk | Discussion RDP Nate Foster Cornell University, Victor Vianu UC San Diego, Mooly Sagiv Tel Aviv University | ||
16:00 - 18:05 | Session FourOff the Beaten Track at Salle 109, Barre 44-54 | ||
16:00 25m Talk | 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 | ||
16:25 25m Talk | Laziness Boxes You In Off the Beaten Track Jose Calderon Galois, Inc., Stephen Magill | ||
16:50 25m Talk | Programming with Epistemic Logic Off the Beaten Track Markus Eger , Chris Martens Carnegie Mellon University | ||
17:15 25m Talk | Preventing False Discoveries in Adaptive Data Analysis: a Programming Language approach Off the Beaten Track Marco Gaboardi SUNY Buffalo, USA | ||
17:40 25m Talk | Running Incomplete Programs Off the Beaten Track Ian Voysey Carnegie Mellon University, Cyrus Omar Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder | ||
19:00 - 21:00 | Social EventCoqPL at CoqPL-social-event-room | ||
19:00 2h Social Event | CoqPL Social Event CoqPL | ||
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