Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 15 JanDisplayed time zone: Eastern Time (US & Canada) change
Sun 15 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | Session #1ProLaLa at Kenmore Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond | ||
09:00 10mDay opening | Opening comments ProLaLa Jonathan Protzenko Microsoft Research, Redmond, Denis Merigoux INRIA, Shrutarshi Basu Middlebury College | ||
09:10 45mKeynote | Academic keynote : A Logician and Lawyer walk into a Classroom ProLaLa | ||
09:55 25mTalk | Formal Modeling and Analysis of Legal Contracts using ContractCheck ProLaLa Alan Khoja University of Konstanz, Martin Kölbl CertiK, Stefan Leue University of Konstanz, Rüdiger Wilhelmi University of Konstanz DOI Pre-print | ||
10:20 10mTalk | What do Relational Properties Have to Say About Legal Expert Systems ? ProLaLa Arthur Correnson École Normale Supérieure de Rennes & Saarland University |
09:00 - 10:30 | First SessionLAFI at Scollay Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6 | ||
09:00 5mDay opening | Opening Comments LAFI | ||
09:05 60mKeynote | Introduction to the tensor-programs framework, a PL approach that helps analyse theoretical properties of deep learning.Boston LAFI | ||
10:10 10mTalk | Exact Inference for Discrete Probabilistic Programs via Generating FunctionsParis LAFI File Attached | ||
10:20 10mTalk | Exact Probabilistic Inference Using Generating FunctionsBoston LAFI A: Lutz Klinkenberg RWTH Aachen University, Tobias Winkler RWTH Aachen University, Mingshuai Chen RWTH Aachen, Joost-Pieter Katoen RWTH Aachen University File Attached |
14:00 - 15:30 | Session #3ProLaLa at Kenmore Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond, Emma Tosch Northeastern University, USA | ||
14:00 25mTalk | Experience report: implementing a real-world, medium-sized program derived from a legislative specification ProLaLa Denis Merigoux INRIA Pre-print File Attached | ||
14:25 25mTalk | Legal Contracts Amending in StipulaVirtual ProLaLa Cosimo Laneve University of Bologna, Alessandro Parenti University of Bologna, Giovanni Sartor University of Bologna | ||
14:50 25mTalk | Towards an Automatic Consolidation of French LawVirtual ProLaLa Georges-André Silber Mines Paris, PSL University File Attached | ||
15:15 10mTalk | DCR Graphs as Co-created Executable Models of the Law ProLaLa Thomas T. Hildebrandt University of Copenhagen File Attached | ||
15:25 10mTalk | Visual Propositional Logic With yscriptVirtual ProLaLa William O'Hanley Stanford CodeX Link to publication |
16:00 - 18:00 | Session #4ProLaLa at Kenmore Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond | ||
16:00 45mKeynote | Research keynote ProLaLa Chris Bailey University of Illinois College of Law | ||
16:45 25mTalk | Designing an experiment for comparing user interfaces for legal formalization ProLaLa | ||
17:10 10mTalk | Blawx: User-friendly Goal-Directed Answer Set Programming for Rules as CodeVirtual ProLaLa File Attached | ||
17:20 10mTalk | Formalising Criminal Law in CatalaVirtual ProLaLa Luca Arnaboldi The University of Edinburgh, David Aspinall University of Edinburgh, Ronny Bogani University of Edinburgh, Burkhard Schafer University of Edinburgh, Scott Herman Conan & Herman, Jonathan Protzenko Microsoft Research, Redmond, Ekaterina Komendantskaya Heriot-Watt University, UK, Remi Desmartin Heriot-Watt University, Yue Li Heriot-Watt University, UK Pre-print File Attached |
16:00 - 18:00 | |||
Mon 16 JanDisplayed time zone: Eastern Time (US & Canada) change
Mon 16 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | Towards a Theoretical Understanding of Property-Directed Reachability VMCAI Sharon Shoham Tel Aviv University | ||
10:00 30mTalk | Distributing and Parallelizing Non-canonical Loops VMCAI Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS |
09:00 - 10:30 | |||
09:00 90mTutorial | Deductive Verification of Probabilistic Programs TutorialFest Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU |
09:00 - 10:30 | |||
09:00 90mTutorial | QuickChick: Combining Random Testing and Verification in Coq TutorialFest Leonidas Lampropoulos University of Maryland, College Park |
09:00 - 10:30 | |||
09:00 90mTutorial | Isabelle/HOL: Foundations, Induction, and Coinduction TutorialFest |
09:00 - 10:30 | |||
09:00 90mTutorial | Z3 Internals – A guide to principles, art and empirics of programming SMT solvers TutorialFest Nikolaj Bjørner Microsoft Research |
09:00 - 10:30 | |||
09:00 60mKeynote | CompCert: a journey through the landscape of mechanized semantics for verified compilation CPP | ||
10:08 22mTalk | Mechanised Semantics for Gated Static Single Assignment CPP Yann Herklotz Imperial College London, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA DOI Pre-print |
09:00 - 10:00 | |||
09:00 60mTalk | Towards Declarative Content Generation for Creativity Support Tools PADL Chris Martens Northeastern University |
10:00 - 10:30 | |||
10:00 30mTalk | Using Hybrid Knowledge Bases for Meta-reasoning over OWL 2 QL PADL |
11:00 - 12:30 | |||
11:00 30mTalk | Efficient Interprocedural Data-Flow Analysis using Treedepth and Treewidth VMCAI | ||
11:30 30mTalk | Result Invalidation for Incremental Modular Analyses VMCAI Jens Van der Plas Software Languages Lab, Vrije Universiteit Brussel, Quentin Stiévenart Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel | ||
12:00 30mTalk | Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference VMCAI |
11:00 - 12:30 | |||
11:00 90mTutorial | Deductive Verification of Probabilistic Programs TutorialFest Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU |
11:00 - 12:30 | |||
11:00 90mTutorial | QuickChick: Combining Random Testing and Verification in Coq TutorialFest Leonidas Lampropoulos University of Maryland, College Park |
11:00 - 12:30 | |||
11:00 90mTutorial | Isabelle/HOL: Foundations, Induction, and Coinduction TutorialFest |
11:00 - 12:30 | |||
11:00 90mTutorial | Z3 Internals – A guide to principles, art and empirics of programming SMT solvers TutorialFest Nikolaj Bjørner Microsoft Research |
11:00 - 12:30 | Domain Specific LanguagesPADL at The Loft Chair(s): Sarat Chandra Varanasi The University of Texas at Dallas, General Electric Research | ||
11:00 30mTalk | Fluo: A Domain-Specific Language for Experiments in Fluorescence Microscopy (Application Paper) PADL | ||
11:30 30mTalk | SwitchLog: A Logic Programming Language for Network Switches PADL Vaibhav Mehta Princeton University, Devon Loehr Princeton University, John Sonchack University of Pennsylvania, USA, David Walker Princeton University | ||
12:00 30mTalk | Formalizing and Reasoning about Contracts between Agents PADL Dylan Flynn , Chasity Nadeau , Jeannine Shantz , Marcello Balduccini Saint Joseph's University, USA, Tran Cao Son New Mexico State University, Edward Griffor |
12:30 - 14:00 | |||
14:00 - 15:30 | |||
14:00 60mKeynote | What Can Program Analysis Say About Data Bias? VMCAI Aws Albarghouthi University of Wisconsin-Madison | ||
15:00 30mTalk | Bayesian parameter estimation with guarantees via interval analysis and simulation VMCAI Luisa Collodi University of Florence |
14:00 - 15:30 | |||
14:00 90mTutorial | Neurosymbolic Programming TutorialFest Swarat Chaudhuri University of Texas at Austin, Atharva Sehgal University of Texas, Austin, Armando Solar-Lezama Massachusetts Institute of Technology |
14:00 - 15:30 | |||
14:00 90mTutorial | RUST: Regions, Uniqueness, Ownership & Types TutorialFest Media Attached File Attached |
14:00 - 15:30 | |||
14:00 90mTutorial | Using a Proof Assistant to Teach PL Theory, Without the Overhead TutorialFest |
14:00 - 15:30 | |||
14:00 90mTutorial | Incorrectness Logic and Under-approximation: Foundations of Bug Catching TutorialFest Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London, Julien Vanegue Bloomberg, USA |
14:00 - 15:30 | |||
14:00 22mTalk | A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL CPP Katherine Kosaian Carnegie Mellon University, Yong Kiam Tan Carnegie Mellon University, André Platzer Karlsruhe Institute of Technology | ||
14:22 22mTalk | P4Cub: A Little Language for Big Routers CPP Rudy Peterson Cornell University, Eric Campbell Cornell University, John Chen Cornell University, Natalie Isak Microsoft, Calvin Shyu Cornell University, Ryan Doenges Cornell University, Parsia Ataei Cornell University, Nate Foster Cornell University | ||
14:45 22mTalk | ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER CPP Haobin Ni Cornell University, Antoine Delignat-Lavaud Microsoft Research, n.n., Cédric Fournet Microsoft Research, Tahina Ramananandro Microsoft Research, Nikhil Swamy Microsoft Research | ||
15:07 22mTalk | Verifying term graph optimizations using Isabelle/HOL CPP Brae J. Webb The University of Queensland, Ian J. Hayes The University of Queensland, Mark Utting The University of Queensland |
14:00 - 15:30 | Applications of Answer Set Programming (I)PADL at The Loft Chair(s): Wolfgang Faber Alpen-Adria-Universität, Austria | ||
14:00 30mTalk | Jury-trial Story Construction and Analysis using Goal-directed Answer Set Programming PADL Zesheng Xu The University of Texas at Dallas, Gopal Gupta University of Texas at Dallas, USA, Elmer Salazar The University of Texas at Dallas, Joaquín Arias Universidad Rey Juan Carlos, Sarat Chandra Varanasi The University of Texas at Dallas, General Electric Research | ||
14:30 30mTalk | Solving Vehicle Equipment Specification Problems with Answer Set Programming PADL Raito Takeuchi Nagoya University, Mutsunori Banbara Nagoya University, Naoyuki Tamura Kobe University, JAPAN, Torsten Schaub University of Potsdam | ||
15:00 30mTalk | Pruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance Scheduling PADL Anssi Yli-Jyrä Tampere University, Masood Feyzbakhsh Rankooh Tampere University, Tomi Janhunen Tampere University |
16:00 - 18:00 | |||
16:00 30mTalk | Solving Constrained Horn Clauses over Algebraic Data Types VMCAI Lucas Zavalia Florida State University Tallahassee, Lidiia Chernigovskaia , Grigory Fedyukovich Florida State University | ||
16:30 30mTalk | Satisfiability Modulo Custom Theories in Z3 (Tool Paper) VMCAI | ||
17:00 30mTalk | CosySEL: Improving SAT Solving Using Local Symmetries VMCAI |
16:00 - 17:30 | |||
16:00 90mTutorial | Neurosymbolic Programming TutorialFest Swarat Chaudhuri University of Texas at Austin, Atharva Sehgal University of Texas, Austin, Armando Solar-Lezama Massachusetts Institute of Technology |
16:00 - 17:30 | |||
16:00 90mTutorial | RUST: Regions, Uniqueness, Ownership & Types TutorialFest Media Attached File Attached |
16:00 - 17:30 | |||
16:00 90mTutorial | Using a Proof Assistant to Teach PL Theory, Without the Overhead TutorialFest |
16:00 - 17:30 | |||
16:00 90mTutorial | Incorrectness Logic and Under-approximation: Foundations of Bug Catching TutorialFest Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London, Julien Vanegue Bloomberg, USA |
16:00 - 18:00 | Formalized Mathematics ICPP at Studio 1 Chair(s): Adam Chlipala Massachusetts Institute of Technology | ||
16:00 22mTalk | Formalising the h-principle and sphere eversionremote presentation CPP | ||
16:22 22mTalk | A Formalized Reduction of Keller's Conjecture CPP Joshua Clune Carnegie Mellon University | ||
16:45 22mTalk | Computing Cohomology Rings in Cubical Agdadistinguished paper CPP Thomas Lamiaux University of Paris-Saclay, Ens Paris-Saclay, Axel Ljungström Stockholm University, Anders Mörtberg Department of Mathematics, Stockholm University | ||
17:07 8mBreak | short break CPP | ||
17:15 45mMeeting | CPP Business Meeting CPP Pre-print |
Tue 17 JanDisplayed time zone: Eastern Time (US & Canada) change
Tue 17 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | Differential Verification of Deep Neural Networks VMCAI Chao Wang University of Southern California | ||
10:00 30mTalk | ARENA: Enhancing Abstract Refinement for Neural Network Verification VMCAI Yuyi Zhong , Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore |
09:00 - 10:30 | Keynote + 1 talkPEPM at Scollay Chair(s): Jens Palsberg University of California, Los Angeles (UCLA) | ||
09:00 60mKeynote | Fast Cryptographic Code via Partial Evaluation PEPM Adam Chlipala Massachusetts Institute of Technology | ||
10:00 30mTalk | Towards Type Debugging using Partial Evaluation PEPM |
09:00 - 10:30 | |||
09:00 60mKeynote | (canceled invited talk) CPP | ||
10:08 22mTalk | Aesop: White-Box Best-First Proof Search for Leandistinguished paper CPP Link to publication DOI Pre-print |
09:00 - 10:30 | |||
09:00 15mTalk | Introduction PLMW @ POPL Amal Ahmed Northeastern University, USA Media Attached | ||
09:15 45mTalk | Imagining the Reader PLMW @ POPL Benjamin C. Pierce University of Pennsylvania Media Attached File Attached | ||
10:00 30mSocial Event | Icebreaker Activity PLMW @ POPL |
09:00 - 10:00 | |||
09:00 60mTalk | Modern Macros PADL Robert Bruce Findler Northwestern University |
10:00 - 10:30 | |||
10:00 30mTalk | Automatic Rollback Suggestions for Incremental Datalog Evaluation PADL David Zhao The University of Sydney, Pavle Subotic Microsoft Azure, Mukund Raghothaman University of Southern California, Bernhard Scholz University of Sydney |
11:00 - 12:30 | Neural networks and Abstract InterpretationVMCAI at Arlington Chair(s): Grigory Fedyukovich Florida State University | ||
11:00 15mTalk | Maximal Robust Neural Network Specifications via Oracle-guided Numerical OptimizationRecorded VMCAI | ||
11:15 15mTalk | SMT-Based Modeling and Verification of Spiking Neural Networks: A Case StudyRecorded VMCAI | ||
11:30 30mTalk | A generic framework to coarse-grain stochastic reaction networks by Abstract Interpretation VMCAI | ||
12:00 30mTalk | Sound Symbolic Execution via Abstract Interpretation and its Application to Security VMCAI Xavier Rival Inria; ENS; CNRS; PSL University, Ignacio Tiraboschi Inria, France / ENS, France, Tamara Rezk INRIA |
11:00 - 12:30 | |||
11:00 30mTalk | Semantic Transformation Framework for Rewriting Rules PEPM | ||
11:30 30mTalk | Symbolic Execution of Hadamard-Toffoli Quantum Circuits PEPM | ||
12:00 30mTalk | Generating Programs for Polynomial Multiplication with Correctness Assurance PEPM |
11:00 - 12:30 | |||
11:00 22mTalk | Terms for Efficient Proof Checking and ParsingRecorded Presentation CPP Michael Färber Universität Innsbruck, Austria | ||
11:22 22mTalk | Compositional pre-processing for automated reasoning in dependent type theoryremote presentation CPP Valentin Blot LMF, Inria, Université Paris-Saclay, Denis Cousineau Mitsubishi Electric R&D Centre Europe, Enzo Crance Mitsubishi Electric R&D Centre Europe, Louise Dubois de Prisque LMF, Inria, Université Paris-Saclay, Chantal Keller LRI, Université Paris-Sud, Assia Mahboubi INRIA, Pierre Vial Inria | ||
11:45 22mTalk | Practical and sound equality tests, automatically CPP | ||
12:07 22mTalk | Compiling higher-order specifications to SMT solvers: how to deal with rejection constructivelyremote presentation CPP Matthew L. Daggitt Heriott-Watt University, Robert Atkey University of Strathclyde, Wen Kokke University of Strathclyde, Ekaterina Komandantskaya Heriot-Watt University, UK, Luca Arnaboldi The University of Edinburgh |
11:00 - 12:30 | |||
11:00 45mTalk | Session Types Meet Polymorphism and Dependent Types PLMW @ POPL Peter Thiemann University of Freiburg, Germany Media Attached File Attached | ||
11:45 45mPanel | Career Trajectories in PL PLMW @ POPL Richard A. Eisenberg Jane Street, Anitha Gollamudi University of Massachusetts Lowell, Ryan Kavanagh McGill University, Joseph Tassarotti NYU, M: Michael Greenberg Stevens Institute of Technology |
11:00 - 12:30 | Functional (Logic) ProgrammingPADL at The Loft Chair(s): William E. Byrd University of Alabama at Birmingham, USA | ||
11:00 30mTalk | RICE: An Optimizing Curry Compiler PADL Steven Libby University of Portland | ||
11:30 30mTalk | Embedding Functional Logic Programming in Haskell via a Compiler Plugin PADL Kai-Oliver Prott University of Kiel, Germany, Finn Teegen University of Kiel, Germany, Jan Christiansen Flensburg University of Applied Sciences, Germany DOI File Attached | ||
12:00 30mTalk | Program Synthesis Using Example Propagation PADL Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Bastiaan Heeren Open University of the Netherlands, Netherlands |
12:30 - 14:00 | |||
14:00 - 15:30 | |||
14:00 60mKeynote | Verifying, Inferring and Exploiting Code Commutativity VMCAI Eric Koskinen Stevens Institute of Technology |
14:00 - 15:30 | |||
14:00 60mIndustry talk | MATLAB Coder: Partial Evaluation in Practice PEPM | ||
15:00 30mTalk | Modular Construction of Multi-sorted Free Extensions PEPM Guillaume Allais University of St Andrews, Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Nachiappan Valliappan Chalmers University of Technology, Sam Lindley University of Edinburgh, Jeremy Yallop University of Cambridge File Attached |
14:00 - 15:30 | |||
14:00 22mTalk | FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Storesremote presentation CPP Arvind Arasu Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Aymeric Fromherz Inria, Kesha Hietala University of Maryland, Bryan Parno Carnegie Mellon University, Ravi Ramamurthy Microsoft Research | ||
14:22 22mTalk | Formalising Decentralised Exchanges in Coq CPP Eske Hoy Nielsen Aarhus University, Danil Annenkov Concordium, Bas Spitters Concordium Blockchain Research Center, Aarhus University | ||
14:45 22mTalk | Semantics of Probabilistic Programs using S-Finite Kernels in Coq CPP Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Cyril Cohen Inria, Ayumu Saito Tokyo Institute of Technology | ||
15:07 22mTalk | Formalising Sharkovsky's Theorem (Proof Pearl) CPP Bhavik Mehta University of Cambridge |
14:00 - 15:30 | |||
14:00 45mTalk | Anti-disciplinary: doing academic research when you like too many thingsremote presentation PLMW @ POPL Chris Martens Northeastern University Media Attached File Attached | ||
14:45 45mTalk | How (not) to give a great research talk PLMW @ POPL Leonidas Lampropoulos University of Maryland, College Park Media Attached File Attached |
14:00 - 15:30 | |||
14:00 30mTalk | Execution Time Program Verification With Tight Bounds PADL Ana Carolina Silva FCUP, Manuel Barbosa HASLab - INESC TEC and FCUP, Mario Florido Universidade do Porto | ||
14:30 30mTalk | From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting PADL DOI File Attached | ||
15:00 30mTalk | Multiple Query Satisfiability of Constrained Horn Clauses PADL Emanuele De Angelis CNR-IASI, Fabio Fioravanti University of Chieti-Pescara, Alberto Pettorossi University of Rome Tor Vergata, Italy, Maurizio Proietti CNR-IASI |
16:00 - 17:30 | |||
16:00 15mTalk | A Pragmatic Approach to Stateful Partial Order ReductionRecorded VMCAI Berk Cirisci IRIF, University Paris Diderot and CNRS, France, Constantin Enea Ecole Polytechnique / LIX / CNRS, Azadeh Farzan University of Toronto, Suha Orhun Mutluergil Sabanci University, Turkey | ||
16:15 15mTalk | StaticPersist : Compiler Support for PMEM ProgrammingRecorded VMCAI Sorav Bansal IIT Delhi and CompilerAI Labs | ||
16:30 30mTalk | Compositional Verification of Stigmergic Collective Systems VMCAI | ||
17:00 30mTalk | Synthesizing History and Prophecy Variables for Symbolic Model Checking VMCAI |
16:00 - 17:30 | |||
16:00 30mTalk | Efficient Embedding of Strategic Attribute Grammars via MemoizationRemote PEPM José Nuno Macedo University of Minho, Emanuel Rodrigues HASLab & INESC TEC, University of Minho, Marcos Viera University of the Republic, Uruguay, João Saraiva | ||
16:30 30mTalk | Towards a Reflection for Effect HandlersRecorded PEPM | ||
17:00 30mDay closing | Wrap up PEPM Jens Palsberg University of California, Los Angeles (UCLA), Edwin Brady University of St Andrews, UK |
16:00 - 17:30 | |||
16:00 22mTalk | A formalization of Doob's martingale convergence theorems in mathlibremote presentation CPP Kexing Ying University of Cambridge, Rémy Degenne Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9198-CRIStAL, F-59000 Lille, France | ||
16:22 22mTalk | A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL CPP Angeliki Koutsoukou-Argyraki University of Cambridge, Department of Computer Science and Technology, Mantas Bakšys University of Cambridge, Chelsea Edmonds University of Cambridge | ||
16:45 22mTalk | A Formal Disproof of Hirsch Conjecture CPP Xavier Allamigeon Inria and Ecole Polytechnique, Quentin Canu Inria and Ecole Polytechnique, Pierre-Yves Strub Meta | ||
17:07 22mTalk | Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves CPP Anne Baanen Vrije Universiteit Amsterdam, Alex Best Vrije Universiteit Amsterdam, Nirvana Coppola Vrije Universiteit Amsterdam, Sander R. Dahmen Vrije Universiteit Amsterdam |
16:00 - 17:30 | |||
16:00 45mTalk | Big Ideas in Program Synthesis PLMW @ POPL Nadia Polikarpova University of California at San Diego Media Attached File Attached | ||
16:45 45mTalk | Care and Feeding of Advisors PLMW @ POPL Stephen Chong Harvard University Media Attached File Attached |
16:00 - 17:30 | |||
16:00 30mTalk | Dynamic slicing of Reaction Systems based on assertions and monitors PADL Linda Brodo Università di Sassari, Roberto Bruni University of Pisa, Moreno Falaschi Dipartimento di Ingegneria dell'Informazione e Scienze Matematiche, University of Siena | ||
16:30 30mTalk | Linear Algebraic Abduction with Partial Evaluation PADL DOI File Attached |
Wed 18 JanDisplayed time zone: Eastern Time (US & Canada) change
Wed 18 Jan
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | |||
08:30 - 08:50 | Wednesday Breakfast Session PreviewSession Previews at White Hill Chair(s): Nate Foster Cornell University | ||
08:30 10mTalk | Automated Verification: Session Preview Session Previews Michael Greenberg Stevens Institute of Technology | ||
08:40 10mTalk | Types I: Session Preview Session Previews Neel Krishnaswami University of Cambridge |
09:00 - 09:10 | WelcomePOPL at Grand Ballroom A Chair(s): Andrew Myers Cornell University, Amal Ahmed Northeastern University, USA | ||
09:10 - 10:15 | |||
09:10 65mKeynote | Principles of Persistent Programming POPL Viktor Vafeiadis MPI-SWS |
10:20 - 10:40 | Wednesday Morning Break Session PreviewSession Previews at White Hill Chair(s): Eric Campbell Cornell University | ||
10:20 10mTalk | Security: Session Preview Session Previews Limin Jia Carnegie Mellon University | ||
10:30 10mTalk | Synthesis I: Session Preview Session Previews Nadia Polikarpova University of California at San Diego |
10:45 - 12:00 | |||
10:45 25mTalk | Higher-Order Leak and Deadlock Free LocksDistinguished Paper POPL DOI | ||
11:10 25mTalk | Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations POPL DOI | ||
11:35 25mTalk | Recursive Subtyping for All POPL Litao Zhou University of Hong Kong, Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI |
10:45 - 12:00 | Automated VerificationPOPL at Grand Ballroom A Chair(s): Michael Greenberg Stevens Institute of Technology | ||
10:45 25mTalk | Kater: Automating Weak Memory Model Metatheory and Consistency Checking POPL DOI | ||
11:10 25mTalk | Stratified Commutativity in Verification Algorithms for Concurrent ProgramsVirtual POPL Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg DOI | ||
11:35 25mTalk | A Partial Order View of Message-Passing Communication Models POPL Cinzia Di Giusto Université Côte d'Azur; CNRS, Davide Ferre' Université Côte d'Azur; CNRS, Laetitia Laversa Université Côte d'Azur; CNRS, Etienne Lozes Université Côte d'Azur; CNRS DOI |
12:00 - 13:30 | |||
12:00 - 13:30 | |||
12:40 - 13:20 | Wednesday Lunch Session PreviewSession Previews at White Hill Chair(s): Chelsea Edmonds University of Cambridge | ||
12:40 10mTalk | Logic & Decidability I: Session Preview Session Previews Zachary Kincaid Princeton University | ||
12:50 10mTalk | Program Logics & Resources: Session Preview Session Previews Philippa Gardner Imperial College London | ||
13:00 10mTalk | Verified Compilation: Session Preview Session Previews Deian Stefan University of California at San Diego | ||
13:10 10mTalk | Probabilistic Inference: Session Preview Session Previews Alexandra Silva Cornell University |
13:30 - 14:45 | |||
13:30 25mTalk | A High-Level Separation Logic for Heap Space under Garbage Collection POPL Alexandre Moine Inria, Arthur Charguéraud Inria; Université de Strasbourg; CNRS; ICube, François Pottier Inria DOI | ||
13:55 25mTalk | CN: Verifying Systems C Code with Separation-Logic Refinement Types POPL Christopher Pulte University of Cambridge, Dhruv C. Makwana University of Cambridge, Thomas Sewell University of Cambridge, Kayvan Memarian University of Cambridge, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge DOI | ||
14:20 25mTalk | Conditional Contextual Refinement POPL Youngju Song Seoul National University; MPI-SWS, Minki Cho Seoul National University, Dongjae Lee Seoul National University, Chung-Kil Hur Seoul National University, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWS DOI |
13:30 - 14:45 | |||
13:30 25mTalk | Witnessability of Undecidable Problems POPL DOI | ||
13:55 25mTalk | On the Expressive Power of String Constraints POPL Joel D. Day Loughborough University, Vijay Ganesh Georgia Tech, Nathan Grewal University of Waterloo, Florin Manea University of Göttingen DOI | ||
14:20 25mTalk | A Robust Theory of Series Parallel Graphs POPL Rajeev Alur University of Pennsylvania, Caleb Stanford University of California, San Diego; University of California, Davis, Chris Watson University of Pennsylvania DOI |
15:10 - 16:25 | |||
15:10 25mTalk | MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code POPL Alexandra E. Michael University of California at San Diego; University of Washington, Anitha Gollamudi University of Massachusetts Lowell, Jay Bosamiya Carnegie Mellon University, Evan Johnson University of California at San Diego; Arm, Aidan Denlinger University of California at San Diego, Craig Disselkoen University of California at San Diego, Conrad Watt University of Cambridge, Bryan Parno Carnegie Mellon University, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Deian Stefan University of California at San Diego DOI | ||
15:35 25mTalk | Reconciling Shannon and Scott with a Lattice of Computable Information POPL Sebastian Hunt City University of London, Dave Sands Chalmers University of Technology, Sandro Stucki Amazon Prime Video Link to publication DOI Pre-print | ||
16:00 25mTalk | A Core Calculus for Equational Proofs of Cryptographic Protocols POPL Joshua Gancher Carnegie Mellon University, Kristina Sojakova Inria, Xiong Fan Rutgers University, Elaine Shi Carnegie Mellon University, Greg Morrisett Cornell University DOI |
15:10 - 16:25 | Synthesis IPOPL at Grand Ballroom A Chair(s): Nadia Polikarpova University of California at San Diego | ||
15:10 25mTalk | Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions POPL DOI | ||
15:35 25mTalk | FlashFill++: Scaling Programming by Example by Cutting to the Chase POPL José Pablo Cambronero Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Perelman Microsoft, Arjun Radhakrishna Microsoft, Clint Simon Microsoft, Ashish Tiwari Microsoft DOI | ||
16:00 25mTalk | Unrealizability Logic POPL Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison DOI |
16:45 - 18:00 | |||
16:45 25mTalk | DimSum: A Decentralized Approach to Multi-language Semantics and VerificationDistinguished Paper POPL Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Youngju Song Seoul National University; MPI-SWS, Emanuele D’Osualdo MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Deepak Garg MPI-SWS, Derek Dreyer MPI-SWS DOI | ||
17:10 25mTalk | Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler POPL Aurèle Barrière University of Rennes; Inria; CNRS; IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA, David Pichardie Meta DOI Pre-print | ||
17:35 25mTalk | Dargent: A Silver Bullet for Verified Data Layout Refinement POPL Zilin Chen UNSW, Ambroise Lafont University of Cambridge, Liam O'Connor University of Edinburgh, Gabriele Keller Utrecht University, Craig McLaughlin UNSW, Vincent Jackson University of Melbourne, Christine Rizkallah University of Melbourne DOI |
16:45 - 18:00 | |||
16:45 25mTalk | Affine Monads and Lazy Structures for Bayesian Programming POPL Swaraj Dash University of Oxford, Younesse Kaddar University of Oxford, Hugo Paquet University of Oxford, Sam Staton University of Oxford DOI | ||
17:10 25mTalk | Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic InferenceVirtual POPL Jianlin Li University of Waterloo, Leni Ven University of Waterloo, Pengyuan Shi University of Waterloo, Yizhou Zhang University of Waterloo DOI | ||
17:35 25mTalk | Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference POPL Wonyeol Lee Stanford University, Xavier Rival Inria; ENS; CNRS; PSL University, Hongseok Yang KAIST; IBS DOI |
18:10 - 18:30 | Wednesday Evening Session PreviewSession Previews at White Hill Chair(s): Xuejing Huang University of Hong Kong | ||
18:10 10mTalk | Synthesis II: Session Preview Session Previews Nate Foster Cornell University | ||
18:20 10mTalk | Semantics I: Session Preview Session Previews Ugo Dal Lago University of Bologna; Inria |
Thu 19 JanDisplayed time zone: Eastern Time (US & Canada) change
Thu 19 Jan
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | |||
08:20 - 08:50 | Thursday Breakfast Session PreviewSession Previews at White Hill Chair(s): Eric Campbell Cornell University | ||
08:20 10mTalk | Program Analysis & Parsing: Session Preview Session Previews David Pichardie Meta | ||
08:30 10mTalk | Resource Analysis: Session Preview Session Previews Xavier Rival Inria; ENS; CNRS; PSL University | ||
08:40 10mTalk | Automatic Differentiation: Session Preview Session Previews Sasa Misailovic University of Illinois at Urbana-Champaign |
09:00 - 10:00 | |||
09:00 60mPanel | Panel: Next 50 Years of POPL POPL M: Derek Dreyer MPI-SWS, P: Michael Carbin Massachusetts Institute of Technology, P: Nate Foster Cornell University, P: Xavier Leroy Collège de France, P: Benjamin C. Pierce University of Pennsylvania, P: Nadia Polikarpova University of California at San Diego, P: Azalea Raad Imperial College London, P: Sharon Shoham Tel Aviv University |
10:05 - 10:15 | Thursday Morning Break Session PreviewSession Previews at White Hill Chair(s): Nate Foster Cornell University | ||
10:05 10mTalk | Type Theory: Session Preview Session Previews Max S. New University of Michigan |
10:20 - 12:00 | |||
10:20 25mTalk | A Type-Based Approach to Divide-and-Conquer Recursion in Coq POPL Pedro da Costa Abreu Junior Purdue University, Benjamin Delaware Purdue University, Alex Hubers University of Iowa, Christa Jenkins University of Iowa, J. Garrett Morris University of Iowa, Aaron Stump University of Iowa DOI | ||
10:45 25mTalk | Elements of Quantitative RewritingVirtual POPL DOI | ||
11:10 25mTalk | The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding POPL Simon Castellan University of Rennes; Inria; CNRS; IRISA, Pierre Clairambault Université Aix-Marseille; Université de Toulon; CNRS; LIS DOI | ||
11:35 25mTalk | Deconstructing the Calculus of Relations with Tape Diagrams POPL Filippo Bonchi University of Pisa, Alessandro Di Giorgio University of Pisa, Alessio Santamaria University of Pisa; University of Sussex DOI |
10:20 - 12:00 | |||
10:20 25mTalk | babble: Learning Better Abstractions with E-Graphs and Anti-unification POPL David Cao University of California at San Diego, Rose Kunkel University of California at San Diego, Chandrakana Nandi Certora, Max Willsey University of Washington, Zachary Tatlock University of Washington, Nadia Polikarpova University of California at San Diego DOI Pre-print | ||
10:45 25mTalk | Combining Functional and Automata Synthesis to Discover Causal Reactive Programs POPL Ria Das Stanford University, Joshua B. Tenenbaum Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Zenna Tavares Basis; Columbia University DOI | ||
11:10 25mTalk | Comparative Synthesis: Learning Near-Optimal Network Designs by Query POPL Yanjun Wang Amazon Web Services, USA, Zixuan Li Purdue University, Chuan Jiang Purdue University, Xiaokang Qiu Purdue University, Sanjay Rao Purdue University DOI | ||
11:35 25mTalk | Top-Down Synthesis for Library Learning POPL Maddy Bowers Massachusetts Institute of Technology, Theo X. Olausson Massachusetts Institute of Technology, Lionel Wong Massachusetts Institute of Technology, Gabriel Grand Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Kevin Ellis Cornell University, Armando Solar-Lezama Massachusetts Institute of Technology DOI Pre-print |
12:00 - 13:30 | |||
13:00 - 13:20 | |||
13:00 10mTalk | Logic & Decidability II: Session Preview Session Previews Caleb Stanford University of California, San Diego; University of California, Davis | ||
13:10 10mTalk | Types II: Session Preview Session Previews Benjamin C. Pierce University of Pennsylvania |
13:30 - 14:45 | |||
13:30 25mTalk | Probabilistic Resource-Aware Session Types POPL DOI | ||
13:55 25mTalk | A Calculus for Amortized Expected Runtimes POPL Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU, Lena Verscht RWTH Aachen University DOI | ||
14:20 25mTalk | A General Noninterference Policy for Polynomial Time POPL Emmanuel Hainry Université de Lorraine; CNRS; Inria; LORIA, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA DOI |
13:30 - 14:45 | |||
13:30 25mTalk | SSA Translation Is an Abstract InterpretationDistinguished Paper POPL Matthieu Lemerre Université Paris-Saclay - CEA LIST DOI Pre-print | ||
13:55 25mTalk | Dynamic Race Detection with O(1) SamplesDistinguished Paper POPL Mosaad Al Thokair University of Illinois at Urbana-Champaign, Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur National University of Singapore, Mahesh Viswanathan University of Illinois at Urbana-Champaign Link to publication DOI Pre-print | ||
14:20 25mTalk | Statically Resolvable Ambiguity POPL Viktor Palmkvist KTH Royal Institute of Technology, Elias Castegren Uppsala University, Philipp Haller KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology DOI |
13:30 - 15:00 | |||
13:30 15mTalk | Scalable Synthesis of Regular Expressions From Only Positive Examples Student Research Competition | ||
13:45 15mTalk | Synthesizing Vectorized Code via Verified Lifting Student Research Competition Jeremy Ferguson University of California-Berkeley | ||
14:00 15mTalk | Evaluating Soundness of a Gradual Verifier with Property Based Testing Student Research Competition Jan-Paul Ramos-Davila Cornell University | ||
14:15 15mTalk | On the metatheory of IRs and the CPS-calculus Student Research Competition Paulo Torrens University of Kent | ||
14:30 15mTalk | Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness Student Research Competition Joshua Turcotti Cornell University | ||
14:45 15mTalk | Compiling and Running High-level Quantum Programs Student Research Competition Hristo Venev INSAIT |
15:10 - 16:25 | |||
15:10 25mTalk | Admissible Types-to-PERs Relativization in Higher-Order LogicDistinguished Paper POPL DOI | ||
15:35 25mTalk | An Order-Theoretic Analysis of Universe Polymorphism POPL Kuen-Bang Hou (Favonia) University of Minnesota, Carlo Angiuli Carnegie Mellon University, Reed Mullanix University of Minnesota DOI | ||
16:00 25mTalk | Impredicative Observational Equality POPL DOI |
15:10 - 16:25 | |||
15:10 25mTalk | You Only Linearize Once: Tangents Transpose to Gradients POPL Alexey Radul Google Research, Adam Paszke Google Research, Roy Frostig Google Research, Matthew J. Johnson Google Research, Dougal Maclaurin Google Research DOI | ||
15:35 25mTalk | Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations POPL DOI Pre-print | ||
16:00 25mTalk | ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic ProgramsDistinguished Paper POPL Alexander K. Lew Massachusetts Institute of Technology, Mathieu Huot University of Oxford, Sam Staton University of Oxford, Vikash K. Mansinghka Massachusetts Institute of Technology DOI Pre-print |
16:45 - 18:00 | |||
18:10 - 18:30 | Thursday Evening Session PreviewSession Previews at White Hill Chair(s): Alexandra E. Michael University of California at San Diego; University of Washington | ||
18:10 10mTalk | Semantics & Effects: Session Preview Session Previews Andrew K. Hirsch University at Buffalo, SUNY | ||
18:20 10mTalk | Logic Programming: Session Preview Session Previews Cody Roux AWS |
19:30 - 21:30 | |||
20:00 - 23:00 | |||
Fri 20 JanDisplayed time zone: Eastern Time (US & Canada) change
Fri 20 Jan
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | |||
08:30 - 08:50 | |||
08:30 10mTalk | Formal Methods in Compilation & Implementation: Session Preview Session Previews Arjun Guha Northeastern University and Roblox Research | ||
08:40 10mTalk | Quantum Computing: Session Preview Session Previews Jens Palsberg University of California, Los Angeles (UCLA) |
09:00 - 10:15 | |||
09:00 25mTalk | A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ POPL Nick Rioux University of Pennsylvania, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Steve Zdancewic University of Pennsylvania DOI | ||
09:25 25mTalk | Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations POPL Han Xu Peking University, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
09:50 25mTalk | Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework POPL Victor Arrial Université Paris Cité - CNRS - IRIF, Giulio Guerrieri Aix Marseille Université - CNRS - LIS; Edinburgh Research Centre - Central Software Institute - Huawei, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France DOI |
09:00 - 10:15 | |||
09:00 25mTalk | When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic POPL Zachary Kincaid Princeton University, Nicolas Koh Princeton University, Shaowei Zhu Princeton University DOI | ||
09:25 25mTalk | Higher-Order MSL Horn Constraints POPL Jerome Jochems University of Bristol, Eddie Jones University of Bristol, Steven Ramsay University of Bristol DOI | ||
09:50 25mTalk | Fast Coalgebraic Bisimilarity Minimization POPL DOI Pre-print |
10:20 - 10:40 | Friday Morning Break Session PreviewSession Previews at White Hill Chair(s): Neea Rusch Augusta University | ||
10:20 10mTalk | Concurrency & Linearizability: Session Preview Session Previews Chung-Kil Hur Seoul National University | ||
10:30 10mTalk | Algorithmic Verification Session Previews Umang Mathur National University of Singapore |
10:45 - 12:00 | |||
10:45 25mTalk | Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice POPL DOI | ||
11:10 25mTalk | Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq POPL Nicolas Chappe University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Paul He University of Pennsylvania, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Steve Zdancewic University of Pennsylvania DOI | ||
11:35 25mTalk | Hefty Algebras: Modular Elaboration of Higher-Order Algebraic EffectsRecorded POPL DOI Pre-print |
10:45 - 12:00 | |||
10:45 25mTalk | Qunity: A Unified Language for Quantum and Classical Computing POPL Finn Voichick University of Maryland, Liyi Li University of Maryland, Robert Rand University of Chicago, Michael Hicks University of Maryland; Amazon DOI Pre-print | ||
11:10 25mTalk | Proto-Quipper with Dynamic LiftingVirtual POPL Peng Fu Dalhousie University, Kohei Kishida University of Illinois at Urbana-Champaign, Neil Julien Ross Dalhousie University, Peter Selinger Dalhousie University DOI | ||
11:35 25mTalk | CoqQ: Foundational Verification of Quantum ProgramsVirtual POPL Li Zhou MPI-SP; Institute of Software at Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Pierre-Yves Strub Meta, Junyi Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University DOI |
12:00 - 13:30 | |||
12:00 - 13:30 | |||
13:00 - 13:20 | |||
13:00 10mTalk | Relational & Automated Verification: Session Preview Session Previews Eric Campbell Cornell University | ||
13:10 10mTalk | Semantics II: Session Preview Session Previews Robert Atkey University of Strathclyde |
13:30 - 14:45 | Formal Methods in Compilation & ImplementationPOPL at Avenue34 Chair(s): Lindsey Kuper University of California at Santa Cruz | ||
13:30 25mTalk | Tail Recursion Modulo Context: An Equational Approach POPL DOI | ||
13:55 25mTalk | Taking Back Control in an Intermediate Representation for GPU Computing POPL Vasileios Klimis Imperial College London, Jack Clark Imperial College London, Alan Baker Google, David Neto Google, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London; Google DOI | ||
14:20 25mTalk | Executing Microservice Applications on Serverless, Correctly POPL Konstantinos Kallas University of Pennsylvania, Haoran Zhang University of Pennsylvania, Rajeev Alur University of Pennsylvania, Sebastian Angel University of Pennsylvania; Microsoft Research, Vincent Liu University of Pennsylvania DOI |
13:30 - 14:45 | |||
13:30 25mTalk | Modular Primal-Dual Fixpoint Logic Solving for Temporal VerificationDistinguished Paper POPL Hiroshi Unno University of Tsukuba; RIKEN AIP, Tachio Terauchi Waseda University, Yu Gu University of Tsukuba, Eric Koskinen Stevens Institute of Technology DOI | ||
13:55 25mTalk | Optimal CHC Solving via Termination Proofs POPL Yu Gu University of Tsukuba, Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP DOI | ||
14:20 25mTalk | From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems POPL Aaron Bembenek Harvard University, Michael Greenberg Stevens Institute of Technology, Stephen Chong Harvard University DOI Pre-print |
15:10 - 16:25 | |||
15:10 25mTalk | An Operational Approach to Library Abstraction under Relaxed Memory Concurrency POPL DOI | ||
15:35 25mTalk | The Path to Durable Linearizability POPL DOI | ||
16:00 25mTalk | A Compositional Theory of Linearizability POPL DOI |
15:10 - 16:25 | |||
15:10 25mTalk | The Fine-Grained Complexity of CFL Reachability POPL DOI | ||
15:35 25mTalk | Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming POPL Yuanbo Li Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology, Thomas Reps University of Wisconsin-Madison DOI | ||
16:00 25mTalk | Context-Bounded Verification of Context-Free Specifications POPL Pascal Baumann MPI-SWS, Moses Ganardi MPI-SWS, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam MPI-SWS, Georg Zetzsche MPI-SWS DOI |
16:45 - 18:00 | |||
16:45 25mTalk | Locally Nameless Sets POPL Andrew M. Pitts University of Cambridge DOI Pre-print | ||
17:10 25mTalk | Why Are Proofs Relevant in Proof-Relevant Models? POPL Axel Kerinec Université Sorbonne Paris Nord; LIPN; CNRS, Giulio Manzonetto Université Sorbonne Paris Nord; LIPN; CNRS, Federico Olimpieri University of Leeds DOI | ||
17:35 25mTalk | Towards a Higher-Order Mathematical Operational Semantics POPL Sergey Goncharov University of Erlangen-Nuremberg, Stefan Milius University of Erlangen-Nuremberg, Lutz Schröder University of Erlangen-Nuremberg, Stelios Tsampas University of Erlangen-Nuremberg, Henning Urbat University of Erlangen-Nuremberg DOI Pre-print |
16:45 - 18:00 | |||
16:45 25mTalk | An Algebra of Alignment for Relational Verification POPL Timos Antonopoulos Yale University, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Ramana Nagasamudram Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Minh Ngo Stevens Institute of Technology DOI | ||
17:10 25mTalk | Grisette: Symbolic Compilation as a Functional Programming Library POPL DOI | ||
17:35 25mTalk | HFL(Z) Validity Checking for Automated Program Verification POPL Naoki Kobayashi University of Tokyo, Kento Tanahashi University of Tokyo, Ryosuke Sato University of Tokyo, Takeshi Tsukada Chiba University DOI |
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
Sat 21 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 5mDay opening | Introduction PriSC | ||
09:05 60mKeynote | Semantic Intermediate Representations for Sound Language Interoperability PriSC Amal Ahmed Northeastern University, USA Pre-print | ||
10:05 25mTalk | Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers PriSC Farzaneh Derakhshan Carnegie Mellon University, Zichao Zhang Carnegie Mellon University, Amit Vasudevan Carnegie Mellon University, Limin Jia Carnegie Mellon University File Attached |
09:00 - 10:30 | |||
09:00 60mTalk | Omnisemantics: Smooth Handling of Nondeterminism (Invited talk) CoqPL Samuel Gruetter Massachusetts Institute of Technology | ||
10:00 30mTalk | Interactive Theorem Proving in Logic Education:A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching CoqPL File Attached |
11:00 - 12:30 | |||
11:00 25mTalk | Automated Learning and Verification of Embedded Security Architectures PriSC Matteo Busi University Ca' Foscari, Venice, Riccardo Focardi University Ca' Foscari, Venice, Flaminia L. Luccio University Ca' Foscari, Venice File Attached | ||
11:25 25mTalk | pi_RA: A pi-calculus for verifying protocols that use remote attestation PriSC File Attached | ||
11:50 25mTalk | Robust Constant-Time Cryptography PriSC Matthew Kolosick University of California at San Diego, Basavesh Ammanaghatta Shivakumar Max Planck Institute for Security and Privacy (MPI-SP), Sunjay Cauligi University of California at San Diego, USA, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego Pre-print | ||
12:15 15mTalk | Short Talk: Generalising secure compilation criteria PriSC Emiel Lanckriet KU Leuven |
11:00 - 12:30 | |||
11:00 30mTalk | Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation CoqPL File Attached | ||
11:30 30mTalk | Integrating graphical proofs in Coq CoqPL File Attached | ||
12:00 30mTalk | Towards Formally Verified Path ORAM in Coq CoqPL Hannah Leung University of Illinois Urbana-Champaign, Talia Ringer University of Illinois at Urbana-Champaign, Christopher W. Fletcher University of Illinois Urbana-Champaign File Attached |
14:00 - 15:30 | |||
14:00 25mTalk | Blame-Preserving Secure Compilation PriSC Marco Patrignani University of Trento, Matthis Kruse CISPA Helmholtz Center for Information Security Pre-print | ||
14:25 25mTalk | Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed InterfacesRecorded PriSC Pre-print File Attached | ||
14:50 25mTalk | SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine PriSC Jérémy Thibault MPI-SP, Arthur Azevedo de Amorim Boston University, Roberto Blanco MPI-SP, Aina Linn Georges Aarhus University, Cătălin Hriţcu MPI-SP, Andrew Tolmach Portland State University Pre-print Media Attached File Attached |
14:00 - 15:30 | |||
14:00 30mTalk | Verified Differential Privacy for Finite Computers CoqPL Vivien Rindisbacher Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University File Attached | ||
14:30 30mTalk | Formalizing Monoidal Categories and Actions for Syntax with Binders CoqPL Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT (CNRS and Univ. of Toulouse), Kobe Wullaert Technical University Delft File Attached | ||
15:00 30mTalk | Certifying Complexity Analysis CoqPL Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS File Attached |
16:00 - 17:30 | |||
16:00 25mTalk | Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers PriSC Michael Smith UC San Diego, Abhishek Sharma UC San Diego, John Renner University of California at San Diego, USA, David Thien UC San Diego, Sorin Lerner University of California at San Diego, Fraser Brown CMU, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego File Attached | ||
16:25 25mTalk | FaJITa: Verifying Optimizations on Just-In-Time Programs PriSC David Thien UC San Diego, Michael Smith UC San Diego, Evan Johnson University of California at San Diego; Arm, Sorin Lerner University of California at San Diego, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego, Fraser Brown CMU Pre-print File Attached | ||
16:50 25mTalk | Universally Composable Security for Program Partitioning PriSC Coşku Acay Cornell University, Joshua Gancher Carnegie Mellon University, Rolph Recto Cornell University, Andrew Myers Cornell University File Attached |
16:00 - 17:30 | |||
16:00 45mTalk | Session with the Coq Development Team CoqPL |