Filter Program
Conference Dates
Conference Dates are in time zone (GMT-05:00) Guadalajara, Mexico City, Monterrey, and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
Conference DaySun 17 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Sun 17 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
08:50 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | Automating Abstract Interpretation VMCAI Thomas RepsUniversity 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 | ||
Conference DayMon 18 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Mon 18 JanDisplayed 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 HornUniversity of Maryland, College Park Link to publication | ||
08:30 - 10:00 | |||
08:30 90mTalk | T3: Syntax-Guided Synthesis (SyGuS) Tutorials Rajeev AlurUniversity of Pennsylvania, Dana FismanUniversity of Pennsylvania, Rishabh SinghMicrosoft Research, Armando Solar-LezamaMIT 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 ChughUniversity of Chicago | ||
09:00 - 10:00 | |||
09:00 60mTalk | Ironclad - Full Verification of Complex Systems VMCAI Bryan ParnoMicrosoft Research | ||
09:00 - 10:00 | |||
09:00 60mTalk | Perspectives on Formal Verfication CPP Harvey FriedmanOhio 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 VisserDelft University of Technology | ||
10:30 - 12:00 | |||
10:30 90mTalk | T3: Syntax-Guided Synthesis (SyGuS) (Advanced Material) Tutorials Rajeev AlurUniversity of Pennsylvania, Dana FismanUniversity of Pennsylvania, Rishabh SinghMicrosoft Research, Armando Solar-LezamaMIT 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 MaffeiSaarland 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 LammichTechnische Universität München | ||
14:00 - 15:30 | |||
14:00 30mTalk | A GPU implementation of the ASP computation PADL Agostino DovierUniversity of Udine, Andrea FormisanoUniversità di Perugia , Enrico PontelliNew Mexico State University, Flavio VellaSapienza 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 ZhouCUNY Brooklyn College and Graduate Center, Håkan KjellerstrandCUNY 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 HornUniversity 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 MaffeiSaarland University | ||
14:00 - 15:30 | Dynamic and Static VerificationVMCAI at Room St Petersburg I Chair(s): Aarti GuptaPrinceton University | ||
14:00 30mTalk | Hybrid Analysis for Partial Order Reduction of Programs with Arrays VMCAI Pavel ParizekCharles 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 KotelnikovChalmers University of Technology, Laura KovacsChalmers University of Technology, Giles RegerUniversity of Manchester, Andrei VoronkovUniversity of Manchester | ||
14:30 30mTalk | Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP Lukasz CzajkaUniversity of Innsbruck | ||
15:00 30mTalk | Mizar Environment for Isabelle CPP Cezary KaliszykUniversity of Innsbruck, Karol PąkUniversity 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 HertumKU Leuven, Ingmar DassevilleKU Leuven, Gerda JanssensKU Leuven, Marc DeneckerKU 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 VisserDelft 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 BernardINRIA, Yves BertotINRIA, Laurence RideauINRIA, Pierre-Yves StrubIMDEA 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 | ||
Conference DayTue 19 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Tue 19 JanDisplayed 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 ChangUniversity of Colorado Boulder | ||
09:00 60mTalk | Viper - A Verification Infrastructure for Permission-based Reasoning VMCAI Peter MüllerETH Zurich | ||
09:00 - 10:00 | |||
09:00 60mTalk | Dependent Type Practice CPP Leonardo de MouraMicrosoft Research, Redmond | ||
09:00 - 10:00 | |||
09:00 30mTalk | Grad School: A Survival Guide PLMW Matthew MightUniversity of Utah, USA Media Attached | ||
09:30 30mTalk | Theorem Provers are a PL Researcher's Best Friend PLMW Xavier LeroyInria Media Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Computing with Catalan Families, Generically PADL Paul TarauUniversity of North Texas | ||
11:00 30mTalk | A Size-proportionate Bijective Encoding of Lambda Terms as Catalan Objects endowed with Arithmetic Operations PADL Paul TarauUniversity 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 AsaiOchanomizu University | ||
10:30 30mTalk | Practical, General Parser Combinators PEPM Anastasia IzmaylovaCentrum Wiskunde & Informatica, Ali AfroozehCentrum Wiskunde & Informatica, Tijs van der StormCWI 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 LindleyUniversity of Edinburgh, Josef SvenningssonChalmers University of Technology, Sweden, Philip WadlerUniversity of Edinburgh DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Pointer Race Freedom VMCAI | ||
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 DoornCarnegie Mellon University | ||
11:30 30mTalk | A Nominal Exploration of Intuitionism CPP | ||
10:30 - 12:00 | |||
10:30 30mTalk | Academia or Industry? PLMW Aarti GuptaPrinceton University Media Attached | ||
11:00 30mTalk | Refining Types with SMT PLMW Ranjit JhalaUniversity of California, San Diego Media Attached | ||
11:30 30mTalk | How to Write Papers So People Can Read Them PLMW Derek DreyerMPI-SWS Media Attached | ||
14:00 - 15:30 | Domain-Specific Languages IIPEPM at Room Harbor View Chair(s): Sebastian ErdwegTU Darmstadt, Germany | ||
14:00 30mTalk | BiGUL: A Formally Verified Core Language for Putback-Based Bidirectional Programming PEPM Hsiang-Shang ‘Josh’ KoNational Institute of Informatics, Tao ZanSokendai, Japan, Zhenjiang HuNational Institute of Informatics DOI Pre-print | ||
14:30 30mTalk | A Constraint Language for Static Semantic Analysis Based on Scope Graphs PEPM Hendrik van AntwerpenDelft University of Technology, Netherlands, Pierre NeronTU Delft, Andrew TolmachPortland State University, Eelco VisserDelft University of Technology, Guido WachsmuthDelft 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 GurfinkelCarnegie Mellon University | ||
14:00 30mTalk | Regular Symmetry Patterns VMCAI Anthony Widjaja LinYale-NUS College, Singapore, Truong Khanh Nguyen, Philipp RuemmerUppsala 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 WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity 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 SilvaRadboud University Nijmegen Media Attached | ||
15:00 30mTalk | Unaccustomed As I Am to Public Speaking PLMW John HughesChalmers University of Technology Media Attached | ||
16:00 - 17:40 | |||
16:00 30mTalk | Staging Generic Programming PEPM Jeremy YallopUniversity 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 AsaiOchanomizu University DOI | ||
17:20 20mTalk | Staging beyond Terms: Prospects and Challenges PEPM Jun InoueNational 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 HarperCarnegie Mellon University Media Attached | ||
16:30 30mTalk | Highs and Lows of a Language Researcher PLMW Greg MorrisettCornell 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 VytiniotisMicrosoft Research, Cambridge Media Attached | ||
18:00 - 21:00 | |||
18:00 3hSocial Event | CPP Reception, sponsored by the DeepSpec project CPP | ||
Conference DayWed 20 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Wed 20 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | Invited WedInvited Speakers at Grand Bay Ballroom Chair(s): Rastislav BodikUniversity of Washington, USA | ||
09:00 60mTalk | Programming the World of Uncertain Things Invited Speakers Kathryn S McKinleyMicrosoft Research | ||
10:30 - 12:10 | Track 1: Algorithmic VerificationResearch Papers at Grand Bay North Chair(s): Arie GurfinkelCarnegie Mellon University | ||
10:30 25mTalk | Temporal Verification of Higher-order Functional Programs Research Papers Akihiro Murase, Tachio TerauchiJAIST, Naoki KobayashiUniversity of Tokyo, Ryosuke SatoUniversity of Tokyo, Hiroshi UnnoUniversity of Tsukuba | ||
10:55 25mTalk | Scaling Network Verification using Symmetry and Surgery Research Papers Gordon Plotkin, Nikolaj BjørnerMicrosoft Research, Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research, George VargheseMicrosoft 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 AtkeyUniversity 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 CaiUniversity of Tübingen, Germany, Paolo G. GiarrussoUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany Media Attached | ||
11:45 25mTalk | A Theory of Effects and Resources: Adjunction Models and Polarised Calculi Research Papers Pierre-Louis CurienUniv. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo FioreComputer Laboratory, University of Cambridge, Guillaume Munch-MaccagnoniComputer Laboratory, University of Cambridge | ||
14:20 - 16:00 | Track 1: Decision ProceduresResearch Papers at Grand Bay North Chair(s): Loris D'AntoniUniversity of Pennsylvania | ||
14:20 25mTalk | Query-Guided Maximum Satisfiability Research Papers Xin ZhangGeorgia Tech, Ravi MangalGeorgia Institute of Technology, Aditya NoriMicrosoft Research, UK, Mayur NaikGeorgia 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 CardelliMicrosoft Research and University of Oxford, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinIMT Institute for Advanced Studies Lucca, Italy Media Attached | ||
15:35 25mTalk | Unboundedness and Downward Closures of Higher-Order Pushdown Automata Research Papers Matthew HagueRoyal Holloway University of London, UK, Jonathan KochemsDepartment of Computer Science, University of Oxford, C.-H. Luke OngUniversity of Oxford, UK Media Attached | ||
14:20 - 16:00 | Track 2: Correct CompilationResearch Papers at Grand Bay South Chair(s): Jens PalsbergUniversity of California, Los Angeles | ||
14:20 25mTalk | Fully-Abstract Compilation by Approximate Back-Translation Research Papers Dominique DevrieseiMinds - Distrinet, KU Leuven, Marco PatrignaniKU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven Pre-print Media Attached | ||
14:45 25mTalk | Lightweight Verification of Separate Compilation Research Papers Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-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 OngUniversity of Oxford, UK | ||
16:30 25mTalk | Decidability of Inferring Inductive Invariants Research Papers Oded PadonTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Sharon Shoham, Aleksandr KarbyshevTel Aviv University, Mooly SagivTel 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 | |||
Conference DayThu 21 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Thu 21 JanDisplayed 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. MurrayCalifornia Institute of Technology Media Attached | ||
10:30 - 12:10 | Track 1: Foundations of distributed systemsResearch Papers at Grand Bay North Chair(s): Mooly SagivTel 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 GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6 Media Attached | ||
11:20 25mTalk | A Program Logic for Concurrent Objects under Fair Scheduling Research Papers Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity 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 NoriMicrosoft 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 KatzTechnion, Israel Institute of Technology, Ran El-YanivTechnion, Israel Institute of Technology, Eran YahavTechnion Media Attached File Attached | ||
11:20 25mTalk | Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs Research Papers Krishnendu ChatterjeeIST Austria, Hongfei FuIST Austria, Rouzbeh HasheminezhadSharif 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 MonniauxCNRS, VERIMAG | ||
14:20 25mTalk | Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis Research Papers Damien OcteauUniversity of Wisconsin and Pennsylvania State University, Somesh JhaUniversity of Wisconsin, Madison, Matthew DeringPennsylvania State University, Patrick McDanielPennsylvania State University, Alexandre BartelTechnical University Darmstadt, Hongyu LiRice University, Jacques KleinUniversity of Luxembourg, Yves Le TraonUniversity 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 GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Dan RothUniversity 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 RompfPurdue & Oracle Labs | ||
14:20 25mTalk | Principal Type Inference for GADTs Research Papers Media Attached | ||
14:45 25mTalk | Abstracting Gradual Typing Research Papers 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 TakikawaNortheastern University, Daniel FelteyNortheastern University, Ben GreenmanNortheastern University, Max New, Jan VitekNortheastern University, Matthias FelleisenNortheastern 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 BhaskaracharyaIndian Institute of Science and National Instruments, Uday BondhugulaIndian Institute of Science, Albert CohenINRIA Media Attached File Attached | ||
16:55 25mTalk | PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs Research Papers Wenlei Bao, Sriram KrishnamoorthyPacific Northwest National Laboratories, Louis-Noël PouchetOhio State University, Fabrice RastelloINRIA, France, P. SadayappanOhio State University Media Attached | ||
17:20 25mTalk | Printing Floating-Point Numbers: A Faster, Always Correct Method Research Papers Marc AndryscoUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Sorin LernerUniversity of California, San Diego Media Attached | ||
16:30 - 17:45 | Track 2: Sessions and processesResearch Papers at Grand Bay South Chair(s): Matteo MaffeiSaarland 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 JiaCarnegie Mellon University, Hannah GommerstadtCarnegie Mellon University, Frank PfenningCarnegie 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 HicksUniversity of Maryland at College Park, USA | ||
19:00 - 20:00 | POPL SRC Posters and ReceptionSRC at Lobby III Chair(s): Zachary TatlockUniversity of Washington, Seattle | ||
Conference DayFri 22 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Fri 22 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | Invited Speaker FriInvited Speakers at Grand Bay Ballroom Chair(s): Steve ZdancewicUniversity of Pennsylvania | ||
09:00 60mTalk | Confluences in Programming Languages Research Invited Speakers David WalkerPrinceton University Media Attached | ||
10:30 - 12:10 | Track 1: Program Design and AnalysisResearch Papers at Grand Bay North Chair(s): Manu SridharanSamsung Research America | ||
10:30 25mTalk | Newtonian Program Analysis via Tensor Product Research Papers Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc., Emma TuretskyCS Dept., Univ. of Wisconsin-Madison, Prathmesh PrabhuGoogle Media Attached | ||
10:55 25mTalk | Casper: An Efficient Approach to Call Trace Collection Research Papers Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao XiaoThe Hong Kong University of Science and Technology, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu ZhangMicrosoft Research, Charles ZhangHKUST Media Attached | ||
11:20 25mTalk | Pushdown Control-flow Analysis for Free Research Papers Thomas GilrayUniversity of Utah, Steven Lyde, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Utah, USA, David Van HornUniversity of Maryland, College Park Pre-print Media Attached | ||
11:45 25mTalk | Binding as Sets of Scopes Research Papers Matthew FlattUniversity of Utah Pre-print Media Attached | ||
10:30 - 12:10 | Track 2: Semantics and memory modelsResearch Papers at Grand Bay South Chair(s): Alexey GotsmanIMDEA | ||
10:30 25mTalk | Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA Research Papers Shaked FlurUniversity of Cambridge, Kathryn E. GrayUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Susmit SarkarUniversity of St Andrews, Luc MarangetINRIA Rocquencourt, Ali SezginUniversity of Cambridge, Will DeaconARM Ltd., Peter SewellUniversity 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 WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair F. DonaldsonImperial College London Pre-print File Attached | ||
11:45 25mTalk | Taming Release-Acquire Consistency Research Papers Pre-print Media Attached File Attached | ||
14:20 - 15:35 | Track 2: Foundations of Model CheckingResearch Papers at Grand Bay South Chair(s): Alexandra SilvaRadboud University Nijmegen | ||
14:20 25mTalk | Lattice-Theoretic Progress Measures and Coalgebraic Model Checking Research Papers Ichiro HasuoUniversity of Tokyo, Shunsuke ShimizuUniversity of Tokyo, Corina CirsteaUniversity of Southampton Media Attached | ||
14:45 25mTalk | Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components Research Papers Krishnendu ChatterjeeIST 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 | ||
Conference DaySat 23 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Sat 23 JanDisplayed 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 KuperIntel 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 MeentUniversity of Oxford, Brooks PaigeUniversity of Oxford, David TolpinUniversity of Oxford, Frank WoodUniversity 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 SozeauInria | ||
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 KimmigKU Leuven, Oleg Kiselyov, Jan-Willem van de MeentUniversity of Oxford, Avi PfefferCharles River Analytics, M: Frank WoodUniversity 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. BellMIT 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 JiaCarnegie 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ömUppsala University, Ugo Dal LagoUniversity of Bologna, Andrew D. GordonMicrosoft Research and University of Edinburgh, Marcin SzymczakUniversity of Edinburgh Pre-print | ||
14:20 10mMeeting | Discussion 5 PPS | ||
14:30 20mTalk | Making our Own Luck: A Language for Random Generators PPS Leonidas LampropoulosUniversity of Pennsylvania, Benjamin C. PierceUniversity of Pennsylvania, Cătălin HriţcuINRIA Paris, John HughesChalmers University of Technology, Zoe ParaskevopoulouPrinceton University, Li-yao XiaENS Paris Pre-print | ||
14:50 10mMeeting | Discussion 6 PPS | ||
15:00 20mTalk | Semantics of Higher-order Probabilistic Programs PPS Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, UK, Chris HeunenUniversity of Edinburgh, Ohad KammarUniversity of Cambridge, Frank WoodUniversity 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 HurSeoul National University | ||
15:00 25mTalk | Certified Desugaring of Javascript Programs using Coq CoqPL Marek MaterzokUniversity 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 RickettsUniversity of California, San Diego, Sorin LernerUniversity of California, San Diego, Gregory MalechaUCSD Link to publication | ||
17:15 30mTalk | The Science of Deep Specification CoqPL Andrew AppelPrinceton | ||
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 GretzRWTH Aachen University, Nils JansenRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University, Joost-Pieter KatoenRWTH Aachen University, Federico OlmedoRWTH Aachen University Pre-print | ||
17:50 10mMeeting | Discussion 10 PPS | ||