Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 17 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Sun 17 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
08:50 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | Automating Abstract Interpretation VMCAI Thomas Reps University of Wisconsin - Madison and Grammatech Inc. | ||
10:30 - 12:00 | |||
10:30 30mTalk | An Abstract Domain of Uninterpreted Functions VMCAI | ||
11:00 30mTalk | Predicate Abstraction for Linked Data Structures VMCAI | ||
11:30 30mTalk | Property Directed Abstract Interpretation VMCAI | ||
14:00 - 15:30 | |||
14:00 30mTalk | Program Analysis with Local Policy Iteration VMCAI | ||
14:30 30mTalk | Lazy Constrained Monotonic Abstraction VMCAI | ||
15:00 30mTalk | Polyhedral Approximation of Multivariate Polynomials using Handelman’s Theorem VMCAI | ||
16:00 - 17:00 | |||
16:00 30mTalk | D3 : Data-Driven Disjunctive Abstraction VMCAI | ||
16:30 30mTalk | Exact Heap Summaries for Symbolic Execution VMCAI | ||
Mon 18 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Mon 18 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
08:30 - 10:00 | |||
08:30 45mTalk | Invited Talk: Learning from Big Code: Probabilistic Models, Program Analysis and Synthesis PEPM Invited Talks | ||
09:15 45mTalk | Invited Talk: Tracing JITs for Functional Languages PEPM Invited Talks | ||
08:30 - 10:00 | |||
08:30 90mTalk | T1: An Introduction to Redex with Abstracting Abstract Machines Tutorials David Van Horn University of Maryland, College Park Link to publication | ||
08:30 - 10:00 | |||
08:30 90mTalk | T3: Syntax-Guided Synthesis (SyGuS) Tutorials Rajeev Alur University of Pennsylvania, Dana Fisman University of Pennsylvania, Rishabh Singh Microsoft Research, Armando Solar-Lezama MIT Link to publication | ||
08:30 - 10:00 | |||
08:30 90mTalk | T5: Higher-Order Model Checking Tutorials | ||
08:45 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | Program Synthesis for Direct Manipulation Interfaces PADL Ravi Chugh University of Chicago | ||
09:00 - 10:00 | |||
09:00 60mTalk | Ironclad - Full Verification of Complex Systems VMCAI Bryan Parno Microsoft Research | ||
09:00 - 10:00 | |||
09:00 60mTalk | Perspectives on Formal Verfication CPP Harvey Friedman Ohio State University | ||
10:30 - 12:00 | |||
10:30 30mTalk | Simplifying Probabilistic Programs Using Computer Algebra PADL | ||
11:00 30mTalk | Haskino: A Remote Monad for Programming the Arduino PADL | ||
11:30 30mTalk | From Monads to Effects and Back PADL | ||
10:30 - 12:00 | |||
10:30 45mTalk | Invited Talk: Using Formal Methods to Eliminate Exploitable Bugs PEPM Invited Talks | ||
11:15 45mTalk | Invited Talk: Automated Reasoning about Type Systems by Compilation to First-Order Logic PEPM Invited Talks | ||
10:30 - 12:00 | |||
10:30 90mTalk | T2: Declare Your Language (Part 1): Hands-On Spoofax Tutorial Tutorials Eelco Visser Delft University of Technology | ||
10:30 - 12:00 | |||
10:30 90mTalk | T3: Syntax-Guided Synthesis (SyGuS) (Advanced Material) Tutorials Rajeev Alur University of Pennsylvania, Dana Fisman University of Pennsylvania, Rishabh Singh Microsoft Research, Armando Solar-Lezama MIT Link to publication | ||
10:30 - 12:00 | |||
10:30 90mTalk | T4: Programs and Proofs in the Coq Proof Assistant Tutorials Link to publication | ||
10:30 - 12:00 | |||
10:30 90mTalk | T6: Security and Privacy by Typing in Cryptographic Systems Tutorials Matteo Maffei Saarland University | ||
10:30 - 12:00 | |||
10:30 30mTalk | Abstract Interpretation with Infinitesimals VMCAI | ||
11:00 30mTalk | Lipschitz Robustness of Timed I/O Systems VMCAI | ||
11:30 30mTalk | A method for invariant generation for polynomial continuous systems VMCAI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Higher-order Representation Predicates in Separation Logic CPP | ||
11:00 30mTalk | A Unified Coq Framework for Verifying C Programs with Floating-Point Computations CPP | ||
11:30 30mTalk | Refinement Based Verification of Imperative Data Structures CPP Peter Lammich Technische Universität München | ||
14:00 - 15:30 | |||
14:00 30mTalk | A GPU implementation of the ASP computation PADL Agostino Dovier University of Udine, Andrea Formisano Università di Perugia , Enrico Pontelli New Mexico State University, Flavio Vella Sapienza University of Rome, Italy | ||
14:30 30mTalk | Using Constraint Logic Programming to Schedule Solar Array Operations on the International Space Station PADL | ||
15:00 30mTalk | The Picat-SAT Compiler PADL Neng-Fa Zhou CUNY Brooklyn College and Graduate Center, Håkan Kjellerstrand CUNY Brooklyn College and Graduate Center | ||
14:00 - 15:30 | |||
14:00 45mTalk | Invited Talk: Program Synthesis: Opportunities for the next Decade PEPM Invited Talks | ||
14:45 45mTalk | Invited Talk: LMS: a Perspective on Generative Programming PEPM Invited Talks | ||
14:00 - 15:30 | |||
14:00 90mTalk | T1: An Introduction to Redex with Abstracting Abstract Machines(Advanced Material) Tutorials David Van Horn University of Maryland, College Park Link to publication | ||
14:00 - 15:30 | |||
14:00 90mTalk | T7: Trace-based Synchronization Synthesis for Concurrent Programs Tutorials | ||
14:00 - 15:30 | |||
14:00 90mTalk | T4: Programs and Proofs in the Coq Proof Assistant (Advanced Material) Tutorials Link to publication | ||
14:00 - 15:30 | |||
14:00 90mTalk | T6: Security and Privacy by Typing in Cryptographic Systems Tutorials Matteo Maffei Saarland University | ||
14:00 - 15:30 | Dynamic and Static VerificationVMCAI at Room St Petersburg I Chair(s): Aarti Gupta Princeton University | ||
14:00 30mTalk | Hybrid Analysis for Partial Order Reduction of Programs with Arrays VMCAI Pavel Parizek Charles University in Prague | ||
14:30 30mTalk | Cloud-Based Verification of Concurrent Software VMCAI | ||
15:00 30mTalk | Abstraction-driven Concolic Testing VMCAI | ||
14:00 - 15:30 | |||
14:00 30mTalk | The Vampire and the FOOL CPP Evgenii Kotelnikov Chalmers University of Technology, Laura Kovacs Chalmers University of Technology, Giles Reger University of Manchester, Andrei Voronkov University of Manchester | ||
14:30 30mTalk | Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP Lukasz Czajka University of Innsbruck | ||
15:00 30mTalk | Mizar Environment for Isabelle CPP Cezary Kaliszyk University of Innsbruck, Karol Pąk University of Bialystok, Institute of Computer Science, Josef Urban | ||
16:00 - 17:00 | |||
16:00 30mTalk | The KB paradigm and its application to interactive configuration PADL Pieter Van Hertum KU Leuven, Ingmar Dasseville KU Leuven, Gerda Janssens KU Leuven, Marc Denecker KU Leuven | ||
16:30 30mTalk | Default Rules for Curry PADL | ||
16:00 - 17:30 | |||
16:00 45mTalk | Invited Talk: Fiat: Extensible Code Generation with Proofs PEPM Invited Talks | ||
16:45 45mTalk | Invited Talk: The Promise of Relational Programming PEPM Invited Talks | ||
16:00 - 17:30 | |||
16:00 90mTalk | T2: Declare Your Language (Part 2): Name Binding with Scope Graphs Tutorials Eelco Visser Delft University of Technology Link to publication DOI Media Attached | ||
16:00 - 17:30 | |||
16:00 90mTalk | T7: Trace-based Synchronization Synthesis for Concurrent Programs Tutorials | ||
16:00 - 17:30 | |||
16:00 90mTalk | T5: Higher-Order Model Checking Tutorials | ||
16:00 - 17:00 | |||
16:00 30mTalk | Reward-Bounded Reachability Probability for Uncertain Weighted MDPs VMCAI | ||
16:30 30mTalk | Parameter Synthesis for Parametric Interval Markov Chains VMCAI | ||
16:00 - 18:00 | |||
16:00 30mTalk | A Modular, Efficient Formalisation of Real Algebraic Numbers CPP | ||
16:30 30mTalk | Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials CPP Sophie Bernard INRIA, Yves Bertot INRIA, Laurence Rideau INRIA, Pierre-Yves Strub IMDEA Software Institute | ||
17:00 30mTalk | Formalizing Jordan Normal Forms in Isabelle/HOL CPP | ||
17:30 30mTalk | Formalization of a Newton series representation of polynomials CPP | ||
Tue 19 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Tue 19 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
08:50 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | Invited Keynote: Building Languages in Racket: Syntax Objects as an Intermediate Representation PEPM Invited Talks | ||
09:00 - 10:00 | Invited Talk IIIVMCAI at Room St Petersburg I Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder | ||
09:00 60mTalk | Viper - A Verification Infrastructure for Permission-based Reasoning VMCAI Peter Müller ETH Zurich | ||
09:00 - 10:00 | |||
09:00 60mTalk | Dependent Type Practice CPP Leonardo de Moura Microsoft Research, Redmond | ||
09:00 - 10:00 | |||
09:00 30mTalk | Grad School: A Survival Guide PLMW Matthew Might University of Utah, USA Media Attached | ||
09:30 30mTalk | Theorem Provers are a PL Researcher's Best Friend PLMW Xavier Leroy Inria Media Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Computing with Catalan Families, Generically PADL Paul Tarau University of North Texas | ||
11:00 30mTalk | A Size-proportionate Bijective Encoding of Lambda Terms as Catalan Objects endowed with Arithmetic Operations PADL Paul Tarau University of North Texas | ||
11:30 30mTalk | Generic Matching of Tree Regular Expressions over Haskell Data Types PADL | ||
10:30 - 12:00 | Parsing & Domain-Specific Languages IPEPM at Room Harbor View Chair(s): Kenichi Asai Ochanomizu University | ||
10:30 30mTalk | Practical, General Parser Combinators PEPM Anastasia Izmaylova Centrum Wiskunde & Informatica, Ali Afroozeh Centrum Wiskunde & Informatica, Tijs van der Storm CWI DOI Pre-print | ||
11:00 30mTalk | Operator Precedence for Data-Dependent Grammars PEPM DOI Pre-print | ||
11:30 30mTalk | Everything Old Is New Again: Quoted Domain-Specific Languages PEPM Shayan Najd , Sam Lindley University of Edinburgh, Josef Svenningsson Chalmers University of Technology, Sweden, Philip Wadler University of Edinburgh DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Pointer Race Freedom VMCAI Frédéric Haziza , Lukáš Holík , Roland Meyer , Sebastian Wolff Fraunhofer ITWM and TU Kaiserslautern | ||
11:00 30mTalk | A program logic for C11 memory fences VMCAI | ||
11:30 30mTalk | From Low Level Pointers to High Level Containers VMCAI | ||
10:30 - 12:00 | |||
10:30 30mTalk | A Logic of Proofs for Differential Dynamic Logic CPP | ||
11:00 30mTalk | Constructing the Propositional Truncation using Non-recursive HITs CPP Floris van Doorn Carnegie Mellon University | ||
11:30 30mTalk | A Nominal Exploration of Intuitionism CPP | ||
10:30 - 12:00 | |||
10:30 30mTalk | Academia or Industry? PLMW Aarti Gupta Princeton University Media Attached | ||
11:00 30mTalk | Refining Types with SMT PLMW Ranjit Jhala University of California, San Diego Media Attached | ||
11:30 30mTalk | How to Write Papers So People Can Read Them PLMW Derek Dreyer MPI-SWS Media Attached | ||
14:00 - 15:30 | Domain-Specific Languages IIPEPM at Room Harbor View Chair(s): Sebastian Erdweg TU Darmstadt, Germany | ||
14:00 30mTalk | BiGUL: A Formally Verified Core Language for Putback-Based Bidirectional Programming PEPM Hsiang-Shang ‘Josh’ Ko National Institute of Informatics, Tao Zan Sokendai, Japan, Zhenjiang Hu National Institute of Informatics DOI Pre-print | ||
14:30 30mTalk | A Constraint Language for Static Semantic Analysis Based on Scope Graphs PEPM Hendrik van Antwerpen Delft University of Technology, Netherlands, Pierre Neron TU Delft, Andrew Tolmach Portland State University, Eelco Visser Delft University of Technology, Guido Wachsmuth Delft University of Technology Link to publication DOI Pre-print | ||
15:00 30mTalk | Finally, Safely-Extensible and Efficient Language-Integrated Query PEPM DOI | ||
14:00 - 15:30 | Parameterized and Component-Based SystemsVMCAI at Room St Petersburg I Chair(s): Arie Gurfinkel Carnegie Mellon University | ||
14:00 30mTalk | Regular Symmetry Patterns VMCAI Anthony Widjaja Lin Yale-NUS College, Singapore, Truong Khanh Nguyen , Philipp Ruemmer Uppsala University, Jun Sun | ||
14:30 30mTalk | Tight Cutoffs for Guarded Protocols with Fairness VMCAI | ||
15:00 30mTalk | A General Modular Synthesis Problem for Pushdown Systems VMCAI | ||
14:00 - 15:30 | |||
14:00 30mTalk | Bisimulation Up-to Techniques for Psi-calculi CPP | ||
14:30 30mTalk | Planning for Change in a Formal Verification of the Raft Consensus Protocol CPP Doug Woos University of Washington, James R. Wilcox University of Washington, Steve Anton University of Washington, Zachary Tatlock University of Washington, Seattle, Michael D. Ernst University of Washington, Thomas Anderson University of Washington Pre-print | ||
15:00 30mTalk | A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules CPP | ||
14:00 - 15:30 | |||
14:00 30mTalk | Student Interaction Activity PLMW | ||
14:30 30mTalk | Automata and Coinduction PLMW Alexandra Silva Radboud University Nijmegen Media Attached | ||
15:00 30mTalk | Unaccustomed As I Am to Public Speaking PLMW John Hughes Chalmers University of Technology Media Attached | ||
16:00 - 17:40 | |||
16:00 30mTalk | Staging Generic Programming PEPM Jeremy Yallop University of Cambridge, UK DOI | ||
16:30 30mTalk | Removing Runtime Overhead for Optimized Object Queries PEPM DOI | ||
17:00 20mTalk | Toward Introducing Binding-Time Analysis to MetaOCaml PEPM Kenichi Asai Ochanomizu University DOI | ||
17:20 20mTalk | Staging beyond Terms: Prospects and Challenges PEPM Jun Inoue National Institute of Advanced Industrial Science and Technology, Japan, Oleg Kiselyov , Yukiyoshi Kameyama DOI | ||
16:00 - 17:00 | |||
16:00 30mTalk | Model Checking with Multi-Threaded IC3 Portfolios VMCAI | ||
16:30 30mTalk | Automatic Generation of Propagation Complete SAT Encodings VMCAI | ||
16:00 - 17:00 | |||
16:00 30mTalk | Formal Verification of Control-flow Graph Flattening CPP | ||
16:30 30mTalk | Axiomatic Semantics for Compiler Verification CPP | ||
16:00 - 17:00 | |||
16:00 30mTalk | Two Notions of Beauty in Programming PLMW Robert Harper Carnegie Mellon University Media Attached | ||
16:30 30mTalk | Highs and Lows of a Language Researcher PLMW Greg Morrisett Cornell University Media Attached | ||
17:00 - 17:45 | |||
17:00 45mTalk | Young Researcher Panel Session, with panelists: Mark Batty (Kent), Mike Carbin (MIT), Lindsey Kuper (Intel), Ilya Sergey (UCL) PLMW Dimitrios Vytiniotis Microsoft Research, Cambridge Media Attached | ||
18:00 - 21:00 | |||
18:00 3hSocial Event | CPP Reception, sponsored by the DeepSpec project CPP | ||
Wed 20 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Wed 20 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | Invited WedInvited Speakers at Grand Bay Ballroom Chair(s): Rastislav Bodik University of Washington, USA | ||
09:00 60mTalk | Programming the World of Uncertain Things Invited Speakers Kathryn S McKinley Microsoft Research | ||
10:30 - 12:10 | Track 1: Algorithmic VerificationResearch Papers at Grand Bay North Chair(s): Arie Gurfinkel Carnegie Mellon University | ||
10:30 25mTalk | Temporal Verification of Higher-order Functional Programs Research Papers Akihiro Murase , Tachio Terauchi JAIST, Naoki Kobayashi University of Tokyo, Ryosuke Sato University of Tokyo, Hiroshi Unno University of Tsukuba | ||
10:55 25mTalk | Scaling Network Verification using Symmetry and Surgery Research Papers Gordon Plotkin , Nikolaj Bjørner Microsoft Research, Nuno P. Lopes Microsoft Research, Andrey Rybalchenko Microsoft Research, George Varghese Microsoft Research Pre-print | ||
11:20 25mTalk | Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates Research Papers | ||
11:45 25mTalk | Reducing Crash Recoverability to Reachability Research Papers | ||
10:30 - 12:10 | Track 2: Types and FoundationsResearch Papers at Grand Bay South Chair(s): Robert Atkey University of Strathclyde | ||
10:30 25mTalk | Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega Research Papers Media Attached File Attached | ||
10:55 25mTalk | Type Theory in Type Theory using Quotient Inductive Types Research Papers Media Attached File Attached | ||
11:20 25mTalk | System Fω with Equirecursive Types for Datatype-generic Programming Research Papers Yufei Cai University of Tübingen, Germany, Paolo G. Giarrusso University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany Media Attached | ||
11:45 25mTalk | A Theory of Effects and Resources: Adjunction Models and Polarised Calculi Research Papers Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo Fiore Computer Laboratory, University of Cambridge, Guillaume Munch-Maccagnoni Computer Laboratory, University of Cambridge | ||
14:20 - 16:00 | Track 1: Decision ProceduresResearch Papers at Grand Bay North Chair(s): Loris D'Antoni University of Pennsylvania | ||
14:20 25mTalk | Query-Guided Maximum Satisfiability Research Papers Xin Zhang Georgia Tech, Ravi Mangal Georgia Institute of Technology, Aditya Nori Microsoft Research, UK, Mayur Naik Georgia Tech File Attached | ||
14:45 25mTalk | String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS Research Papers Media Attached | ||
15:10 25mTalk | Symbolic Computation of Differential Equivalences Research Papers Luca Cardelli Microsoft Research and University of Oxford, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin IMT Institute for Advanced Studies Lucca, Italy Media Attached | ||
15:35 25mTalk | Unboundedness and Downward Closures of Higher-Order Pushdown Automata Research Papers Matthew Hague Royal Holloway University of London, UK, Jonathan Kochems Department of Computer Science, University of Oxford, C.-H. Luke Ong University of Oxford, UK Media Attached | ||
14:20 - 16:00 | Track 2: Correct CompilationResearch Papers at Grand Bay South Chair(s): Jens Palsberg University of California, Los Angeles | ||
14:20 25mTalk | Fully-Abstract Compilation by Approximate Back-Translation Research Papers Dominique Devriese iMinds - Distrinet, KU Leuven, Marco Patrignani KU Leuven, Frank Piessens iMinds - Distrinet, KU Leuven Pre-print Media Attached | ||
14:45 25mTalk | Lightweight Verification of Separate Compilation Research Papers Jeehoon Kang Seoul National University, Yoonseung Kim Seoul National University (South Korea), Chung-Kil Hur Seoul National University, Derek Dreyer MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany Media Attached File Attached | ||
15:10 25mTalk | From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes Research Papers Media Attached | ||
15:35 25mTalk | Sound Type-dependent Syntactic Language Extension Research Papers Pre-print Media Attached File Attached | ||
16:30 - 17:45 | Track 2: Decidability and complexityResearch Papers at Grand Bay South Chair(s): C.-H. Luke Ong University of Oxford, UK | ||
16:30 25mTalk | Decidability of Inferring Inductive Invariants Research Papers Oded Padon Tel Aviv University, Neil Immerman University of Massachusetts, Amherst, Sharon Shoham , Aleksandr Karbyshev Tel Aviv University, Mooly Sagiv Tel Aviv University Media Attached | ||
16:55 25mTalk | The Hardness of Data Packing Research Papers Media Attached | ||
17:20 25mTalk | The Complexity of Interaction Research Papers Media Attached | ||
19:00 - 22:00 | |||
Thu 21 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Thu 21 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | |||
09:00 60mTalk | Synthesis of Reactive Controllers for Hybrid Systems Invited Speakers Richard M. Murray California Institute of Technology Media Attached | ||
10:30 - 12:10 | Track 1: Foundations of distributed systemsResearch Papers at Grand Bay North Chair(s): Mooly Sagiv Tel Aviv University | ||
10:30 25mTalk | Certified Causally Consistent Distributed Key-Value Stores Research Papers Media Attached | ||
10:55 25mTalk | 'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems Research Papers Alexey Gotsman IMDEA, Hongseok Yang University of Oxford, UK, Carla Ferreira Universidade Nova Lisboa, Mahsa Najafzadeh UPMC & INRIA, Marc Shapiro Inria & LIP6 Media Attached | ||
11:20 25mTalk | A Program Logic for Concurrent Objects under Fair Scheduling Research Papers Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China Media Attached | ||
11:45 25mTalk | PSync: a partially synchronous language for fault-tolerant distributed algorithms Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
10:30 - 12:10 | Track 2: Probabilistic and statistical analysisResearch Papers at Grand Bay South Chair(s): Aditya Nori Microsoft Research, UK | ||
10:30 25mTalk | Prophet: Automatic Patch Generation via Learning from Successful Patches Research Papers Media Attached | ||
10:55 25mTalk | Estimating types in binaries using predictive modeling Research Papers Omer Katz Technion, Israel Institute of Technology, Ran El-Yaniv Technion, Israel Institute of Technology, Eran Yahav Technion Media Attached File Attached | ||
11:20 25mTalk | Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs Research Papers Krishnendu Chatterjee IST Austria, Hongfei Fu IST Austria, Rouzbeh Hasheminezhad Sharif University, Petr Novotný IST Austria Media Attached | ||
11:45 25mTalk | Transforming Spreadsheet Data Types using Examples Research Papers Media Attached | ||
14:20 - 16:00 | Track 1: Learning and verificationResearch Papers at Grand Bay North Chair(s): David Monniaux CNRS, VERIMAG | ||
14:20 25mTalk | Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis Research Papers Damien Octeau University of Wisconsin and Pennsylvania State University, Somesh Jha University of Wisconsin, Madison, Matthew Dering Pennsylvania State University, Patrick McDaniel Pennsylvania State University, Alexandre Bartel Technical University Darmstadt, Hongyu Li Rice University, Jacques Klein University of Luxembourg, Yves Le Traon University of Luxembourg Media Attached | ||
14:45 25mTalk | Abstraction Refinement Guided by a Learnt Probabilistic Model Research Papers Media Attached | ||
15:10 25mTalk | Learning Invariants using Decision Trees and Implication Counterexamples Research Papers Pranav Garg University of Illinois at Urbana-Champaign, Daniel Neider University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Dan Roth University of Illinois at Urbana-Champaign Media Attached | ||
15:35 25mTalk | Symbolic Abstract Data Type Inference Research Papers Media Attached | ||
14:20 - 16:00 | Track 2: Types, Generally or GraduallyResearch Papers at Grand Bay South Chair(s): Tiark Rompf Purdue & Oracle Labs | ||
14:20 25mTalk | Principal Type Inference for GADTs Research Papers Media Attached | ||
14:45 25mTalk | Abstracting Gradual Typing Research Papers Ronald Garcia University of British Columbia, Alison M. Clark , Éric Tanter University of Chile, Chile Link to publication Media Attached | ||
15:10 25mTalk | The Gradualizer: a methodology and algorithm for generating gradual type systems Research Papers Media Attached | ||
15:35 25mTalk | Is Sound Gradual Typing Dead? Research Papers Asumu Takikawa Northeastern University, Daniel Feltey Northeastern University, Ben Greenman Northeastern University, Max New , Jan Vitek Northeastern University, Matthias Felleisen Northeastern University Pre-print Media Attached File Attached | ||
16:30 - 17:45 | |||
16:30 25mTalk | SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization Research Papers Somashekaracharya G Bhaskaracharya Indian Institute of Science and National Instruments, Uday Bondhugula Indian Institute of Science, Albert Cohen INRIA Media Attached File Attached | ||
16:55 25mTalk | PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs Research Papers Wenlei Bao , Sriram Krishnamoorthy Pacific Northwest National Laboratories, Louis-Noël Pouchet Ohio State University, Fabrice Rastello INRIA, France, P. Sadayappan Ohio State University Media Attached | ||
17:20 25mTalk | Printing Floating-Point Numbers: A Faster, Always Correct Method Research Papers Marc Andrysco University of California, San Diego, Ranjit Jhala University of California, San Diego, Sorin Lerner University of California, San Diego Media Attached | ||
16:30 - 17:45 | Track 2: Sessions and processesResearch Papers at Grand Bay South Chair(s): Matteo Maffei Saarland University | ||
16:30 25mTalk | Effects as sessions, sessions as effects Research Papers Pre-print Media Attached | ||
16:55 25mTalk | Monitors and Blame Assignment for Higher-Order Session Types Research Papers Limin Jia Carnegie Mellon University, Hannah Gommerstadt Carnegie Mellon University, Frank Pfenning Carnegie Mellon University Media Attached File Attached | ||
17:20 25mTalk | Environmental Bisimulations for Probabilistic Higher-Order Languages Research Papers Media Attached | ||
18:00 - 19:00 | SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business MeetingResearch Papers at Grand Bay North Chair(s): Michael Hicks University of Maryland at College Park, USA | ||
19:00 - 20:00 | POPL SRC Posters and ReceptionSRC at Lobby III Chair(s): Zachary Tatlock University of Washington, Seattle | ||
Fri 22 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Fri 22 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | Invited Speaker FriInvited Speakers at Grand Bay Ballroom Chair(s): Steve Zdancewic University of Pennsylvania | ||
09:00 60mTalk | Confluences in Programming Languages Research Invited Speakers David Walker Princeton University Media Attached | ||
10:30 - 12:10 | Track 1: Program Design and AnalysisResearch Papers at Grand Bay North Chair(s): Manu Sridharan Samsung Research America | ||
10:30 25mTalk | Newtonian Program Analysis via Tensor Product Research Papers Thomas Reps University of Wisconsin - Madison and Grammatech Inc., Emma Turetsky CS Dept., Univ. of Wisconsin-Madison, Prathmesh Prabhu Google Media Attached | ||
10:55 25mTalk | Casper: An Efficient Approach to Call Trace Collection Research Papers Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao Xiao The Hong Kong University of Science and Technology, Shing-Chi Cheung Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu Zhang Microsoft Research, Charles Zhang HKUST Media Attached | ||
11:20 25mTalk | Pushdown Control-flow Analysis for Free Research Papers Thomas Gilray University of Utah, Steven Lyde , Michael D. Adams University of Utah, Matthew Might University of Utah, USA, David Van Horn University of Maryland, College Park Pre-print Media Attached | ||
11:45 25mTalk | Binding as Sets of Scopes Research Papers Matthew Flatt University of Utah Pre-print Media Attached | ||
10:30 - 12:10 | Track 2: Semantics and memory modelsResearch Papers at Grand Bay South Chair(s): Alexey Gotsman IMDEA | ||
10:30 25mTalk | Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA Research Papers Shaked Flur University of Cambridge, Kathryn E. Gray University of Cambridge, Christopher Pulte University of Cambridge, Susmit Sarkar University of St Andrews, Luc Maranget INRIA Rocquencourt, Ali Sezgin University of Cambridge, Will Deacon ARM Ltd., Peter Sewell University of Cambridge Media Attached File Attached | ||
10:55 25mTalk | A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions Research Papers File Attached | ||
11:20 25mTalk | Overhauling SC atomics in C11 and OpenCL Research Papers John Wickerson Imperial College London, Mark Batty University of Cambridge, Alastair F. Donaldson Imperial College London Pre-print File Attached | ||
11:45 25mTalk | Taming Release-Acquire Consistency Research Papers Pre-print Media Attached File Attached | ||
14:20 - 16:00 | Track 1: SynthesisResearch Papers at Grand Bay North Chair(s): Roberto Giacobazzi University of Verona, Italy | ||
14:20 25mTalk | Learning Programs from Noisy Data Research Papers Veselin Raychev ETH Zurich, Pavol Bielik ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Andreas Krause ETH Zurich Link to publication DOI Pre-print Media Attached File Attached | ||
14:45 25mTalk | Optimizing Synthesis with Metasketches Research Papers James Bornholt University of Washington, Emina Torlak University of Washington, Dan Grossman University of Washington, USA, Luis Ceze University of Washington, USA Pre-print Media Attached | ||
15:10 25mTalk | Maximal Specification Synthesis Research Papers Aws Albarghouthi University of Wisconsin–Madison, Isil Dillig University of Texas, Austin, Arie Gurfinkel Carnegie Mellon University Pre-print Media Attached | ||
15:35 25mTalk | Example-Directed Synthesis: A Type-Theoretic Interpretation Research Papers Jonathan Frankle Princeton University, Peter-Michael Osera Grinnell College, David Walker Princeton University, Steve Zdancewic University of Pennsylvania Pre-print Media Attached File Attached | ||
14:20 - 15:35 | Track 2: Foundations of Model CheckingResearch Papers at Grand Bay South Chair(s): Alexandra Silva Radboud University Nijmegen | ||
14:20 25mTalk | Lattice-Theoretic Progress Measures and Coalgebraic Model Checking Research Papers Ichiro Hasuo University of Tokyo, Shunsuke Shimizu University of Tokyo, Corina Cirstea University of Southampton Media Attached | ||
14:45 25mTalk | Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components Research Papers Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady , Rasmus Ibsen-Jensen , Andreas Pavlogiannis Media Attached | ||
15:10 25mTalk | Memoryful Geometry of Interaction II: Recursion and Adequacy Research Papers Media Attached | ||
Sat 23 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Sat 23 Jan
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | |||
09:00 15mDay opening | Opening remarks and program chair's report Off the Beaten Track Lindsey Kuper Intel Labs | ||
09:15 45mTalk | Keynote Talk: Operationalizing Creative Theories Off the Beaten Track | ||
09:00 - 10:00 | |||
09:00 20mTalk | All You Need is the Monad... What Monad Was That Again? PPS Pre-print | ||
09:20 10mMeeting | Discussion 1 PPS | ||
09:30 20mTalk | An Interface for Black Box Learning in Probabilistic Programs PPS Jan-Willem van de Meent University of Oxford, Brooks Paige University of Oxford, David Tolpin University of Oxford, Frank Wood University of Oxford Pre-print | ||
09:50 10mMeeting | Discussion 2 PPS | ||
09:00 - 10:00 | |||
09:00 60mTalk | Coq 8.5 at work and the future of Coq CoqPL Matthieu Sozeau Inria | ||
10:30 - 12:10 | |||
10:30 25mTalk | Chanakya: Computer-Aided Strategic Reasoning Off the Beaten Track Pre-print | ||
10:55 25mTalk | Programming Interactivity Requires Both Semantics and Semiotics Off the Beaten Track Pre-print | ||
11:20 25mTalk | Correct-by-Construction Interactive Software: From Declarative Specifications to Efficient Implementations Off the Beaten Track Pre-print | ||
11:45 25mTalk | Challenges Facing a High-Level Language for Machine Knitting Off the Beaten Track Pre-print | ||
10:30 - 12:15 | |||
10:30 20mTalk | Models for Probabilistic Programs with an Adversary PPS Pre-print | ||
10:50 10mMeeting | DIscussion 3 PPS | ||
11:00 20mTalk | The Semantics of Figaro, an Embedded Probabilistic Programming Language PPS Pre-print | ||
11:20 10mMeeting | Discussion 4 PPS | ||
11:30 45mMeeting | Implementor Panel: What can semantics do for probabilistic programming and what can probabilistic programming do for semantics? PPS Angelika Kimmig KU Leuven, Oleg Kiselyov , Jan-Willem van de Meent University of Oxford, Avi Pfeffer Charles River Analytics, M: Frank Wood University of Oxford | ||
10:30 - 12:05 | |||
10:30 25mTalk | A Coq Library for Binary Logical Relations CoqPL Link to publication | ||
10:55 25mTalk | A Coinduction Proof Rule for Hoare Doubles CoqPL Christian J. Bell MIT CSAIL Link to publication | ||
11:20 25mTalk | Formalizing Simple Refinements in Coq CoqPL Link to publication | ||
11:45 20mTalk | Company-Coq: Taking Proof General one step closer to a real IDE CoqPL Link to publication | ||
14:00 - 15:35 | Session ThreeOff the Beaten Track at Room St Petersburg I Chair(s): Limin Jia Carnegie Mellon University | ||
14:00 45mTalk | Keynote Talk: Generalising Abstraction Off the Beaten Track | ||
14:45 25mTalk | The Semantics of Syntax: Applying Denotational Semantics to Hygienic Macro Systems Off the Beaten Track Pre-print | ||
15:10 25mTalk | Affine Functional Programs as Higher-order Boolean Circuits Off the Beaten Track Pre-print | ||
14:00 - 15:30 | |||
14:00 20mTalk | A Lambda-Calculus Foundation for Universal Probabilistic Programming PPS Johannes Borgström Uppsala University, Ugo Dal Lago University of Bologna, Andrew D. Gordon Microsoft Research and University of Edinburgh, Marcin Szymczak University of Edinburgh Pre-print | ||
14:20 10mMeeting | Discussion 5 PPS | ||
14:30 20mTalk | Making our Own Luck: A Language for Random Generators PPS Leonidas Lampropoulos University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Cătălin Hriţcu INRIA Paris, John Hughes Chalmers University of Technology, Zoe Paraskevopoulou Princeton University, Li-yao Xia ENS Paris Pre-print | ||
14:50 10mMeeting | Discussion 6 PPS | ||
15:00 20mTalk | Semantics of Higher-order Probabilistic Programs PPS Sam Staton University of Oxford, Hongseok Yang University of Oxford, UK, Chris Heunen University of Edinburgh, Ohad Kammar University of Cambridge, Frank Wood University of Oxford Pre-print | ||
15:20 10mMeeting | Discussion 7 PPS | ||
14:00 - 15:25 | |||
14:00 60mTalk | A Tutorial on using the Paco Library for coinductive reasoning CoqPL Chung-Kil Hur Seoul National University | ||
15:00 25mTalk | Certified Desugaring of Javascript Programs using Coq CoqPL Marek Materzok University of Wroclaw Link to publication | ||
16:00 - 17:30 | |||
16:00 25mTalk | Declarative, Secure, Convergent Edge Computation Off the Beaten Track Pre-print | ||
16:25 25mTalk | Starting from a Clean Slate: Creating a Top-down Parseable Runtime Off the Beaten Track Pre-print | ||
16:50 25mTalk | New Tools and Practices for Online Collaboration in Teaching, Learning, and Research of Programming Languages Off the Beaten Track Pre-print | ||
17:15 15mDay closing | Closing remarks Off the Beaten Track | ||
16:00 - 18:00 | |||
16:00 25mTalk | The Category-theoretic Solution of Recursive Ultra-metric Space Equations CoqPL Link to publication | ||
16:25 25mTalk | A Case for Tactics with (Limited) Side Effects CoqPL Pre-print | ||
16:50 25mTalk | Formal Verification of Stability Properties of Cyber-Physical Systems CoqPL Matthew Chan , Daniel Ricketts University of California, San Diego, Sorin Lerner University of California, San Diego, Gregory Malecha UCSD Link to publication | ||
17:15 30mTalk | The Science of Deep Specification CoqPL Andrew Appel Princeton | ||
17:45 15mTalk | Discussion CoqPL | ||
16:30 - 18:00 | |||
16:30 20mTalk | eXchangeable Random Primitives PPS Pre-print | ||
16:50 10mMeeting | Discussion 8 PPS | ||
17:00 20mTalk | An Application of Computable Distributions to the Semantics of Probabilistic Programs PPS Pre-print | ||
17:20 10mMeeting | Discussion 9 PPS | ||
17:30 20mTalk | On The Semantic Intricacies of Conditioning PPS Friedrich Gretz RWTH Aachen University, Nils Jansen RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Federico Olmedo RWTH Aachen University Pre-print | ||
17:50 10mMeeting | Discussion 10 PPS | ||