Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 7 JanDisplayed time zone: Tijuana, Baja California change
Sun 7 Jan
Displayed time zone: Tijuana, Baja California change
09:00 - 10:00 | |||
09:00 60mTalk | Reasoning about Functions VMCAI Ranjit Jhala University of California, San Diego | ||
10:30 - 12:00 | |||
10:30 30mTalk | Abstraction-Based Interaction Model for Synthesis VMCAI | ||
11:00 30mTalk | A Framework for Computer-Aided Design of Educational Domain Models VMCAI Eric Butler University of Washington, Emina Torlak University of Washington, Zoran Popovic University of Washington | ||
11:30 30mTalk | Generating Tests by Example VMCAI | ||
14:00 - 15:30 | |||
14:00 30mTalk | Gradual Program Verification VMCAI Johannes Bader Microsoft, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile | ||
14:30 30mTalk | A Logical System for Modular Information Flow Verification VMCAI Adi Prabawa National University of Singapore, Mahmudul Faisal Al Ameen National University of Singapore, Benedict Lee National University of Singapore, Wei-Ngan Chin National University of Singapore | ||
15:00 30mTalk | P5: Planner-less Proofs of Probabilistic Parameterized Protocols VMCAI | ||
16:00 - 17:30 | |||
16:00 30mTalk | Code Obfuscation Against Abstract Model Checking Attacks VMCAI Roberto Bruni Dipartimento di Informatica, Universita' di Pisa, Roberto Giacobazzi University of Verona and IMDEA Software Institute, Roberta Gori Dipartimento di Informatica, Universita' di Pisa | ||
16:30 30mTalk | Scalable Approximation of Quantitative Information Flow in Programs VMCAI Fabrizio Biondi CentraleSupelec Rennes, Mike Enescu INRIA, Annelie Heuser CNRS/IRISA, Axel Legay , Kuldeep S. Meel National University of Singapore, Jean Quilbeuf INRIA | ||
17:00 30mTalk | Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference VMCAI | ||
Mon 8 JanDisplayed time zone: Tijuana, Baja California change
Mon 8 Jan
Displayed time zone: Tijuana, Baja California change
09:00 - 10:30 | |||
09:00 90mTalk | Equational reasoning for probabilistic programming. TutorialFest Media Attached | ||
09:00 - 10:30 | |||
09:00 90mTalk | Programming and Reasoning with Infinite Data in Isabelle/HOL. TutorialFest Media Attached | ||
09:00 - 10:00 | Invited Talk by René ThiemannCPP at Museum A Chair(s): June Andronick Data61,CSIRO (formerly NICTA) and UNSW | ||
09:00 60mTalk | Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper) CPP Jose Divasón , Sebastiaan Joosten , Ondřej Kunčar Technische Universität München, Germany, René Thiemann University of Innsbruck, Akihisa Yamada DOI | ||
09:00 - 10:30 | |||
09:00 90mTalk | Message-Passing Concurrency and Substructural Logics TutorialFest Frank Pfenning Carnegie Mellon University, USA Media Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | How to Stay Decidable VMCAI Kenneth L. McMillan Microsoft Research | ||
09:00 - 10:30 | |||
09:00 90mTalk | Code Obfuscation - A Hacking view on program analysis and understanding. TutorialFest Media Attached | ||
10:30 - 12:00 | Session 1-1PEPM at Crocker Chair(s): Hsiang-Shang ‘Josh’ Ko National Institute of Informatics, Japan | ||
10:30 60mTalk | Developments in Property-Based Testing (Invited Talk) PEPM Jan Midtgaard University of Southern Denmark DOI | ||
11:30 30mTalk | Selective CPS Transformation for Shift and Reset PEPM DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Total Haskell is Reasonable Coq CPP Antal Spector-Zabusky , Joachim Breitner University of Pennsylvania, Christine Rizkallah University of Pennsylvania, USA, Stephanie Weirich University of Pennsylvania, USA DOI | ||
11:00 30mTalk | A Formal Proof in Coq of a Control Function for the Inverted Pendulum CPP Damien Rouhling University of Côte d'Azur, France DOI | ||
11:30 30mTalk | Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq CPP DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | On Constructivity of Galois Connections VMCAI Francesco Ranzato University of Padova | ||
11:00 30mTalk | An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs VMCAI Laura Titolo National Institute of Aerospace, USA, Marco A. Feliu National Institute of Aerospace, Mariano Moscato National Institute of Aerospace, Cesar Munoz NASA | ||
11:30 30mTalk | Modular Analysis of Executables using On-Demand Heyting Completion VMCAI | ||
11:00 - 12:00 | |||
11:00 60mTalk | Equational reasoning for probabilistic programming. TutorialFest Media Attached | ||
11:00 - 12:00 | |||
11:00 60mTalk | Programming and Reasoning with Infinite Data in Isabelle/HOL. TutorialFest Media Attached | ||
11:00 - 12:00 | |||
11:00 60mTalk | Message-Passing Concurrency and Substructural Logics TutorialFest Frank Pfenning Carnegie Mellon University, USA Media Attached | ||
11:00 - 12:00 | |||
11:00 60mTalk | Code Obfuscation - A Hacking view on program analysis and understanding. TutorialFest Media Attached | ||
13:30 - 15:30 | |||
13:30 30mTalk | Mechanising and Verifying the WebAssembly Specification CPP Conrad Watt University of Cambridge, UK DOI | ||
14:00 30mTalk | Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL CPP Sidney Amani UNSW, Australia, Myriam Bégel ENS Paris-Saclay, France, Maksym Bortin , Mark Staples CSIRO, Australia DOI | ||
14:30 30mTalk | Mechanising Blockchain Consensus CPP DOI Pre-print | ||
15:00 30mTalk | Formal Microeconomic Foundations and the First Welfare Theorem CPP | ||
13:30 - 14:30 | |||
13:30 30mDay opening | Opening PADL | ||
14:00 30mTalk | INVITED TALK: ``Safe'' Languages Require Sequential Consistency PADL | ||
14:00 - 15:30 | |||
14:00 90mTalk | Computational Higher Type Theory TutorialFest Media Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | A Guess-and-Assume Approach to Loop Fusion for Program Verification PEPM Akifumi Imanishi Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University, Atsushi Igarashi Kyoto University, Japan DOI | ||
14:30 30mTalk | Gradually Typed Symbolic Expressions PEPM DOI | ||
15:00 30mTalk | On the Cost of Type-Tag Soundness PEPM DOI | ||
14:00 - 15:30 | |||
14:00 90mTalk | Introduction to Algebraic Program analysis. TutorialFest Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. Media Attached | ||
14:00 - 15:30 | |||
14:00 90mTalk | Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic. TutorialFest Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, A: Robbert Krebbers Delft University of Technology Media Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | Revisiting MITL to Fix Decision Procedures VMCAI Nima Roohi University of Pennsylvania, Mahesh Viswanathan University of Illinois at Urbana-Champaign | ||
14:30 30mTalk | On abstraction and compositionality for weak-memory linearisability VMCAI Brijesh Dongol Brunel University London, Radha Jagadeesan DePaul University, James Riely DePaul University, Alasdair Armstrong Brunel University | ||
15:00 30mTalk | Automatic Verification of RMA Programs via Abstraction Extrapolation VMCAI Cedric Baumann ETH Zurich, Andrei Marian Dan ETH Zurich, Yuri Meshman IMDEA, Torsten Hoefler ETH Zurich, Martin Vechev ETH Zürich | ||
14:00 - 15:30 | |||
14:00 90mTalk | One Weird Trick: Relational Interpreters for Program Synthesis. TutorialFest Media Attached | ||
14:30 - 15:30 | |||
14:30 30mTalk | Exploiting Term Hiding to Reduce Run-time Checking Overhead PADL A: Nataliia Stulova IMDEA Software Institute and T.U. of Madrid (UPM), A: José Morales IMDEA Software Institute, A: Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid (UPM) | ||
15:00 30mTalk | On k-colored Lambda Terms and their Skeletons PADL | ||
16:00 - 17:00 | |||
16:00 60mTalk | Computational Higher Type Theory TutorialFest Media Attached | ||
16:00 - 17:30 | |||
16:00 60mTalk | The Simple Essence of Automatic Differentiation (Invited Talk) PEPM Conal Elliott Target, USA Pre-print | ||
16:00 - 17:00 | |||
16:00 60mTalk | Introduction to Algebraic Program analysis. TutorialFest Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. Media Attached | ||
16:00 - 18:00 | |||
16:00 30mTalk | Triangulating Context Lemmas CPP DOI | ||
16:30 30mTalk | Adapting Proof Automation to Adapt Proofs CPP Talia Ringer University of Washington, Nathaniel Yazdani University of Washington, Seattle, John Leo Halfaya Research, Dan Grossman University of Washington DOI | ||
17:00 30mTalk | A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations CPP Niklas Grimm Vienna University of Technology, Austria, Kenji Maillard Inria Paris and ENS Paris, Cédric Fournet Microsoft Research, Cătălin Hriţcu Inria Paris, Matteo Maffei Saarland University, Jonathan Protzenko Microsoft Research, n.n., Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Santiago Zanella-Béguelin Microsoft Research, n.n. DOI | ||
17:30 30mTalk | Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations CPP Hugo Férée University of Kent, UK, Samuel Hym University of Lille, France, Micaela Mayero , Jean-Yves Moyen University of Copenhagen, Denmark, David Nowak CNRS, France DOI | ||
16:00 - 17:00 | |||
16:00 60mTalk | Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic. TutorialFest Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, A: Robbert Krebbers Delft University of Technology Media Attached | ||
16:00 - 17:00 | |||
16:00 30mTalk | An Automated Detection of Inconsistencies in SBVR-based Business Rules using Many-sorted Logic PADL | ||
16:30 30mTalk | Three is a crowd: SAT, SMT and CLP on a chessboard PADL A: Sebastian Krings , A: Michael Leuschel University of Düsseldorf, A: Philipp Koerner , A: Stefan Hallerstede , A: Miran Hasanagic | ||
16:00 - 17:30 | Invited Tutorial by Mayur NaikVMCAI at Watercourt Chair(s): Jens Palsberg University of California, Los Angeles (UCLA) | ||
16:00 90mTalk | Maximum Satisfiability in Program Analysis: Applications and Techniques VMCAI Mayur Naik University of Pennsylvania, Xujie Si University of Pennsylvania, Xin Zhang Massachusetts Institute of Technology, USA, Radu Grigore University of Kent | ||
16:00 - 17:00 | |||
16:00 60mTalk | One Weird Trick: Relational Interpreters for Program Synthesis. TutorialFest Media Attached | ||
18:00 - 22:00 | |||
18:00 4hDinner | Banquet VMCAI | ||
18:15 - 20:15 | |||
18:15 2hSocial Event | CPP Reception CPP | ||
Tue 9 JanDisplayed time zone: Tijuana, Baja California change
Tue 9 Jan
Displayed time zone: Tijuana, Baja California change
09:00 - 10:00 | SESSION I (invited talk) PPS at Bradbury Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
09:00 60mTalk | Software is eating the world, but ML is going to eat software PPS | ||
09:00 - 10:00 | |||
09:00 30mTalk | Store, Translate and Forward: From Model to Metal in 25 Years NetPL Jonathan Smith DARPA | ||
09:30 30mTalk | Common Models for Network Configuration and Behavioral Validation NetPL Anees Shaikh Google | ||
09:00 - 10:00 | |||
09:00 60mTalk | POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk) CPP Brigitte Pientka McGill University DOI | ||
09:00 - 10:00 | |||
09:00 30mTalk | Liquid Haskell: Refinement Types for Haskell PLMW Niki Vazou University of Maryland File Attached | ||
09:30 30mTalk | How to Become a Researcher PLMW Armando Solar-Lezama MIT CSAIL File Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | INVITED TALK: Declarative Algorithms on Big Data: a Logic-Based Solution PADL File Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | Rethinking Compositionality for Concurrent Program Proofs VMCAI Azadeh Farzan University of Toronto | ||
10:30 - 12:00 | |||
10:30 30mTalk | The semantic structure of quasi-Borel spaces: algebra, logic, and recursion PPS Chris Heunen University of Edinburgh, Ohad Kammar University of Oxford, Sean Moss University of Oxford, Adam Ścibior University of Cambridge and MPI Tuebingen, Sam Staton University of Oxford, Matthijs Vákár University of Oxford, Hongseok Yang University of Oxford | ||
11:00 30mTalk | Stable, measurable functions and probabilistic programs PPS Michele Pagani University Paris Diderot, Thomas Ehrhard CNRS and University Paris Diderot, Christine Tasson University Paris Diderot | ||
11:30 30mTalk | Formal Methods For Probabilistic Programming PPS Daniel Selsam Stanford University | ||
10:30 - 12:00 | |||
10:30 60mTalk | Challenges in the Design and Compilation of Programming Languages for Exascale Machines (Invited Talk) PEPM Alex Aiken Stanford University | ||
11:30 30mTalk | Checking Cryptographic API Usage with Composable Annotations (Short Paper) PEPM Duncan Mitchell Royal Holloway, University of London, L. Thomas van Binsbergen Royal Holloway University of London, Blake Loring , Johannes Kinder Royal Holloway, University of London DOI | ||
10:30 - 12:00 | |||
10:30 30mTalk | Very Large Scale Network Verification NetPL Andrey Rybalchenko Microsoft Research | ||
11:00 60mOther | Working Groups NetPL | ||
10:30 - 12:00 | |||
10:30 30mTalk | A Verified SAT Solver with Watched Literals Using Imperative HOL CPP Mathias Fleury MPI-INF, Jasmin Blanchette Vrije Universiteit Amsterdam, Peter Lammich Technische Universität München DOI | ||
11:00 30mTalk | Œuf: Minimizing the Coq Extraction TCB CPP Eric Mullen University of Washington, Stuart Pernsteiner University of Washington, USA, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle, Dan Grossman University of Washington DOI | ||
11:30 30mTalk | Proofs in Conflict-Driven Theory Combination CPP Maria Paola Bonacina University of Verona, Italy, Stéphane Graham-Lengrand CNRS, France, Natarajan Shankar SRI International, USA DOI | ||
10:30 - 12:00 | |||
10:30 90mTalk | Panel I: Technical Trends in Programming Languages Research PLMW Aws Albarghouthi University of Wisconsin-Madison, Constantin Enea Université Paris Diderot, David Walker Princeton University, Andrew Myers Cornell University | ||
10:30 - 12:00 | |||
10:30 30mTalk | Hygienic Source-Code Generation Using Functors PADL | ||
11:00 30mTalk | Snaarkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell PADL | ||
11:30 30mTalk | Rewriting High-Level Spreadsheet Structures into Higher-Order Functional Programs PADL A: Florian Biermann IT University of Copenhagen, Wensheng Dou Institute of Software, Chinese Academy of Sciences, China, A: Peter Sestoft IT University of Copenhagen | ||
10:30 - 12:00 | |||
10:30 30mTalk | Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity VMCAI | ||
11:00 30mTalk | Automatic Verification of Intermittent Systems VMCAI | ||
11:30 30mTalk | Co-Design and Verification of an Available File System VMCAI | ||
13:30 - 15:30 | |||
14:00 30mOther | Working Groups Debrief NetPL | ||
14:30 30mTalk | Safety Verification of Stateful Networks NetPL Sharon Shoham Tel Aviv university | ||
15:00 30mTalk | Understand and verify your network using Header Space Analysis NetPL Peyman Kazemian Forward Networks | ||
13:30 - 15:30 | Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A Chair(s): Thorsten Altenkirch University of Nottingham | ||
13:30 30mTalk | Finite Sets in Homotopy Type Theory CPP Dan Frumin Radboud University, Herman Geuvers Radboud University Nijmegen, Netherlands, Léon Gondelman LRI, Université Paris-Sud, Niels van der Weide Radboud University Nijmegen, Netherlands DOI | ||
14:00 30mTalk | Generic Derivation of Induction for Impredicative Encodings in Cedille CPP DOI | ||
14:30 30mTalk | Large Model Constructions for Second-Order ZF in Dependent Type Theory CPP DOI | ||
15:00 30mTalk | A Constructive Formalisation of Semi-algebraic Sets and Functions CPP Boris Djalal INRIA | ||
13:30 - 15:30 | |||
14:00 30mTalk | Dafny Overview PLMW K. Rustan M. Leino Amazon Media Attached File Attached | ||
14:30 30mTalk | The Curse of Knowledge PLMW Benjamin C. Pierce University of Pennsylvania Media Attached | ||
15:00 30mTalk | How to Give Talks That People Can Follow PLMW Derek Dreyer MPI-SWS Media Attached | ||
13:30 - 15:30 | |||
13:30 30mTalk | Automatic Web Services Composition for Phylotastic PADL | ||
14:00 30mTalk | Navigating Online Semantic Resources for Entity Set Expansion PADL | ||
14:30 30mTalk | A REST-based Development Framework for ASP: Tools and Application PADL A: Gelsomina Catalano , A: Giovanni Laboccetta , A: Kristian Reale , A: Francesco Ricca , A: Pierfrancesco Veltri | ||
15:00 30mTalk | LoIDE: a a web-based IDE for Logic Programming - Preliminary Report PADL | ||
14:00 - 15:30 | |||
14:00 60mTalk | Deep Probabilistic Programming: TensorFlow Distributions and Edward PPS | ||
15:00 30mTalk | More support for symbolic disintegration PPS | ||
14:00 - 15:30 | |||
14:00 30mTalk | Partially Static Data as Free Extension of Algebras (Short Paper) PEPM Jeremy Yallop University of Cambridge, UK, Tamara von Glehn University of Cambridge, Ohad Kammar University of Oxford Pre-print | ||
14:30 30mTalk | Program Generation for ML Modules (Short Paper) PEPM DOI | ||
15:00 30mTalk | Recursive Programs in Normal Form (Short Paper) PEPM Barry Jay University of Technology Sydney DOI | ||
14:00 - 15:30 | |||
14:00 30mTalk | From Shapes to Amortized Complexity VMCAI Tomas Fiedor VUT Brno, Lukáš Holík Brno University of Technology, Adam Rogalewicz Brno University of Technology , Moritz Sinn St. Polten University of Applied Sciences, Tomáš Vojnar Brno University of Technology, Florian Zuleger TU Vienna | ||
14:30 30mTalk | Invariant Generation for Multi-Path Loops with Polynomial Assignments VMCAI Andreas Humenberger Vienna University of Technology, Maximilian Jaroschek Vienna University of Technology, Laura Kovacs Chalmers University of Technology | ||
15:00 30mTalk | Refinement Types for Ruby VMCAI Milod Kazerounian , Niki Vazou University of Maryland, Austin Bourgerie University of Maryland, Jeffrey S. Foster University of Maryland, College Park, Emina Torlak University of Washington | ||
16:00 - 18:00 | |||
16:00 30mTalk | Auxiliary variables in Probabilistic Programs PPS | ||
16:30 30mTalk | Probabilistic Program Inference With Abstractions PPS Steven Holtzen University of California, Los Angeles, Guy Van den Broeck University of California, Los Angeles, Todd Millstein University of California, Los Angeles Pre-print | ||
17:00 30mTalk | SlicStan: Improving Probabilistic Programming using Information Flow Analysis PPS Maria I. Gorinova The University of Edinburgh, Andrew D. Gordon Microsoft Research and University of Edinburgh, Charles Sutton University of Edinburgh Pre-print | ||
17:30 30mTalk | Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion PPS Mitchell Wand Northeastern University, USA, Theophilos Giannakopoulos BAE Systems, Inc., Andrew Cobb Northeastern University, Ryan Culpepper Northeastern University | ||
16:00 - 17:30 | |||
16:00 10mTalk | Towards Language-independent Code Synthesis (Poster/Demo Talk) PEPM Jan Bessai Technical University Dortmund, Boris Düdder University of Copenhagen, George Heineman Worcester Polytechnic Institute, Jakob Rehof Technical University Dortmund File Attached | ||
16:10 10mTalk | Dataflow Metaprogramming (Poster/Demo Talk) PEPM | ||
16:20 10mTalk | An Approach to Generating Text-Based IDEs with Syntax Completion (Poster/Demo Talk) PEPM Isao Sasano Shibaura Institute of Technology | ||
16:30 10mTalk | Modular Macros (Poster/Demo Talk) PEPM File Attached | ||
16:40 10mTalk | Equations: From Clauses to Splittings to Functions (Poster/Demo Talk) PEPM File Attached | ||
16:50 40mOther | Posters/Demos PEPM | ||
16:00 - 18:00 | |||
16:00 30mTalk | P4: A Language for Data Plane Programming NetPL Calin Cascaval Barefoot Networks | ||
16:30 30mTalk | A Vision for Network Design Automation NetPL George Varghese UCLA | ||
17:00 30mOther | Panel NetPL Nate Foster Cornell University, David Walker Princeton University, Barath Raghavan ICSI, Jonathan Smith DARPA | ||
17:30 30mDay closing | Wrap Up NetPL Marco Canini KAUST, Nate Foster Cornell University, Todd Millstein University of California, Los Angeles | ||
16:00 - 18:00 | |||
16:00 30mTalk | HOpi in Coq CPP DOI | ||
16:30 30mTalk | A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory CPP DOI | ||
17:00 30mTalk | A Two-Level Logic Perspective on (Simultaneous) Substitutions CPP Kaustuv Chaudhuri Inria, France DOI | ||
17:30 30mTalk | Binder Aware Recursion over Well-Scoped de Bruijn Syntax CPP DOI | ||
16:00 - 18:00 | |||
16:00 30mTalk | Work-Life Balance? PLMW Andrew Myers Cornell University File Attached | ||
16:30 90mTalk | Panel II: Life in Grad School (and Beyond) PLMW Azadeh Farzan University of Toronto, Zachary Tatlock University of Washington, Seattle, Thomas Ball Microsoft Research, Jennifer Paykin University of Pennsylvania | ||
16:00 - 18:00 | |||
16:00 30mTalk | Probabilistic Functional Logic Programming PADL A: Sandra Dylus University of Kiel, Germany, A: Jan Christiansen Flensburg University of Applied Sciences, Germany, A: Finn Teegen University of Kiel, Germany | ||
16:30 30mTalk | Optimizing Answer Set Computation via Heuristic-Based Decomposition PADL A: Francesco Calimeri University of Calabria, A: Davide Fuscà , A: Simona Perri , A: Jessica Zangari | ||
17:00 30mDay closing | Closing PADL | ||
16:00 - 17:30 | |||
16:00 30mTalk | Learning to Complement Büchi Automata VMCAI Yong Li Institute of Software, Chinese Academy of Sciences, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool | ||
16:30 30mTalk | Selfless Interpolation for Infinite-State Model Checking VMCAI | ||
17:00 30mTalk | Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction VMCAI Benjamin Aminof Vienna University of Technology, Sasha Rubin University of Naples Federico II, Ilina Stoilkovska Vienna University of Technology , Josef Widder TU Wien, Florian Zuleger TU Vienna | ||
Wed 10 JanDisplayed time zone: Tijuana, Baja California change
Wed 10 Jan
Displayed time zone: Tijuana, Baja California change
08:30 - 10:00 | Awards & Keynote-IResearch Papers at Bunker Hill / Watercourt Chair(s): Ranjit Jhala University of California, San Diego | ||
08:30 5mDay opening | Welcome to POPL 2018 Research Papers | ||
08:35 10mAwards | SIGPLAN Awards Research Papers Satnam Singh X, the moonshot factory | ||
08:45 60mTalk | Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and Now You Can) Research Papers Derek Dreyer MPI-SWS | ||
09:45 20mTalk | Lightning Overview - Day 1 Research Papers | ||
10:30 - 12:10 | |||
10:30 25mTalk | Synthesizing Bijective Lenses Research Papers Anders Miltner Princeton University, Kathleen Fisher Tufts University, Benjamin C. Pierce University of Pennsylvania, David Walker Princeton University, Steve Zdancewic University of Pennsylvania | ||
10:55 25mTalk | WebRelate: Integrating Web Data with Spreadsheets using Examples Research Papers | ||
11:20 25mTalk | What's Decidable About String Constraints with ReplaceAll Function? Research Papers Taolue Chen Birkbeck, University of London, Yan Chen State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences, Matthew Hague Royal Holloway, University of London, Anthony Widjaja Lin Oxford University, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences | ||
11:45 25mTalk | String Constraints with Concatenation and Transducers Solved Efficiently Research Papers Lukáš Holík Brno University of Technology, Anthony Widjaja Lin Oxford University, Petr Janků Brno University of Technology, Philipp Ruemmer Uppsala University, Tomáš Vojnar Brno University of Technology | ||
10:30 - 12:10 | Types and EffectsResearch Papers at Watercourt Chair(s): Neel Krishnaswami Computer Laboratory, University of Cambridge | ||
10:30 25mTalk | Linear Haskell: practical linearity in a higher-order polymorphic language Research Papers Jean-Philippe Bernardy University of Gothenburg, Mathieu Boespflug Tweag I/O, Ryan R. Newton Indiana University, Simon Peyton Jones Microsoft Research, Arnaud Spiwack Tweag I/O Pre-print File Attached | ||
10:55 25mTalk | Polyadic Approximations, Fibrations and Intersection Types Research Papers | ||
11:20 25mTalk | Handling fibred algebraic effects Research Papers Danel Ahman Inria Paris | ||
11:45 25mTalk | Handle with Care: Relational Interpretation of Algebraic Effects and Handlers 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 | ||
12:10 - 13:40 | |||
12:10 90mLunch | Wednesday Lunch Research Papers | ||
13:40 - 15:20 | |||
13:40 25mTalk | Automated Lemma Synthesis in Symbolic-Heap Separation Logic Research Papers Quang-Trung Ta National University of Singapore, Ton Chanh Le National University of Singapore, Siau-Cheng Khoo National University of Singapore, Wei-Ngan Chin National University of Singapore | ||
14:05 25mTalk | Foundations for Natural Proofs and Quantifier Instantiation Research Papers Christof Löding RWTH Aachen University, P. Madhusudan University of Illinois at Urbana-Champaign, Lucas Peña University of Illinois at Urbana-Champaign | ||
14:30 25mTalk | Higher-Order Constrained Horn Clauses for Verification Research Papers Toby Cathcart Burn University of Oxford, C.-H. Luke Ong University of Oxford, Steven Ramsay University of Bristol | ||
14:55 25mTalk | Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs Research Papers Hiroshi Unno University of Tsukuba, Yuki Satake University of Tsukuba, Tachio Terauchi Waseda University | ||
13:40 - 15:20 | Interpretation and EvaluationResearch Papers at Watercourt Chair(s): Atsushi Igarashi Kyoto University, Japan | ||
13:40 25mTalk | Unifying Analytic and Statically-Typed Quasiquotes Research Papers Lionel Parreaux EPFL, Antoine Voizard University of Pennsylvannia, Amir Shaikhha EPFL, Christoph E. Koch EPFL Pre-print | ||
14:05 25mTalk | Jones-Optimal Partial Evaluation by Specialization-Safe Normalization Research Papers | ||
14:30 25mTalk | Migrating Gradual Types Research Papers John Peter Campora ULL Lafayette, Sheng Chen University of Louisiana at Lafayette, Martin Erwig Oregon State University, Eric Walkingshaw Oregon State University | ||
14:55 25mTalk | Intrinsically-Typed Definitional Interpreters for Imperative Languages Research Papers Casper Bach Poulsen Delft University of Technology, Arjen Rouvoet Delft University of Technology, Andrew Tolmach Portland State University, Robbert Krebbers Delft University of Technology, Eelco Visser Delft University of Technology DOI Pre-print | ||
15:50 - 17:30 | |||
15:50 25mTalk | Effective Stateless Model Checking for C/C++ Concurrency Research Papers Michalis Kokologiannakis National Technical University of Athens, Greece, Ori Lahav Tel Aviv University, Israel, Konstantinos (Kostis) Sagonas , Viktor Vafeiadis MPI-SWS, Germany | ||
16:15 25mTalk | Transactions in Relaxed Memory Architectures Research Papers Brijesh Dongol Brunel University London, Radha Jagadeesan DePaul University, James Riely DePaul University Link to publication DOI Pre-print Media Attached | ||
16:40 25mTalk | Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Research Papers Christopher Pulte University of Cambridge, Shaked Flur University of Cambridge, Will Deacon ARM Ltd., Jon French University of Cambridge, Susmit Sarkar University of St. Andrews, Peter Sewell University of Cambridge | ||
17:05 25mTalk | Progress of Concurrent Objects with Partial Methods Research Papers Hongjin Liang University of Science and Technology of China, Xinyu Feng University of Science and Technology of China | ||
15:50 - 17:30 | |||
15:50 25mTalk | A Principled approach to Ornamentation in ML Research Papers | ||
16:15 25mTalk | Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible Research Papers William J. Bowman Northeastern University, USA, Youyou Cong Ochanomizu University, Japan, Nick Rioux Northeastern University, USA, Amal Ahmed Northeastern University, USA Link to publication DOI Pre-print | ||
16:40 25mTalk | Safety and Conservativity of Definitions in HOL and Isabelle/HOL Research Papers | ||
17:05 25mTalk | Univalent Higher Categories via Complete Semi-Segal Types Research Papers | ||
19:00 - 22:00 | |||
19:00 3hDinner | POPL Banquet Research Papers | ||
Thu 11 JanDisplayed time zone: Tijuana, Baja California change
Thu 11 Jan
Displayed time zone: Tijuana, Baja California change
08:30 - 10:00 | |||
08:30 60mTalk | Some Principles of Differential Programming Languages Research Papers Gordon Plotkin University of Edinburgh, UK | ||
09:30 30mTalk | Lightning Overview - Day 2 Research Papers | ||
10:30 - 12:10 | ConsistencyResearch Papers at Bunker Hill Chair(s): Xinyu Feng University of Science and Technology of China | ||
10:30 25mTalk | Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections Research Papers | ||
10:55 25mTalk | Reducing Liveness to Safety in First-Order Logic Research Papers Oded Padon Tel Aviv University, Jochen Hoenicke Universität Freiburg, Giuliano Losa University of California at Los Angeles, USA, Andreas Podelski University of Freiburg, Germany, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university | ||
11:20 25mTalk | Alone Together: Compositional Reasoning and Inference for Weak Isolation Research Papers Gowtham Kaki Purdue University, Kartik Nagar Purdue University, Mahsa Najafzadeh Purdue University, Suresh Jagannathan Purdue University | ||
11:45 25mTalk | Programming and Proving with Distributed Protocols Research Papers Ilya Sergey University College London, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle DOI Pre-print | ||
10:30 - 12:10 | |||
10:30 25mTalk | Inference of Static Semantics for Incomplete C Programs Research Papers Leandro T. C. Melo UFMG, Rodrigo Geraldo Ribeiro UFOP, Marcus Rodrigues de Araújo UFMG, Fernando Magno Quintão Pereira UFMG Pre-print | ||
10:55 25mTalk | Optimal Dyck Reachability for Data-dependence and Alias Analysis Research Papers | ||
11:20 25mTalk | Data-centric Dynamic Partial Order Reduction Research Papers Marek Chalupa Masaryk University, Krishnendu Chatterjee IST Austria, Andreas Pavlogiannis IST Austria, Kapil Vaidya IIT Bombay, Nishant Sinha IBM Research | ||
11:45 25mTalk | Analytical Modeling of Cache Behavior for Affine Programs Research Papers Wenlei Bao Ohio State University, Sriram Krishnamoorthy Pacific Northwest National Laboratories, Louis-Noël Pouchet Colorado State University, P. Sadayappan Ohio State University | ||
12:10 - 13:40 | |||
12:10 90mLunch | Thursday Lunch Research Papers | ||
13:40 - 15:20 | |||
13:40 25mTalk | A new proof rule for almost-sure termination Research Papers Annabelle McIver Macquarie University, Carroll Morgan University of New South Wales; Data 61, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University | ||
14:05 25mTalk | Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs Research Papers | ||
14:30 25mTalk | Algorithmic Analysis of Termination Problems for Quantum Programs Research Papers Yangjia Li Institute of Software, Chinese Academy of Sciences, Mingsheng Ying University of Technology Sydney | ||
14:55 25mTalk | Monadic refinements for relational cost analysis Research Papers Ivan Radicek TU Vienna, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Florian Zuleger TU Vienna | ||
13:40 - 15:20 | |||
13:40 25mTalk | Go with the Flow: Compositional Abstractions for Concurrent Data Structures Research Papers Siddharth Krishna New York University, Dennis Shasha New York University, Thomas Wies New York University | ||
14:05 25mTalk | Parametricity versus the Universal Type Research Papers | ||
14:30 25mTalk | Linearity in Higher-Order Recursion Schemes Research Papers Pierre Clairambault CNRS & ENS Lyon, Charles Grellois INRIA Sophia Antipolis & Aix-Marseille Université, Andrzej Murawski University of Oxford | ||
14:55 25mTalk | Symbolic Types for Lenient Symbolic Execution Research Papers Stephen Chang Northeastern University, Alex Knauth Northeastern University, Emina Torlak University of Washington | ||
15:50 - 16:40 | Language DesignResearch Papers at Bunker Hill Chair(s): Zachary Tatlock University of Washington, Seattle | ||
15:50 25mTalk | An Axiomatic Basis for Bidirectional Programming Research Papers Hsiang-Shang ‘Josh’ Ko National Institute of Informatics, Japan, Zhenjiang Hu National Institute of Informatics Link to publication DOI Pre-print Media Attached File Attached | ||
16:15 25mTalk | Simplicitly: Foundations and Applications of Implicit Function Types Research Papers Martin Odersky EPFL, Switzerland, Olivier Blanvillain EPFL, Fengyun Liu EPFL, Switzerland, Aggelos Biboudis Ecole Polytechnique Federale de Lausanne, Heather Miller Ecole Polytechnique Federale de Lausanne, Sandro Stucki EPFL | ||
15:50 - 16:40 | |||
15:50 25mTalk | Up-to Techniques Using Sized Types Research Papers Nils Anders Danielsson University of Gothenburg, Chalmers University of Technology | ||
16:15 25mTalk | Decidability of Conversion for Type Theory in Type Theory Research Papers Andreas Abel Gothenburg University, Joakim Öhman IMDEA Software Institute, Andrea Vezzosi Chalmers University of Technology | ||
17:00 - 18:00 | Business MeetingResearch Papers at Bunker Hill / Watercourt Chair(s): Ranjit Jhala University of California, San Diego, Andrew Myers Cornell University | ||
17:00 20mTalk | Chairs' Report Research Papers | ||
17:20 10mTalk | POPL 2019 Preview Research Papers | ||
17:30 30mTalk | SIGPLAN Town Hall Research Papers | ||
18:15 - 20:15 | |||
18:15 2hOther | POPL Poster Session Research Papers | ||
Fri 12 JanDisplayed time zone: Tijuana, Baja California change
Fri 12 Jan
Displayed time zone: Tijuana, Baja California change
08:30 - 10:00 | |||
08:30 60mTalk | Formal Methods and the Law Research Papers | ||
09:30 30mTalk | Lightning Overview - Day 3 Research Papers | ||
10:30 - 12:10 | Testing and VerificationResearch Papers at Bunker Hill Chair(s): Santosh Nagarakatte Rutgers University, USA | ||
10:30 25mTalk | Generating Good Generators for Inductive Relations Research Papers Leonidas Lampropoulos University of Pennsylvania, Zoe Paraskevopoulou Princeton University, Benjamin C. Pierce University of Pennsylvania | ||
10:55 25mTalk | Why is Random Testing Effective for Partition Tolerance Bugs? Research Papers | ||
11:20 25mTalk | On Automatically Proving the Correctness of math.h Implementations Research Papers | ||
11:45 25mTalk | Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Research Papers Shelly Grossman Tel Aviv University, Ittai Abraham VMWare Research, Guy Gueta VMWare Research, Yan Michalevsky Stanford University, Noam Rinetzky Tel Aviv University, Mooly Sagiv Tel Aviv University, Yoni Zohar Tel Aviv University | ||
10:30 - 12:00 | |||
10:30 15mTalk | Graduate Finalist 1 Student Research Competition | ||
10:45 15mTalk | Graduate Finalist 2 Student Research Competition | ||
11:00 15mTalk | Graduate Finalist 3 Student Research Competition | ||
11:15 15mTalk | Undergraduate Finalist 1 Student Research Competition | ||
11:30 15mTalk | Undergraduate Finalist 2 Student Research Competition | ||
11:45 15mTalk | Undergraduate Finalist 3 Student Research Competition | ||
10:30 - 12:10 | |||
10:30 25mTalk | Correctness of Speculative Optimizations with Dynamic Deoptimization Research Papers Olivier Flückiger Northeastern University, USA, Gabriel Scherer Northeastern University, USA, Ming-Ho Yee Northeastern University, USA, Aviral Goel Northeastern University, Amal Ahmed Northeastern University, USA, Jan Vitek Northeastern University DOI Pre-print | ||
10:55 25mTalk | JaVerT: JavaScript Verification Toolchain Research Papers José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, Daiva Naudžiūnienė Imperial College London, Thomas Wood Imperial College London, Philippa Gardner Imperial College London | ||
11:20 25mTalk | Soft Contract Verification for Higher-order Stateful Programs Research Papers Phúc C. Nguyễn University of Maryland, Thomas Gilray University of Maryland, Sam Tobin-Hochstadt Indiana University, David Van Horn University of Maryland | ||
11:45 25mTalk | Collapsing Towers of Interpreters Research Papers | ||
12:10 - 13:30 | |||
12:10 80mLunch | Friday Lunch Research Papers | ||
13:30 - 15:20 | |||
13:30 10mAwards | SRC Awards Research Papers Benjamin Delaware Purdue University | ||
13:30 22mTalk | Refinement Reflection: Complete Verification with SMT Research Papers Niki Vazou University of Maryland, Anish Tondwalkar UCSD, Vikraman Choudhury , Ryan Scott Indiana University, Ryan R. Newton Indiana University, Philip Wadler University of Edinburgh, UK, Ranjit Jhala University of California, San Diego | ||
14:05 25mTalk | Non-Linear Reasoning For Invariant Synthesis Research Papers Zachary Kincaid Princeton University, John Cyphert University of Wisconsin - Madison, Jason Breck University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. | ||
14:30 25mTalk | A Practical Construction for Decomposing Numerical Abstract Domains Research Papers | ||
14:55 25mTalk | Verifying Equivalence of Database-Driven Applications Research Papers Yuepeng Wang University of Texas at Austin, Işıl Dillig UT Austin, Shuvendu K. Lahiri Microsoft Research, William Cook University of Texas at Austin | ||
13:40 - 15:20 | |||
13:40 25mTalk | Proving expected sensitivity of probabilistic programs Research Papers Gilles Barthe IMDEA Software Institute, Thomas Espitau Universite Pierre et Marie Curie, Benjamin Gregoire INRIA, Justin Hsu University College London, Pierre-Yves Strub Ecole Polytechnique | ||
14:05 25mTalk | Synthesizing Coupling Proofs of Differential Privacy Research Papers | ||
14:30 25mTalk | Measurable cones and stable, measurable functions Research Papers Thomas Ehrhard CNRS and University Paris Diderot, Michele Pagani University Paris Diderot, Christine Tasson University Paris Diderot | ||
14:55 25mTalk | Denotational validation of higher-order Bayesian inference Research Papers Adam Ścibior University of Cambridge and MPI Tuebingen, Ohad Kammar University of Oxford, Matthijs Vákár University of Oxford, Sam Staton University of Oxford, Hongseok Yang University of Oxford, Yufei Cai University of Tuebingen, Klaus Ostermann University of Tuebingen, Sean Moss University of Oxford, Chris Heunen University of Edinburgh, Zoubin Ghahramani University of Cambridge | ||
15:50 - 17:05 | SynthesisResearch Papers at Bunker Hill Chair(s): Nadia Polikarpova University of California, San Diego | ||
15:50 25mTalk | Strategy Synthesis for Linear Arithmetic Games Research Papers | ||
16:15 25mTalk | Bonsai: Synthesis-Based Reasoning for Type Systems Research Papers | ||
16:40 25mTalk | Program Synthesis using Abstraction Refinement Research Papers | ||
15:50 - 17:05 | Types for StateResearch Papers at Watercourt Chair(s): Neel Krishnaswami Computer Laboratory, University of Cambridge | ||
15:50 25mTalk | A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST Research Papers Amin Timany imec-Distrinet KU-Leuven, Leo Stefanesco ENS Lyon, Morten Krogh-Jespersen Aarhus University, Lars Birkedal Aarhus University | ||
16:15 25mTalk | Recalling a Witness: Foundations and Applications of Monotonic State Research Papers Danel Ahman Inria Paris, Cédric Fournet Microsoft Research, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris and ENS Paris, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research Pre-print | ||
16:40 25mTalk | RustBelt: Securing the Foundations of the Rust Programming Language Research Papers Ralf Jung MPI-SWS, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Robbert Krebbers Delft University of Technology, Derek Dreyer MPI-SWS | ||
Sat 13 JanDisplayed time zone: Tijuana, Baja California change
Sat 13 Jan
Displayed time zone: Tijuana, Baja California change
09:00 - 10:00 | |||
09:00 60mTalk | Keynote: Programming and proving with FoCaLiZe: a tour from computer algebra to interoperability applications Off the Beaten Track Catherine Dubois ENSIIE Paris-Evry File Attached | ||
09:00 - 10:00 | |||
09:00 10mTalk | PriSC Welcome PriSC Cătălin Hriţcu Inria Paris File Attached | ||
09:10 50mTalk | Challenges For Compiler-backed Security: From Sanitizer to Mitigation (Invited Talk) PriSC Mathias Payer Purdue University File Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | CoqHammer: Strong Automation for Program Verification CoqPL File Attached | ||
10:30 - 12:00 | |||
10:30 30mTalk | Synthesizing Program-Specific Static Analyses Off the Beaten Track Colin Gordon Drexel University File Attached | ||
11:00 30mTalk | On quantifying the degree of unsoundness of static analyses Off the Beaten Track Dimitrios Vardoulakis Google File Attached | ||
11:30 30mTalk | Explaining Type Errors Off the Beaten Track Brent Yorgey Hendrix College, Richard A. Eisenberg Bryn Mawr College, USA, Harley D. Eades III Augusta University File Attached | ||
10:30 - 11:30 | |||
10:30 30mTalk | Linear capabilities for modular fully-abstract compilation of verified code PriSC File Attached | ||
11:00 30mTalk | Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities PriSC File Attached | ||
10:30 - 12:10 | |||
10:30 25mTalk | A “destruct” Tactic for Mtac2 CoqPL File Attached | ||
10:55 25mTalk | Typed Template Coq CoqPL Simon Boulier , Matthieu Sozeau Inria, Nicolas Tabareau Inria, France, Abhishek Anand Cornell University File Attached | ||
11:20 25mTalk | Elpi: an extension language for Coq CoqPL Enrico Tassi INRIA File Attached | ||
11:45 25mTalk | Coqatoo: Generating Natural Language Versions of Coq Proofs CoqPL Andrew Bedford Laval University File Attached | ||
11:30 - 12:00 | |||
11:30 5mTalk | Short talk: The Meaning of Memory Safety PriSC Arthur Azevedo de Amorim Carnegie Mellon University, USA, Cătălin Hriţcu Inria Paris, Benjamin C. Pierce University of Pennsylvania Pre-print File Attached | ||
11:35 5mTalk | Short talk: Dependently Typed Assembly for Secure Linking PriSC William J. Bowman Northeastern University, USA Link to publication File Attached | ||
11:40 5mTalk | Short talk: Compiler Optimizations with Retrofitting Transformations: Is there a Semantic Mismatch? PriSC Santosh Nagarakatte Rutgers University, USA Pre-print File Attached | ||
11:45 5mTalk | Short Talk: Secure compilation from F* to WebAssembly PriSC Jonathan Protzenko Microsoft Research, n.n. File Attached | ||
13:30 - 15:30 | Session 2Off the Beaten Track at Crocker Chair(s): William E. Byrd University of Alabama at Birmingham, USA | ||
13:30 30mLunch | Lunch (12pm-2pm) Off the Beaten Track | ||
14:00 30mTalk | SweetPea: A Language for Designing Experiments Off the Beaten Track Annie Cherkaev University of Utah, Sebastian Musslick Princeton University, Jonathan Cohen Princeton University, Vivek Srikumar University of Utah, Matthew Flatt University of Utah File Attached | ||
14:30 30mTalk | Extensible Semantics for Fluidics Off the Beaten Track File Attached | ||
15:00 30mTalk | Towards Proof Synthesis by Neural Machine Translation Off the Beaten Track Taro Sekiyama IBM Research, Japan, Akifumi Imanishi Kyoto University, Kohei Suenaga Graduate School of Informatics, Kyoto University File Attached | ||
13:30 - 15:30 | |||
13:30 30mTalk | Building Secure SGX Enclaves using F*, C/C++ and X64 PriSC File Attached | ||
14:00 30mTalk | Robust Hyperproperty Preservation for Secure Compilation PriSC Deepak Garg Max Planck Institute for Software Systems, Cătălin Hriţcu Inria Paris, Marco Patrignani Saarland University, CISPA, Marco Stronati , David Swasey MPI-SWS Pre-print File Attached | ||
14:30 30mTalk | Formally Secure Compilation of Unsafe Low-Level Components PriSC Guglielmo Fachini Inria Paris, Cătălin Hriţcu Inria Paris, Marco Stronati , Ana Nora Evans University of Virginia, USA, Théo Laurent , Arthur Azevedo de Amorim Carnegie Mellon University, USA, Benjamin C. Pierce University of Pennsylvania, Andrew Tolmach Portland State University Pre-print File Attached | ||
15:00 30mTalk | Secure Compilation in a Production Environment PriSC Vijay D'Silva Google File Attached | ||
14:00 - 14:50 | |||
14:00 25mTalk | Locally Nameless at Scale CoqPL Stephanie Weirich University of Pennsylvania, USA, Antoine Voizard University of Pennsylvannia, Anastasiya Kravchuk-Kirilyuk University of Pennsylvania File Attached | ||
14:25 25mTalk | A Coq Formalisation of a Core of R CoqPL Martin Bodin CMM File Attached | ||
14:50 - 15:30 | |||
14:50 40mTalk | Session with the Coq Development Team CoqPL File Attached | ||
16:00 - 18:00 | |||
16:00 30mTalk | Back to the Future with Denotational Semantics Off the Beaten Track Jeremy G. Siek Indiana University, USA File Attached | ||
16:30 30mTalk | Climbing Up the Semantic Tower — at Runtime Off the Beaten Track File Attached | ||
17:00 30mTalk | Towards A Systems Approach To Distributed Programming Off the Beaten Track Christopher Meiklejohn Université catholique de Louvain, Peter Van Roy Université catholique de Louvain File Attached | ||
17:30 30mDay closing | Discussion and business meeting Off the Beaten Track | ||
16:00 - 18:00 | |||
16:00 30mTalk | Constant-time WebAssembly PriSC Pre-print File Attached | ||
16:30 30mTalk | Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs PriSC Rob Sison Data61, CSIRO and UNSW File Attached | ||
17:00 30mTalk | On Compositional Compiler Correctness and Fully Abstract Compilation PriSC File Attached | ||
17:30 30mTalk | Foundations of Dependent Interoperability PriSC Link to publication File Attached | ||
16:00 - 18:05 | |||
16:00 25mTalk | Phantom Types for Quantum Programs CoqPL Robert Rand University of Pennsylvania, Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of Pennsylvania File Attached | ||
16:25 25mTalk | Revisiting Parametricity: Inductives and Uniformity of Propositions CoqPL File Attached | ||
16:50 25mTalk | Towards Context-Aware Data Refinement CoqPL Paul Krogmeier Purdue University, Steven Kidd Purdue University, Benjamin Delaware Purdue University File Attached | ||
17:15 25mTalk | Mechanizing the Construction and Rewriting of Proper Functions in Coq CoqPL Edwin Westbrook Galois, Inc. File Attached | ||
17:40 25mTalk | A calculus for logical refinements in separation logic CoqPL File Attached | ||