Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 13 JanDisplayed time zone: Belfast change
Sun 13 Jan
Displayed time zone: Belfast change
08:30 - 10:30 | |||
08:30 10mDay opening | Opening BEAT António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. Pérez University of Groningen, The Netherlands | ||
08:40 50mTalk | Invited Talk: Gradual Session Types — an Ongoing Journey BEAT Peter Thiemann University of Freiburg, Germany | ||
09:30 20mTalk | Gradual Session Types in Imperative Style BEAT | ||
09:50 20mTalk | Checking the Equivalence of Context-Free Session Types BEAT Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon File Attached | ||
10:10 20mTalk | Effpi: Concurrent Programming with Dependent Behavioural Types BEAT Alceste Scalas Imperial College London, Elias Benussi Imperial College London, Nobuko Yoshida Imperial College London File Attached | ||
09:00 - 10:30 | |||
09:00 90mTalk | Under and Over Approximated Reachability Analysis for the Verifcation of Control Systems VMCAI Sylvie Putot École Polytechnique | ||
09:00 - 10:30 | |||
09:00 60mTalk | PriSC Keynote - Jasmin: A Compiler and Framework for High-Assurance and High-Speed Cryptography PriSC Benjamin Gregoire INRIA File Attached | ||
10:00 30mTalk | Towards Secure Compilation of Power Side-Channel Countermeasures PriSC Marc Gourjon Hamburg University of Technology and NXP Semiconductors Germany GmbH File Attached | ||
11:00 - 12:30 | |||
11:00 30mTalk | Static Analysis of Binary Code with Memory Indirections Using Polyhedra VMCAI Clément Ballabriga , Julien Forget , Laure Gonnord University of Lyon & LIP, France, Giuseppe Lipari , Jordy Ruiz File Attached | ||
11:30 30mTalk | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis VMCAI File Attached | ||
12:00 30mTalk | Application of Abstract Interpretation to the Automotive Electronic Control System VMCAI | ||
11:00 - 12:30 | |||
11:00 30mTalk | Trestle: Bridging the Performance and Safety Divide in WebAssembly PriSC Craig Disselkoen University of California San Diego, Tal Garfinkel Stanford University, Deian Stefan University of California San Diego, Conrad Watt University of Cambridge File Attached | ||
11:30 30mTalk | Protecting C++ Applications Using CHERI PriSC Khilan Gudka University of Cambridge, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge File Attached | ||
12:00 30mTalk | Secure Linking in the CheriBSD Operating System PriSC File Attached | ||
11:00 - 12:30 | |||
11:00 50mTalk | Invited Talk: On Type-Based Complexity Analysis of Programs and Processes BEAT Ugo Dal Lago University of Bologna, Italy / Inria, France | ||
11:50 20mTalk | Global Types with Internal Delegation BEAT Ilaria Castellani INRIA Sophia Antipolis, France, Mariangiola Dezani Università di Torino, Paola Giannini Universita' del Piemonte Orientale, Ross Horne Computer Science and Communications Research Unit, University of Luxembourg File Attached | ||
12:10 20mTalk | Two Declarative Approaches for Session-Based Concurrency BEAT | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Workshops | ||
13:30 - 15:30 | |||
13:30 50mTalk | Invited Talk: Resource-Aware Session Types BEAT Jan Hoffmann Carnegie Mellon University | ||
14:20 50mTalk | Invited Talk: A Session Type Provider: Compile-time Generation of Session Types with Interaction Refinements BEAT Rumyana Neykova Brunel University London File Attached | ||
15:10 20mTalk | Getting Rid of Null-Dereferences – Behavioural Types to the Rescue BEAT Hans Hüttel Department of Computer Science, Aalborg University, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Adrian Francalanza University of Malta, Mario Bravetti Università di Bologna File Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | Minimal Synthesis of String To String Functions From Examples VMCAI | ||
14:30 30mTalk | Lazy but Effective Functional Synthesis VMCAI Grigory Fedyukovich Princeton University, Arie Gurfinkel University of Waterloo, Aarti Gupta Princeton University | ||
15:00 30mTalk | Automatic Program Repair using Formal Verification and Expression Templates VMCAI Thanh-Toan Nguyen , Quang-Trung Ta National University of Singapore, Wei-Ngan Chin National University of Singapore | ||
14:00 - 15:30 | |||
14:00 30mTalk | Translation Validation for Security Properties PriSC Matteo Busi Università di Pisa - Dipartimento di Informatica, Pierpaolo Degano Università di Pisa - Dipartimento di Informatica, Letterio Galletta IMT School for Advanced Studies Pre-print File Attached | ||
14:30 30mTalk | Security Witnesses for Compiler Transformations PriSC File Attached | ||
15:00 30mTalk | A Data Layout Description Language for Cogent PriSC Zilin Chen Data61, CSIRO and UNSW, Matthew Di Meglio UNSW, Liam O'Connor UNSW, Partha Susarla Data61, CSIRO, Christine Rizkallah UNSW, Gabriele Keller Utrecht University | ||
16:00 - 17:30 | Abstract Interpretation (2)VMCAI at Sala III Chair(s): Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France | ||
16:00 30mTalk | Demand Control-Flow Analysis VMCAI Kimball Germane University of Utah, Jay McCarthy University of Massachusetts Lowell, Michael D. Adams University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School | ||
16:30 30mTalk | Effect-driven Flow Analysis VMCAI Jens Nicolay Vrije Universiteit Brussel, Belgium, Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel | ||
17:00 30mTalk | Relatively Complete Pushdown Analysis of Escape Continuations VMCAI Kimball Germane University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School | ||
16:00 - 18:00 | Session 4PriSC at Sala VI Chair(s): David Naumann Stevens Institute of Technology, Aslan Askarov Aarhus University | ||
16:00 30mOther | Short Talks Session PriSC | ||
16:30 30mTalk | Modular Security Guarantees for Low-Level Languages with Stack Traversal PriSC File Attached | ||
17:00 30mTalk | Confidentiality-Preserving Refinement PriSC File Attached | ||
17:30 30mTalk | (Un)Encrypted Computing and Indistinguishability Obfuscation PriSC File Attached | ||
16:00 - 18:25 | Session 4BEAT at Sala VII Chair(s): Adrian Francalanza University of Malta, Jorge A. Pérez University of Groningen, The Netherlands | ||
16:00 50mTalk | Invited Talk: Session Types for Fault-Tolerant Distributed Algorithms BEAT Kirstin Peters TU Berlin | ||
16:50 20mTalk | Behavioral Types as a Semantic Foundation for the GDPR Notion of Purpose BEAT Evangelia Vanezi University of Cyprus, Dimitrios Kouzapas University of Cyprus, Anna Philippou University of Cyprus | ||
17:10 20mTalk | Relating Process Languages for Security and Communication Correctness BEAT Daniele Nantes-Sobrinho University of Brasília, Brazil, Jorge A. Pérez University of Groningen, The Netherlands | ||
17:30 10mBreak | Short break BEAT | ||
17:40 20mTalk | Towards Legally Compliant Governmental Case Work with Dynamic Condition Response Graphs BEAT Søren Debois IT University of Copenhagen, Thomas H. Hildebrandt , Hugo A. López IT University of Copenhagen, Denmark & DCR Solutions A/S Media Attached | ||
18:00 20mTalk | Hardware Interactions as Behavioural Types BEAT Carlos Mão de Ferro LASIGE, Faculty of Sciences, University of Lisbon, Francisco Martins LaSIGE, University of Lisbon, Tiago Cogumbreiro University of Massachusetts Boston File Attached | ||
18:20 5mDay closing | Closing BEAT António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. Pérez University of Groningen, The Netherlands | ||
Mon 14 JanDisplayed time zone: Belfast change
Mon 14 Jan
Displayed time zone: Belfast change
09:00 - 10:30 | |||
09:00 90mTalk | Designing Self-Certifying Software Systems VMCAI Kedar Namjoshi Bell Labs, Nokia | ||
09:00 - 10:30 | |||
09:00 90mTalk | [T4] Programming Cyber-Physical Systems with Logic TutorialFest André Platzer Carnegie Mellon University | ||
09:00 - 10:30 | |||
09:00 90mTalk | [T1] QuickChick: Property-Based Testing in Coq TutorialFest | ||
09:00 - 10:30 | |||
09:00 90mTalk | [T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning TutorialFest Dominic Orchard University of Kent, UK, Harley D. Eades III Augusta University, Vilem-Benjamin Liepelt University of Kent, UK | ||
09:00 - 10:30 | |||
09:00 15mDay opening | Opening OPCT | ||
09:15 25mTalk | A Concurrent Functional Language with Session Types and Control Effects Based on Linear Logic OPCT Luís Caires NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa | ||
09:40 25mTalk | A Foundation for Runtime Enforcement OPCT Adrian Francalanza University of Malta | ||
10:05 25mTalk | Processes as Names? OPCT Hans Hüttel Department of Computer Science, Aalborg University File Attached | ||
09:00 - 10:30 | |||
09:00 90mTalk | [T2] Engineering Distributed Systems via Protocols and Commitments TutorialFest | ||
09:00 - 10:30 | Keynote 1 and Research PaperCPP at Sala XII Chair(s): Magnus O. Myreen Chalmers University of Technology, Sweden | ||
09:00 60mTalk | A Linear Logical Framework in Hybrid CPP Amy Felty University of Ottawa DOI | ||
10:00 30mResearch paper | Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines CPP DOI | ||
11:00 - 12:30 | |||
11:00 30mTalk | Solving and Interpolating Constant Arrays Based on Weak Equivalences VMCAI | ||
11:30 30mTalk | A Decidable Logic for Tree Data-Structures with Measurements VMCAI File Attached | ||
12:00 30mTalk | A Practical Algorithm for Structure Embedding VMCAI File Attached | ||
11:00 - 12:30 | |||
11:00 90mTalk | [T4] Programming Cyber-Physical Systems with Logic TutorialFest André Platzer Carnegie Mellon University | ||
11:00 - 12:30 | |||
11:00 90mTalk | [T1] QuickChick: Property-Based Testing in Coq TutorialFest | ||
11:00 - 12:30 | |||
11:00 90mTalk | [T3] Linear and Graded Modal Types for Fine-Grained Program Reasoning TutorialFest Dominic Orchard University of Kent, UK, Harley D. Eades III Augusta University, Vilem-Benjamin Liepelt University of Kent, UK | ||
11:00 - 12:30 | |||
11:00 90mTalk | [T2] Engineering Distributed Systems via Protocols and Commitments TutorialFest | ||
11:00 - 12:30 | Session 1PEPM at Sala X Chair(s): Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid (UPM) | ||
11:00 5mDay opening | Welcome to PEPM19 PEPM C: Atsushi Igarashi Kyoto University, Japan, C: Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid (UPM) | ||
11:05 55mTalk | Applying Futamura Projections to Compose Languages and Tools in GraalVM (Invited Talk) PEPM Christian Humer Oracle Labs, Switzerland File Attached | ||
12:00 30mTalk | A Simpler Lambda Calculus PEPM Barry Jay University of Technology Sydney DOI | ||
11:00 - 12:30 | Research Papers: Proof Theory, Theory of Programming LanguagesCPP at Sala XII Chair(s): Assia Mahboubi INRIA | ||
11:00 30mResearch paper | A Proof-Theoretic Approach to Certifying Skolemization CPP Kaustuv Chaudhuri Inria, France, Matteo Manighetti Inria & École Polytechnique, Dale Miller INRIA Saclay and LIX DOI | ||
11:30 30mResearch paper | Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory CPP Yannick Forster Saarland University, Steven Schäfer Saarland University, Simon Spies Saarland University, Kathrin Stark Saarland University, Germany DOI | ||
12:00 30mResearch paper | Eliminating Reflection from Type Theory CPP DOI | ||
11:15 - 12:30 | |||
11:15 25mTalk | Causal Reasoning for Safety OPCT Georgiana Caltais University of Konstanz File Attached | ||
11:40 25mTalk | A Calculus of Branching Processes OPCT Jean Krivine CNRS | ||
12:05 25mTalk | An Axiomatic Approach to Reversible Computation OPCT Irek Ulidowski University of Leicester | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Workshops | ||
13:50 - 15:30 | Session Types, Graph-RewritingOPCT at Sala VII Chair(s): António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS | ||
13:50 25mTalk | Taming Concurrency for Verification using Multiparty Session Types OPCT Kirstin Peters TU Berlin | ||
14:15 25mTalk | From Testing Preorders to Flaky Tests OPCT Giovanni Bernardi Université Paris Diderot File Attached | ||
14:40 25mTalk | Multiparty Reactive Sessions OPCT Cinzia Di Giusto Laboratoire I3S File Attached | ||
15:05 25mTalk | Independence, Concurrency and Abstraction in Graph-Rewriting Processes OPCT | ||
14:00 - 15:30 | |||
14:00 30mTalk | Syntactic Partial Order Compression for Probabilistic Reachability VMCAI | ||
14:30 30mTalk | Termination of Nondeterministic Probabilistic Programs VMCAI | ||
15:00 30mTalk | Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics VMCAI | ||
14:00 - 15:30 | |||
13:50 10mDay opening | PADL Opening and Welcome PADL Moa Johansson Chalmers University of Technology, José Julio Alferes NOVA LINCS -- Universidade Nova de Lisboa | ||
14:00 30mTalk | Natural Language Generation From Ontologies PADL | ||
14:30 30mTalk | Incremental Evaluation of Lattice-Based Aggregates in Logic Programming Using Modular TCLP PADL File Attached | ||
15:00 30mTalk | Improving Residuation in Declarative Programs PADL Michael Hanus Kiel University File Attached | ||
14:00 - 15:30 | |||
14:00 90mTalk | [T7] Higher-Order Probabilistic Programming TutorialFest Ugo Dal Lago University of Bologna, Italy / Inria, France Pre-print | ||
14:00 - 15:30 | |||
14:00 90mTalk | [T5] Correct-by-Construction Programming in Agda TutorialFest | ||
14:00 - 15:30 | |||
14:00 90mTalk | [T8] Building Your Own Modular Static Analyser with Infer TutorialFest Jules Villard Facebook London, Ezgi Çiçek Facebook London, Mehdi Bouaziz Facebook London, Nikos Gorogiannis | ||
14:00 - 15:30 | |||
14:00 90mTalk | [T6] Session-Typed Concurrent Programming TutorialFest Stephanie Balzer Carnegie Mellon University, USA | ||
14:00 - 15:30 | |||
14:00 30mTalk | Method Name Suggestion with Hierarchical Attention Networks PEPM Sihan Xu Nankai University, China, Sen Zhang Nankai University, China, Weijing Wang Nankai University, China, Xinya Cao Nankai University, China, Chenkai Guo Nankai University, China, Jing Xu Nankai University, China DOI | ||
14:30 30mTalk | Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking PEPM Keiichi Watanabe University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Hiroki Oshikawa University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan DOI | ||
15:00 30mTalk | Typed Parsing and Unparsing for Untyped Regular Expression Engines PEPM Gabriel Radanne University of Freiburg, Germany DOI Pre-print File Attached | ||
14:00 - 15:30 | |||
14:00 30mResearch paper | Formally Verified Big Step Semantics out of x86-64 Binaries CPP Ian Roessle Virginia Tech, USA, Freek Verbeek Open University of the Netherlands, The Netherlands, Binoy Ravindran Virginia Tech DOI | ||
14:30 30mResearch paper | Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions CPP DOI | ||
15:00 30mResearch paper | From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server CPP Nicolas Koh , Yao Li University of Pennsylvania, Yishuai Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Lennart Beringer Princeton University, Wolf Honore , William Mansky University of Illinois at Chicago, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI | ||
16:00 - 17:30 | |||
16:00 30mTalk | Verification of an Industrial Asynchronous Leader Election Algorithm Using Abstractions and Parametric Model Checking VMCAI Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Laurent Fribourg , Romain Soulat , Jean-Marc Mota | ||
16:30 30mTalk | A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization VMCAI File Attached | ||
17:00 30mTalk | Flat Model Checking for Counting LTL using Quantifier-free Presburger Arithmetic VMCAI | ||
16:00 - 17:30 | |||
16:00 30mTalk | Faster Coroutine Pipelines: A Reconstruction PADL | ||
16:30 30mTalk | Distributed Protocol Combinators PADL Kristoffer Just Arndal Andersen Aarhus University, Ilya Sergey Yale-NUS College and National University of Singapore Pre-print | ||
17:00 30mTalk | Classes of Arbitrary Kind PADL Alejandro Serrano Utrecht University, Netherlands, Victor Cacciari Miraldo Utrecht University, Netherlands Link to publication DOI File Attached | ||
16:00 - 17:30 | |||
16:00 90mTalk | [T7] Higher-Order Probabilistic Programming TutorialFest Ugo Dal Lago University of Bologna, Italy / Inria, France Pre-print | ||
16:00 - 17:30 | |||
16:00 90mTalk | [T5] Correct-by-Construction Programming in Agda TutorialFest | ||
16:00 - 17:30 | |||
16:00 90mTalk | [T8] Building Your Own Modular Static Analyser with Infer TutorialFest Jules Villard Facebook London, Ezgi Çiçek Facebook London, Mehdi Bouaziz Facebook London, Nikos Gorogiannis | ||
16:00 - 17:15 | Concurrent Programming, Memory ModelsOPCT at Sala VII Chair(s): Gustavo Petri IRIF, Université Paris Diderot | ||
16:00 25mTalk | Linearizability in the Context of Weak Memory Models OPCT Kirsten Winter The University of Queensland File Attached | ||
16:25 25mTalk | IPA: Invariant-preserving Applications for Weakly Consistent Replicated Databases OPCT Carla Ferreira Universidade Nova Lisboa | ||
16:50 25mTalk | Compositional Reasoning for Termination of Fine-grained Concurrent Programs OPCT Emanuele D’Osualdo Imperial College London, UK Pre-print File Attached | ||
16:00 - 17:30 | |||
16:00 90mTalk | [T6] Session-Typed Concurrent Programming TutorialFest Stephanie Balzer Carnegie Mellon University, USA | ||
16:00 - 17:30 | |||
16:00 60mTalk | What Is the Type of a Partial Evaluator? (Invited Talk) PEPM Jens Palsberg University of California, Los Angeles (UCLA) File Attached | ||
17:00 30mTalk | Combining Higher-Order Model Checking with Refinement Type Inference PEPM Ryosuke Sato Kyushu University, Japan, Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan DOI | ||
16:00 - 17:30 | Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII Chair(s): Georges Gonthier Inria | ||
16:00 30mResearch paper | A Formal Proof of Hensel's Lemma over the p-adic Integers CPP Robert Y. Lewis Vrije Universiteit Amsterdam DOI | ||
16:30 30mResearch paper | Counting Polynomial Roots in Isabelle/HOL: A formal Proof of the Budan-Fourier Theorem CPP DOI | ||
17:00 30mResearch paper | Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL CPP DOI | ||
17:30 - 18:30 | |||
17:30 60mSocial Event | Social Hour Workshops | ||
Tue 15 JanDisplayed time zone: Belfast change
Tue 15 Jan
Displayed time zone: Belfast change
09:00 - 10:30 | |||
09:00 15mDay opening | PLMW Welcome PLMW Pre-print | ||
09:15 45mTalk | Technical Talk: Verification of Distributed Protocols Using Decidable Logic PLMW Sharon Shoham Tel Aviv university Pre-print File Attached | ||
10:00 30mTalk | Research Skills: How to Give a Talk PLMW Chung-chieh Shan Indiana University, USA Pre-print File Attached | ||
09:00 - 10:30 | |||
09:00 90mTalk | Semantics for Compiler IRs: Undefined Behavior is not Evil! VMCAI Nuno P. Lopes Microsoft Research Media Attached | ||
09:00 - 10:30 | |||
09:30 30mTalk | Personalized Course Schedule Planning using Answer Set Programming PADL File Attached | ||
10:00 30mTalk | Static Partitioning of Spreadsheets for Parallel Execution PADL File Attached | ||
09:00 - 10:30 | |||
09:00 30mTalk | Probabilistic Lambda Calculus: Beyond Deterministic Evaluation LAFI File Attached | ||
09:30 60mTalk | Invited talk: Connecting Probabilistic Programming Theory to Applications in Stan LAFI Matthijs Vákár University of Oxford File Attached | ||
09:00 - 10:30 | Equational Characterisations, TransactionsOPCT at Sala VII Chair(s): Mohammad Mousavi University of Leicester, UK | ||
09:15 25mTalk | Revised Semantics for Sequential Composition in the Presence of Successful Termination (Tentative) OPCT Bas Luttik Eindhoven University of Technology File Attached | ||
09:40 25mTalk | ULTraS at Work: Compositionality and Equational Characterization of Behavioral Metaequivalences OPCT Marco Bernardo University of Urbino File Attached | ||
10:05 25mTalk | A Uniform Framework of Transactional Consistency Models for Protocol Verification and Program Analysis OPCT Andrea Cerone Imperial College London | ||
09:00 - 10:30 | |||
09:00 60mTalk | Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL CPP Jasmin Blanchette Vrije Universiteit Amsterdam DOI | ||
10:00 30mResearch paper | A Verified Prover Based on Ordered Resolution CPP Anders Schlichtkrull Technical University of Denmark, Jasmin Blanchette Vrije Universiteit Amsterdam, Dmitriy Traytel ETH Zurich DOI | ||
11:00 - 12:30 | |||
11:00 30mTalk | Research Skills: How to Choose Research Areas PLMW Catuscia Palamidessi INRIA and LIX Pre-print File Attached | ||
11:30 60mTalk | Panel: Grad School and Beyond PLMW Dominic Orchard University of Kent, UK, Jorge A. Pérez University of Groningen, The Netherlands, Azalea Raad MPI-SWS, Germany, Max S. New Northeastern University, Stephanie Balzer Carnegie Mellon University, USA Pre-print | ||
11:00 - 12:30 | |||
11:00 30mTalk | Mechanically Proving Determinacy of Hierarchical Block Diagram Translations VMCAI Link to publication DOI Pre-print File Attached | ||
11:30 30mTalk | euforia: Complete Software Model Checking with Uninterpreted Functions VMCAI | ||
12:00 30mTalk | Program Synthesis with Equivalence Reduction VMCAI | ||
11:00 - 12:30 | |||
11:00 30mTalk | An ASP-based Approach to Representing and Querying Textual Knowledge PADL | ||
11:30 30mTalk | Strong Equivalence and Program's Structure in Arguing Essential Equivalence PADL Yuliya Lierler University of Nebraska | ||
12:00 30mTalk | Automatic Program Rewriting in Non-Ground Answer Set Programs PADL | ||
11:00 - 12:30 | |||
11:00 30mTalk | The Geometry of Bayesian Programming LAFI | ||
11:30 30mTalk | Model and Inference Combinators for Deep Probabilistic Programming LAFI Eli Sennesh Northeastern University, Adam Ścibior University of Cambridge and MPI Tuebingen, Hao Wu Northeastern University, Jan-Willem van de Meent Northeastern University File Attached | ||
12:00 30mTalk | Server-side Probabilistic Programming LAFI David Tolpin PUB+ Media Attached | ||
11:00 - 12:30 | Session 4PEPM at Sala X Chair(s): Roberto Giacobazzi University of Verona and IMDEA Software Institute | ||
11:00 60mTalk | Making Proofs Easy: Horn Clause Transformations to the Aid of Program Verification (Invited Talk) PEPM File Attached | ||
12:00 30mTalk | Control Flow Obfuscation via CPS Transformation PEPM Kenny Zhuo Ming Lu Nanyang Polytechnic, Singapore DOI | ||
11:00 - 12:30 | Research Papers: Rewriting, Automated ReasoningCPP at Sala XII Chair(s): Andrei Popescu Middlesex University, London | ||
11:00 30mResearch paper | Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions CPP DOI | ||
11:30 30mResearch paper | Certified ACKBO CPP DOI | ||
12:00 30mResearch paper | A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL CPP DOI | ||
11:15 - 12:30 | Cyberphysical Systems, Hybrid SystemsOPCT at Sala VII Chair(s): Philippa Gardner Imperial College London | ||
11:15 25mTalk | Hybrid Systems Reachability Analysis OPCT Erika Abraham RWTH Aachen University | ||
11:40 25mTalk | Attribute Based Communication for Collective Adaptive Systems OPCT | ||
12:05 25mTalk | Designing Resilient Large Scaled CPS: Models, Languages and Tools OPCT Michele Loreti University of Camerino | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Workshops | ||
13:50 - 15:30 | Algebra, Coalgebra, Model CheckingOPCT at Sala VII Chair(s): Barbara König University of Duisburg-Essen | ||
13:50 25mTalk | Bayes meets Dijkstra: Verifying Bayes Networks by Program Verification OPCT Joost-Pieter Katoen RWTH Aachen University File Attached | ||
14:15 25mTalk | Model Checking True Concurrency Properties OPCT Paolo Baldan University of Padova File Attached | ||
14:40 25mTalk | A (Co)algebraic Approach to Hennessy-Milner Theorems for Weakly Expressive Logics OPCT Helle Hvid Hansen Delft University of Technology File Attached | ||
15:05 25mTalk | Weak Bisimulation Metrics in Models with Nondeterminism and Continuous States Space: A Logical Characterization OPCT Simone Tini University of Insubria | ||
14:00 - 15:30 | |||
14:00 45mTalk | Technical Talk: How to Think about Types PLMW Frank Pfenning Carnegie Mellon University, USA Pre-print File Attached | ||
14:45 45mTalk | Technical Talk: What Is Programming Languages Research? PLMW Michael Hicks University of Maryland, College Park Pre-print File Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | Type-directed Bounding of Collections in Reactive Programs VMCAI Tianhan Lu University of Colorado Boulder, Pavol Cerny University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder, Ashutosh Trivedi | ||
14:30 30mTalk | Exploiting Pointer Analysis in Memory Models for Deductive Verification VMCAI Quentin Bouillaguet , François Bobot CEA, Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France, Boris Yakobowski CEA - LIST File Attached | ||
15:00 30mTalk | Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs VMCAI Anja Karl Institute of Applied Information Processing and Communications, Graz University of Technology, Robert Schilling , Roderick Bloem Institute of Software Technology, Graz University of Technology , Stefan Mangard | ||
14:00 - 15:30 | |||
14:00 30mTalk | Composing Syntactical Constructs to Create Domain-Specific Languages PADL DOI Media Attached | ||
14:30 30mTalk | Proof Carrying Plans PADL Christopher Schwaab University of St Andrews, Ekaterina Komendantskaya Heriot-Watt University, UK, Alasdair Hill , Frantisek Farka , Ron Petrick , Joe Wells , Kevin Hammond University of St. Andrews, UK | ||
15:00 30mTalk | A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers PADL Paul Tarau University of North Texas | ||
14:00 - 15:30 | |||
14:00 30mTalk | A Nuts-and-Bolts Differential Geometric Perspective on Automatic Differentiation LAFI Barak A. Pearlmutter Maynooth University | ||
14:30 30mTalk | Kotlin∇: Differentiable Functional Programming with Algebraic Data Types LAFI Breandan Considine Université de Montréal File Attached | ||
15:00 30mTalk | Probabilistic Programming with CuPPL LAFI | ||
14:00 - 15:30 | |||
14:00 30mTalk | Extracting a Call-by-Name Partial Evaluator from a Proof of Termination PEPM Kenichi Asai Ochanomizu University DOI File Attached | ||
14:30 30mTalk | Futures and Promises in Haskell and Scala PEPM Tamino Dauth Karlsruhe University of Applied Sciences, Germany, Martin Sulzmann Karlsruhe University of Applied Sciences, Germany DOI File Attached | ||
15:00 28mTalk | Generating Mutually Recursive Definitions PEPM DOI Pre-print | ||
15:28 2mPoster | Advanced Futures and Promises in C++ (poster) PEPM Tamino Dauth Karlsruhe University of Applied Sciences, Germany, Martin Sulzmann Karlsruhe University of Applied Sciences, Germany | ||
14:00 - 15:30 | |||
14:00 30mResearch paper | A Verified Protocol Buffer Compiler CPP DOI | ||
14:30 30mResearch paper | A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra CPP DOI | ||
15:00 30mResearch paper | Dynamic Class Initialization Semantics: a Jinja Extension CPP DOI | ||
16:00 - 17:30 | |||
16:00 30mTalk | Research Skills: How to Bootstrap a Research Project PLMW Ilya Sergey Yale-NUS College and National University of Singapore Pre-print File Attached | ||
16:30 60mTalk | Panel: How to Do Good PL Research PLMW Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon, Deepak Garg Max Planck Institute for Software Systems, Philippa Gardner Imperial College London, Atsushi Igarashi Kyoto University, Japan, Neel Krishnaswami Computer Laboratory, University of Cambridge Pre-print | ||
16:00 - 17:30 | |||
16:00 30mTalk | On the Semantics of Snapshot Isolation VMCAI | ||
16:30 30mTalk | Fast BGP Simulation of Large Datacenters VMCAI Pre-print | ||
17:00 30mTalk | Parametric Timed Broadcast Protocols VMCAI Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Benoit Delahaye , Paulin Fournier , Didier Lime File Attached | ||
16:00 - 17:30 | |||
16:00 30mTalk | Probabilistic Programming Inference via Intensional Semantics LAFI | ||
16:30 30mTalk | Factorized Exact Inference for Discrete Probabilistic Programs LAFI Steven Holtzen University of California, Los Angeles, Joe Qian University of California, Los Angeles, Todd Millstein University of California, Los Angeles, Guy Van den Broeck University of California, Los Angeles | ||
17:00 30mTalk | Verified Equational Reasoning on a Little Language of Measures LAFI | ||
16:00 - 17:20 | |||
16:00 25mTalk | Coalgebra Learning via Duality OPCT Jurriaan Rot Radboud University Nijmegen | ||
16:25 25mTalk | A Metric Semantics for Coordination Languages OPCT Valentina Castiglioni Inria Saclay - Ile de France File Attached | ||
16:50 25mTalk | Hybrid System Iteration OPCT Renato Neves University of Minho & INESC TEC File Attached | ||
17:15 5mDay closing | Closing OPCT | ||
16:00 - 17:30 | Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII Chair(s): Zhong Shao Yale University | ||
16:00 30mResearch paper | On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem CPP Yannick Forster Saarland University, Dominik Kirst Saarland University, Gert Smolka Saarland University DOI | ||
16:30 30mResearch paper | Verified Solving and Asymptotics of Linear Recurrences CPP Manuel Eberl Technische Universität München DOI | ||
17:00 30mMeeting | Business Meeting CPP | ||
17:30 - 18:30 | |||
17:30 60mSocial Event | Social Hour Workshops | ||
Wed 16 JanDisplayed time zone: Belfast change
Wed 16 Jan
Displayed time zone: Belfast change
09:00 - 10:05 | |||
09:00 5mDay opening | Welcome Research Papers Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU), Stephanie Weirich University of Pennsylvania, USA Media Attached | ||
09:05 60mTalk | Automated Fault-Finding and Fixing at Facebook Research Papers Mark Harman Facebook and University College London Media Attached | ||
10:35 - 12:03 | Reasoning about Probabilistic ProgramsResearch Papers at Sala I Chair(s): Jan Hoffmann Carnegie Mellon University | ||
10:35 22mTalk | Formal Verification of Higher-Order Probabilistic Programs Research Papers Tetsuya Sato University at Buffalo, SUNY, USA, Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Justin Hsu University of Wisconsin-Madison, USA Link to publication DOI Media Attached File Attached | ||
10:57 22mTalk | A Separation Logic for Concurrent Randomized Programs Research Papers Link to publication DOI Media Attached File Attached | ||
11:19 22mTalk | Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs Research Papers Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University Link to publication DOI Media Attached File Attached | ||
11:41 22mTalk | Trace Abstraction Modulo Probability Research Papers Calvin Smith University of Wisconsin - Madison, Justin Hsu University of Wisconsin-Madison, USA, Aws Albarghouthi University of Wisconsin-Madison Link to publication DOI Media Attached | ||
10:35 - 12:03 | |||
10:35 22mTalk | A True Positives Theorem for a Static Race Detector Research Papers Nikos Gorogiannis , Peter W. O'Hearn Facebook and University College London, Ilya Sergey Yale-NUS College and National University of Singapore Link to publication DOI Pre-print Media Attached File Attached | ||
10:57 22mTalk | Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
11:19 22mTalk | Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs Research Papers Klaus v. Gleissenthall University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Alexander Bakst , Deian Stefan University of California San Diego, Ranjit Jhala University of California, San Diego Link to publication DOI Media Attached | ||
11:41 22mTalk | Weak-Consistency Specification via Visibility Relaxation Research Papers Link to publication DOI Media Attached File Attached | ||
12:03 - 13:45 | |||
12:03 1h42mLunch | Lunch Research Papers | ||
13:45 - 14:51 | |||
13:45 22mTalk | Familial Monads and Structural Operational Semantics Research Papers Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry Link to publication DOI Media Attached File Attached | ||
14:07 22mTalk | Bindings as Bounded Natural Functors Research Papers Jasmin Blanchette Vrije Universiteit Amsterdam, Lorenzo Gheri Middlesex University London, Andrei Popescu Middlesex University, London, Dmitriy Traytel ETH Zurich Link to publication DOI Media Attached File Attached | ||
14:29 22mTalk | Categorical Combinatorics of Scheduling and Synchronization in Game Semantics Research Papers Paul-André Melliès CNRS and University Paris Diderot Link to publication DOI Media Attached File Attached | ||
15:21 - 16:27 | Machine Learning and Linear AlgebraResearch Papers at Sala I Chair(s): Aws Albarghouthi University of Wisconsin-Madison | ||
15:21 22mTalk | code2vec: Learning Distributed Representations of Code Research Papers Uri Alon Technion, Meital Zilberstein Technion, Omer Levy University of Washington, USA, Eran Yahav Technion Link to publication DOI Pre-print Media Attached File Attached | ||
15:43 22mTalk | An Abstract Domain for Certifying Neural Networks Research Papers Link to publication DOI Media Attached | ||
16:05 22mTalk | Closed Forms for Numerical Loops Research Papers Zachary Kincaid Princeton University, Jason Breck University of Wisconsin - Madison, John Cyphert University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. Link to publication DOI Media Attached File Attached | ||
15:21 - 16:27 | Capabilities and Session Types IResearch Papers at Sala II Chair(s): Dominic Orchard University of Kent, UK | ||
15:21 22mTalk | StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities Research Papers Lau Skorstengaard Aarhus University, Dominique Devriese Vrije Universiteit Brussel, Belgium, Lars Birkedal Aarhus University Link to publication DOI Media Attached File Attached | ||
15:43 22mTalk | Two sides of the same coin: Session Types and Game Semantics Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
16:05 22mTalk | Exceptional Asynchronous Session Types: Session Types without Tiers Research Papers Simon Fowler The University of Edinburgh, Sam Lindley University of Edinburgh, UK, J. Garrett Morris University of Kansas, USA, Sara Décova Link to publication DOI Pre-print Media Attached File Attached | ||
16:37 - 17:43 | Quantum ProgrammingResearch Papers at Sala I Chair(s): Jens Palsberg University of California, Los Angeles (UCLA) | ||
16:37 22mTalk | Quantitative Robustness Analysis of Quantum Programs Research Papers Shih-Han Hung University of Maryland, Kesha Hietala University of Maryland, Shaopeng Zhu University of Maryland, Mingsheng Ying University of Technology Sydney, Michael Hicks University of Maryland, College Park, Xiaodi Wu University of Oregon, USA Link to publication DOI Media Attached | ||
16:59 22mTalk | Game Semantics for Quantum Programming Research Papers Link to publication DOI Media Attached | ||
17:21 22mTalk | Quantum Relational Hoare Logic Research Papers Dominique Unruh University of Tartu Link to publication DOI Pre-print Media Attached File Attached | ||
16:37 - 17:43 | Session Types IIResearch Papers at Sala II Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
16:37 22mTalk | Interconnectability of Session-Based Logical ProcessesTOPLAS Research Papers Link to publication DOI Pre-print Media Attached | ||
16:59 22mTalk | Distributed Programming using Role-Parametric Session Types in Go Research Papers David Castro-Perez Imperial College London, Raymond Hu Imperial College London, Sung-Shik Jongmans Open University of the Netherlands, Nicholas Ng Imperial College London, Nobuko Yoshida Imperial College London Link to publication DOI Pre-print Media Attached File Attached | ||
17:21 22mTalk | Less is More: Multiparty Session Types Revisited Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
18:00 - 18:30 | |||
18:00 30mTalk | Microsoft Research: Engage, Verify, Open Research Papers Thomas Ball Microsoft Research Media Attached | ||
18:30 - 19:30 | |||
18:30 60mSocial Event | Student Research Competition and Reception supported by Microsoft Research Student Research Competition | ||
Thu 17 JanDisplayed time zone: Belfast change
Thu 17 Jan
Displayed time zone: Belfast change
09:00 - 10:06 | |||
09:00 22mTalk | Abstraction-Safe Effect Handlers via Tunneling Research Papers Link to publication DOI Media Attached | ||
09:22 22mTalk | Abstracting Algebraic Effects Research Papers Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław Link to publication DOI Media Attached | ||
09:44 22mTalk | Fully Abstract Module Compilation Research Papers Karl Crary Carnegie Mellon University Link to publication DOI Media Attached File Attached | ||
09:00 - 10:06 | |||
09:00 22mTalk | Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper Research Papers Nadia Polikarpova University of California, San Diego, Ilya Sergey Yale-NUS College and National University of Singapore Link to publication DOI Pre-print Media Attached File Attached | ||
09:22 22mTalk | FrAngel: Component-Based Synthesis with Control Structures Research Papers Kensen Shi Stanford University, Jacob Steinhardt Stanford University, Percy Liang Stanford University Link to publication DOI Pre-print Media Attached File Attached | ||
09:44 22mTalk | Hamsaz: Replication Coordination Analysis and Synthesis Research Papers Farzin Houshmand University of California, Riverside, Mohsen Lesani University of California, Riverside Link to publication DOI Media Attached | ||
10:30 - 12:30 | |||
10:36 - 12:04 | |||
10:36 22mTalk | Type-Driven Gradual Security with ReferencesTOPLAS Research Papers Matías Toro University of Chile, Ronald Garcia University of British Columbia, Éric Tanter University of Chile & Inria Paris DOI Media Attached File Attached | ||
10:58 22mTalk | Gradual Type Theory Research Papers Max S. New Northeastern University, Daniel R. Licata Wesleyan University, Amal Ahmed Northeastern University, USA Link to publication DOI Media Attached File Attached | ||
11:20 22mTalk | Gradual Parametricity, RevisitedDistinguished Paper Research Papers Matías Toro University of Chile, Elizabeth Labrada University of Chile, Éric Tanter University of Chile & Inria Paris Link to publication DOI Pre-print Media Attached File Attached | ||
11:42 22mTalk | Live Functional Programming with Typed Holes Research Papers Cyrus Omar University of Chicago, Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago, Matthew Hammer None Link to publication DOI Pre-print Media Attached File Attached | ||
10:36 - 12:04 | Separation Logic and Memory SemanticsResearch Papers at Sala II Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore | ||
10:36 22mTalk | Iron: Managing Obligations in Higher-Order Concurrent Separation Logic Research Papers Aleš Bizjak Aarhus University, Daniel Gratzer , Robbert Krebbers Delft University of Technology, Lars Birkedal Aarhus University Link to publication DOI Media Attached File Attached | ||
10:58 22mTalk | JaVerT 2.0: Compositional Symbolic Execution for JavaScript Research Papers José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Gabriela Sampaio Imperial College London, UK, Philippa Gardner Imperial College London Link to publication DOI Media Attached File Attached | ||
11:20 22mTalk | ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS Research Papers Alasdair Armstrong University of Cambridge, Thomas Bauereiss University of Cambridge, Brian Campbell University of Edinburgh, Alastair Reid Arm Ltd, Kathryn E. Gray University of Cambridge, Robert M. Norton University of Cambridge, Prashanth Mundkur SRI International, Mark Wassell University of Cambridge, Jon French University of Cambridge, Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Ian Stark The University of Edinburgh, Neel Krishnaswami Computer Laboratory, University of Cambridge, Peter Sewell University of Cambridge Link to publication DOI Media Attached File Attached | ||
11:42 22mTalk | Exploring C Semantics and Pointer Provenance Research Papers Kayvan Memarian University of Cambridge, Victor B. F. Gomes University of Cambridge, UK, Brooks Davis SRI International, Stephen Kell University of Kent, Alexander Richardson University of Cambridge, Robert N. M. Watson University of Cambridge, Peter Sewell University of Cambridge Link to publication DOI Media Attached File Attached | ||
12:04 - 13:45 | |||
12:04 1h41mLunch | Lunch Research Papers | ||
13:45 - 14:51 | Type Inference IResearch Papers at Sala I Chair(s): Michael Hicks University of Maryland, College Park | ||
13:45 22mTalk | Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types Research Papers Jana Dunfield Queen's University, Kingston, Ontario, Neel Krishnaswami Computer Laboratory, University of Cambridge Link to publication DOI Media Attached | ||
14:07 22mTalk | Abstracting Extensible Data Types; Or, Rows By Any Other Name Research Papers Link to publication DOI Media Attached | ||
14:29 22mTalk | Polymorphic Symmetric Multiple Dispatch with Variance Research Papers Gyunghee Park KAIST, Oracle Labs, Jaemin Hong KAIST, South Korea, Guy L. Steele Jr. Oracle Labs, Sukyoung Ryu KAIST, South Korea Link to publication DOI Media Attached File Attached | ||
13:45 - 14:51 | |||
13:45 22mTalk | On Library Correctness under Weak Memory Consistency Research Papers Azalea Raad MPI-SWS, Germany, Marko Doko MPI-SWS, Germany, Lovro Rožić MPI-SWS, Germany, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany Link to publication DOI Pre-print Media Attached File Attached | ||
14:07 22mTalk | Bridging the Gap Between Programming Languages and Hardware Weak Memory Models Research Papers Anton Podkopaev Higher School of Economics, JetBrains Research, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS, Germany Link to publication DOI Pre-print Media Attached File Attached | ||
14:29 22mTalk | Grounding Thin-Air Reads with Event Structures Research Papers Link to publication DOI Media Attached File Attached | ||
15:21 - 16:49 | |||
15:21 22mTalk | Type-Guided Worst-Case Input Generation Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
15:43 22mTalk | CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem Research Papers Conrad Watt University of Cambridge, John Renner University of California, San Diego, Natalie Popescu University of California San Diego, Sunjay Cauligi UCSD, Deian Stefan University of California San Diego Link to publication DOI Media Attached File Attached | ||
16:05 22mTalk | Modular Quantitative Monitoring Research Papers Rajeev Alur University of Pennsylvania, Konstantinos Mamouras University of Pennsylvania, Caleb Stanford University of Pennsylvania Link to publication DOI Media Attached File Attached | ||
16:27 22mTalk | CSS Minification via Constraint SolvingTOPLAS Research Papers Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Chih-Duo Hong University of Oxford Media Attached File Attached | ||
17:00 - 18:00 | |||
17:00 15mOther | PC Chair Report Research Papers Stephanie Weirich University of Pennsylvania, USA Media Attached | ||
17:15 10mAwards | SIGPLAN Awards Research Papers Benjamin C. Pierce University of Pennsylvania Media Attached | ||
17:25 5mOther | POPL 2020 Announcement Research Papers Media Attached | ||
17:30 10mOther | NSF funding for PL Research Papers Rance Cleaveland University of Maryland Media Attached | ||
17:40 10mOther | SIGPLAN Climate Committee Report Research Papers Benjamin C. Pierce University of Pennsylvania Media Attached | ||
17:50 10mOther | State of SIGPLAN Research Papers Jens Palsberg University of California, Los Angeles (UCLA) Media Attached | ||
18:15 - 19:15 | |||
18:15 60mSocial Event | Reception supported by Facebook Research Papers | ||
Fri 18 JanDisplayed time zone: Belfast change
Fri 18 Jan
Displayed time zone: Belfast change
09:00 - 10:05 | SRC Announcement & Keynote IIStudent Research Competition / Research Papers at Sala I + II Chair(s): Stephanie Weirich University of Pennsylvania, USA | ||
09:00 5mAwards | SRC Announcement Student Research Competition Niki Vazou IMDEA Software Institute Media Attached | ||
09:05 60mTalk | Mechanized Metatheory - The Next Chapter Research Papers Brigitte Pientka McGill University Media Attached File Attached | ||
10:35 - 12:03 | |||
10:35 22mTalk | Higher Inductive Types in Cubical Computational Type Theory Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
10:57 22mTalk | Constructing Quotient Inductive-Inductive Types Research Papers Thorsten Altenkirch University of Nottingham, Ambrus Kaposi University of Nottingham, András Kovács Eötvös Loránd University Link to publication DOI Media Attached File Attached | ||
11:19 22mTalk | Definitional Proof-Irrelevance without K Research Papers Gaetan Gilbert , Jesper Cockx Chalmers | University of Gothenburg, Matthieu Sozeau Inria, Nicolas Tabareau Inria Link to publication DOI Media Attached File Attached | ||
11:41 22mTalk | Bisimulation as Path Type for Guarded Recursive Types Research Papers Link to publication DOI Media Attached File Attached | ||
12:03 - 13:45 | |||
12:03 1h42mLunch | Lunch Research Papers | ||
13:45 - 14:51 | |||
13:45 22mTalk | Better Late Than Never: A Fully Abstract Semantics for Classical Processes Research Papers Wen Kokke University of Edinburgh, Fabrizio Montesi University of Southern Denmark, Marco Peressotti University of Southern Denmark Link to publication DOI Media Attached | ||
14:07 22mTalk | Diagrammatic Algebra: From Linear to Concurrent Systems Research Papers Filippo Bonchi University of Pisa, Joshua Holland University of Southampton, Robin Piedeleu University of Oxford, Pawel Sobocinski University of Southampton, Fabio Zanasi University College London Link to publication DOI Media Attached | ||
14:29 22mTalk | Fixpoint Games on Continuous Lattices Research Papers Paolo Baldan University of Padova, Barbara König University of Duisburg-Essen, Christina Mika-Michalski University of Duisburg-Essen, Tommaso Padoan University of Padova Link to publication DOI Media Attached File Attached | ||
13:45 - 14:51 | Model CheckingResearch Papers at Sala II Chair(s): P. Madhusudan University of Illinois at Urbana-Champaign | ||
13:45 22mTalk | Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations Research Papers Taolue Chen Birkbeck, University of London, Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Philipp Ruemmer Uppsala University, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Link to publication DOI Media Attached File Attached | ||
14:07 22mTalk | Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation Research Papers Kyungmin Bae Pohang University of Science and Technology (POSTECH), Jia Lee Pohang University of Science and Technology (POSTECH) Link to publication DOI Media Attached File Attached | ||
14:29 22mTalk | Adventures in Monitorability: From Branching to Linear Time and Back Again Research Papers Luca Aceto Reykjavik University, Antonis Achilleos Reykjavik University, Adrian Francalanza University of Malta, Anna Ingolfsdottir Reykjavik University, Karoliina Lehtinen University of Kiel and University of Liverpool Link to publication DOI Media Attached | ||
15:21 - 16:27 | |||
15:21 22mTalk | LWeb: Information Flow Security for Multi-Tier Web Applications Research Papers James Parker University of Maryland, Niki Vazou IMDEA Software Institute, Michael Hicks University of Maryland, College Park Link to publication DOI Media Attached File Attached | ||
15:43 22mTalk | From Fine- to Coarse-Grained Dynamic Information Flow Control and BackDistinguished Paper Research Papers Marco Vassena Chalmers University of Technology, Alejandro Russo Chalmers University of Technology, Sweden, Deepak Garg Max Planck Institute for Software Systems, Vineet Rajani MPI-SWS, Deian Stefan University of California San Diego Link to publication DOI Media Attached File Attached | ||
16:05 22mTalk | Modalities, Cohesion, and Information Flow Research Papers Alex Kavvos Wesleyan University Link to publication DOI Pre-print File Attached | ||
15:21 - 16:27 | |||
15:21 22mTalk | Decidable Verification of Uninterpreted Programs Research Papers Umang Mathur University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign Link to publication DOI Pre-print Media Attached File Attached | ||
15:43 22mTalk | Inferring Frame Conditions with Static Correlation Analysis Research Papers Oana-Fabiana Andreescu Internet of Trust, Thomas P. Jensen INRIA Rennes, Stéphane Lescuyer Prove & Run, Benoît Montagu Prove & Run Link to publication DOI Pre-print Media Attached File Attached | ||
16:05 22mTalk | Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown SystemsDistinguished Paper Research Papers Johannes Späth Fraunhofer IEM, Karim Ali University of Alberta, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM Link to publication DOI Pre-print Media Attached File Attached | ||
16:37 - 17:43 | |||
16:37 22mTalk | Efficient Automated Repair of High Floating-Point Errors in Numerical Libraries Research Papers Xin Yi National University of Defense Technology, Liqian Chen National University of Defense Technology, Xiaoguang Mao National University of Defense Technology, Tao Ji National University of Defense Technology Link to publication DOI Media Attached File Attached | ||
16:59 22mTalk | Efficient Parameterized Algorithms for Data Packing Research Papers Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady IST Austria, Nastaran Okati Ferdowsi University of Mashhad, Andreas Pavlogiannis EPFL, Switzerland Link to publication DOI Pre-print Media Attached File Attached | ||
17:21 22mTalk | Fast and exact analysis for LRU caches Research Papers Valentin Touzeau Univ. Grenoble Alpes, Claire Maiza Verimag, France, David Monniaux CNRS, VERIMAG, Jan Reineke Saarland University Link to publication DOI Media Attached File Attached | ||
17:45 - 18:45 | |||
17:45 60mSocial Event | Social Hour Research Papers | ||
Sat 19 JanDisplayed time zone: Belfast change
Sat 19 Jan
Displayed time zone: Belfast change
09:00 - 10:30 | Keynote & Contributed Talks 1CoqPL at Sala VI Chair(s): Ilya Sergey Yale-NUS College and National University of Singapore | ||
09:00 5mDay opening | Opening CoqPL | ||
09:05 60mTalk | Coq User Interfaces: Past, Present, and Future (Keynote) CoqPL | ||
10:05 25mTalk | Counterexamples for Coq Conjectures CoqPL Samuel Gruetter Massachusetts Institute of Technology File Attached | ||
09:00 - 10:30 | |||
09:30 60mTalk | De-escalating Software (Keynote) Off the Beaten Track Stephen Kell University of Kent | ||
11:00 - 12:30 | |||
11:00 45mTalk | Facile : A Domain Specific Language and Compiler for Program Analysis and Optimization Off the Beaten Track File Attached | ||
11:45 45mTalk | From Tactics to Structure Editors for Proofs Off the Beaten Track Xuanrui Qi Tufts University Pre-print | ||
11:15 - 12:30 | |||
11:15 25mTalk | Towards Mechanising Probabilistic Properties of a Blockchain CoqPL Kiran Gopinathan University College London, Ilya Sergey Yale-NUS College and National University of Singapore File Attached | ||
11:40 25mTalk | Verifying Finality for Blockchain Systems CoqPL Karl Palmskog University of Texas at Austin, Milos Gligoric University of Texas at Austin, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign File Attached | ||
12:05 25mTalk | WIP: Formalizing the Concordium Consensus Protocol in Coq CoqPL Thomas Dinsdale-Young , Bas Spitters Aarhus University, Søren Eller Thomsen Aarhus University, Daniel Tschudi Aarhus University File Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Workshops | ||
14:00 - 15:30 | Contributed Talks 3 & Coq DevelopersCoqPL at Sala VI Chair(s): Qinxiang Cao Shanghai Jiao Tong University | ||
14:00 25mTalk | Reification of Shallow-Embedded DSLs in Coq with Automated Verification CoqPL File Attached | ||
14:25 25mTalk | Reifying and Translating a Monadic Fragment of Gallina CoqPL File Attached | ||
14:50 40mDemonstration | Session with the Coq Development Team CoqPL | ||
14:00 - 15:30 | |||
14:00 45mOther | Design Critique and Discussion Off the Beaten Track | ||
14:45 45mTalk | F a Language for Music Composition Off the Beaten Track File Attached | ||
16:00 - 17:40 | |||
16:00 25mTalk | Deep Embedded Hoare Logic for Building Machine-Checkable Foundational Program Correctness Proofs CoqPL Qinxiang Cao Shanghai Jiao Tong University File Attached | ||
16:25 25mTalk | Teaching Discrete Mathematics to Early Undergraduates with Software Foundations CoqPL File Attached | ||
16:50 25mTalk | Ltac2: Tactical Warfare CoqPL File Attached | ||
17:15 25mTalk | Towards a Coq Formalisation of Build Systems CoqPL File Attached | ||
16:00 - 17:30 | |||
16:00 90mMeeting | Informal + Business Meeting Off the Beaten Track | ||