Filter Program
Conference Dates
Conference Dates are in time zone (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna, and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
Sun 17 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
07:00 - 08:00 | |||
07:00 60mSocial Event | POPL Card Game POPL Meetups | ||
15:30 - 16:00 | |||
15:30 30mSocial Event | Sunday Breakfast Tables Workshops and Co-located Events | ||
16:00 - 17:00 | |||
16:00 60mTalk | Invited Talk: Teaching Algorithms and Data Structures with a Proof Assistant CPP Tobias NipkowTechnische Universität München Media Attached File Attached | ||
16:00 - 16:50 | |||
16:00 - 17:30 | Secure compilers & cryptographyPriSC at PriSC Chair(s): Fraser BrownStanford University, USA, Aastha MehtaMPI-SWS, Germany and University of British Columbia, Canada | ||
16:00 18mTalk | High-level high-speed high-assurance crypto PriSC Jonathan CoganStanford, Fraser BrownStanford University, USA, Alex OzdemirStanford, Riad S. WahbyStanford University, USA Media Attached | ||
16:18 18mTalk | Cross-Architecture Testing for Compiler-Introduced Security Bugs PriSC Media Attached File Attached | ||
16:36 18mTalk | High-Assurance Cryptography in the Spectre Era PriSC Gilles BartheMPI-SP, Germany / IMDEA Software Institute, Spain, Sunjay CauligiUniversity of California at San Diego, USA, Benjamin GregoireINRIA, Adrien KoutsosINRIA Paris, Kevin LiaoMax Planck Institute for Security and Privacy, Tiago OliveiraUniversity of Porto (FCUP) and INESC TEC, Swarn PriyaPurdue University, Tamara RezkInria, France, Peter SchwabeMax Planck Institute for Security and Privacy Media Attached | ||
16:54 18mTalk | Compilation as Multi-Language Semantics PriSC William J. BowmanUniversity of British Columbia Pre-print Media Attached | ||
17:12 18mTalk | Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs PriSC Coşku AcayCornell University, Rolph Recto, Joshua GancherCornell University, Andrew C. MyersCornell University, Elaine ShiCornell University Media Attached | ||
16:00 - 17:00 | |||
16:00 60mKeynote | Model Checking Hyperproperties VMCAI Media Attached | ||
16:50 - 17:30 | |||
16:50 13mTalk | Binary Tree Hamiltonian Monte Carlo LAFI Carol MakUniversity of Oxford, Fabian ZaiserUniversity of Oxford, C.-H. Luke OngUniversity of Oxford File Attached | ||
17:03 13mTalk | An algebraic theory of conditioning LAFI File Attached | ||
17:16 13mTalk | The Selection Monad and Decision-Making Languages LAFI File Attached | ||
17:00 - 17:30 | Proof TacticsCPP at CPP Chair(s): Jesper CockxTU Delft Streamed session: https://youtu.be/PAxUO84tUE8?t=3781 | ||
17:00 15mTalk | A Novice-Friendly Induction Tactic for Lean CPP Jannis LimpergVrije Universiteit Amsterdam Pre-print Media Attached | ||
17:15 15mTalk | Lassie: HOL4 Tactics by Example CPP Heiko BeckerMPI-SWS, Nathaniel BosMcGill University, Ivan GavranMPI-SWS, Eva DarulovaMPI-SWS, Rupak MajumdarMPI-SWS Pre-print Media Attached File Attached | ||
17:00 - 17:30 | |||
17:00 15mTalk | Compositional Model Checking for Multi-Properties VMCAI Ohad GoudsmidDepartment of Computer Science, The Technion, Orna GrumbergTechnion – Israel Institute of Technology, Sarai SheinvaldDepartment of Software Engineering, ORT Braude College of Engineering Media Attached | ||
17:15 15mTalk | Decomposing Data Structure Commutativity Proofs with mn-Differencing VMCAI Media Attached | ||
17:30 - 18:00 | |||
17:30 30mBreak | Sunday Coffee Break Workshops and Co-located Events | ||
18:00 - 18:45 | Logic, Set Theory, and Category TheoryCPP at CPP Chair(s): Yannick ForsterSaarland University Streamed session: https://youtu.be/U_ZT9hfDAUQ | ||
18:00 15mTalk | An Anti-Locally-Nameless Approach to Formalizing Quantifiers CPP Olivier LaurentCNRS & ENS Lyon Pre-print Media Attached | ||
18:15 15mTalk | The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq CPP Pre-print Media Attached | ||
18:30 15mTalk | Formalizing Category Theory in Agda CPP Pre-print Media Attached | ||
18:00 - 19:00 | |||
18:00 60mKeynote | Frontiers in Secure Compilation – an Industrial Perspective (invited talk) PriSC Hugo VincentArm Research | ||
18:00 - 19:30 | |||
18:00 90mPoster | SRC Poster Session Student Research Competition | ||
18:00 - 18:30 | Infinite-State Systems and CompilationVMCAI at VMCAI Chair(s): Orna GrumbergTechnion – Israel Institute of Technology | ||
18:00 15mTalk | Proving the existence of fair paths in infinite state systems VMCAI Enrico MagnagoFondazione Bruno Kessler, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno Kessler Media Attached | ||
18:15 15mTalk | A Self-Certifying Compilation Framework for WebAssembly VMCAI Media Attached | ||
18:45 - 19:30 | Formalized MathematicsCPP at CPP Chair(s): Amin TimanyAarhus University Streamed session: https://youtu.be/U_ZT9hfDAUQ?t=2768 | ||
18:45 15mTalk | Formalizing the Ring of Witt VectorsDistinguished Paper Award CPP Pre-print Media Attached | ||
19:00 15mTalk | Formal Verification of Semi-algebraic Sets and Real Analytic Functions CPP J Tanner SlagelNASA Langley Research Center, Lauren WhiteKansas State University, Aaron DutleNASA Langley Research Center Pre-print Media Attached | ||
19:15 15mTalk | On the Formalisation of Kolmogorov Complexity CPP Pre-print Media Attached | ||
19:30 - 20:00 | |||
19:30 30mSocial Event | Sunday Hallway Time Workshops and Co-located Events | ||
21:00 - 21:30 | |||
21:00 15mTalk | A Categorical Approach to Secure Compilation (and others things) (short talk) PriSC Stylianos Tsampas, Andreas NuytsKU Leuven, Belgium, Dominique DevrieseVrije Universiteit Brussel, Frank PiessensKU Leuven | ||
21:15 15mTalk | Contract-aware Secure Compilation (short talk) PriSC Pre-print | ||
Mon 18 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
04:30 - 05:30 | |||
04:30 60mSocial Event | Panel Discussion 1: Choosing Research Topics POPL Meetups Chung-Kil HurSeoul National University, South Korea, Christine RizkallahUNSW Sydney, Hongseok YangKAIST, Ilya SergeyYale-NUS College and National University of Singapore, James NobleVictoria University of Wellington | ||
07:00 - 08:00 | |||
07:00 60mBreak | Monday Coffee Break 1 POPL Meetups | ||
10:00 - 11:00 | Session 1PEPM at PEPM Chair(s): Torben MogensenDIKU, University of Copenhagen Live stream: https://www.youtube.com/watch?v=fvWxWyV05v4 | ||
10:00 30mShort-paper | A Functional Abstraction of Typed Trails PEPM Kenichi AsaiOchanomizu University, Youyou CongTokyo Institute of Technology, Chiaki IshioOchanomizu University Media Attached File Attached | ||
10:30 30mResearch paper | A Text-based Syntax Completion Method Using LR Parsing PEPM Media Attached | ||
11:30 - 12:30 | Session 2PEPM at PEPM Chair(s): Youyou CongTokyo Institute of Technology Live stream: https://www.youtube.com/watch?v=tuxm51MLkHM | ||
11:30 30mResearch paper | Coq to C Translation with Partial Evaluation PEPM Akira TanakaNational Institute of Advanced Industrial Science and Technology (AIST) Media Attached | ||
12:00 30mResearch paper | Counterexample Generation for Program Verification based on Ownership Refinement TypesBest Paper Award PEPM Hideto UenoThe Univeristy of Tokyo, John TomanCertora, inc., Naoki KobayashiUniversity of Tokyo, Japan, Takeshi TsukadaChiba University, Japan Media Attached | ||
13:30 - 14:30 | Session 3PEPM at PEPM Chair(s): Robert AtkeyUniversity of Strathclyde Live stream: https://www.youtube.com/watch?v=G5vngBBn398 | ||
13:30 30mShort-paper | Control Flow Obfuscation for Featherweight Java using Continuation Passing PEPM Kenny Zhuo Ming LuISTD, Singapore University of Technology and Design Media Attached File Attached | ||
14:00 30mResearch paper | Efficient Fair Conjunction for Structurally-Recursive Relations PEPM Petr LozovSain Petersburg State University, SPbGU, Dmitri BoulytchevSaint Petersburg State University / JetBrains Research Media Attached File Attached | ||
14:30 - 15:30 | |||
14:30 60mKeynote | Semantics-based Synthesis in miniKanren PADL William E. ByrdUniversity of Alabama at Birmingham, USA | ||
14:30 - 15:15 | |||
14:30 45mTalk | Think Abstractly, Work Concretely PLMW Ichiro HasuoNational Institute of Informatics, Japan Media Attached | ||
15:00 - 16:00 | Keynote 1PEPM at PEPM Chair(s): Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK Live stream: https://www.youtube.com/watch?v=kaJOj_LErQo The PEPM 2021 Best Paper Award will be announced at the beginning of this session immediately before this keynote. | ||
15:00 60mKeynote | Program Manipulation of C Code: From Partial Evaluation to Semantic Patches for the Linux Kernel PEPM Julia LawallInria File Attached | ||
15:30 - 16:00 | |||
15:30 30mSocial Event | Topic Oriented Discussions Workshops and Co-located Events | ||
16:00 - 17:00 | Invited TalkCPP at CPP Chair(s): Andrei PopescuUniversity of Sheffield Streamed session: https://youtu.be/poHYVOMQuro?t=144 | ||
16:00 60mTalk | Invited Talk: Underpinning the foundations: Sail-based semantics, testing, and reasoning, for production and CHERI-enabled architectures CPP Peter SewellUniversity of Cambridge Media Attached | ||
16:00 - 17:30 | Applications of Declarative LanguagesPADL at PADL Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK | ||
16:00 30mResearch paper | A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States PADL Fabio TardivoNew Mexico State University, Loc PhamNew Mexico State University, Tran Cao SonNew Mexico State University, Enrico PontelliNew Mexico State University | ||
16:30 30mResearch paper | Data validation meets Answer Set Programming PADL Mario AlvianoUniversity of Calabria, Carmine DodaroDepartment of Mathematics and Computer Science, University of Calabria, Arnel ZamaylaUniversity of Calabria, Italy | ||
17:00 30mResearch paper | Lightweight Declarative Server-Side Web Programming PADL Michael HanusKiel University | ||
16:00 - 17:30 | |||
16:00 45mTalk | Numbers, Logic, and Decidability Results for Cyber-Physical Systems PLMW Rupak MajumdarMPI-SWS | ||
16:45 45mTalk | The Lean Researcher PLMW Alastair F. DonaldsonImperial College London and Google | ||
16:00 - 17:30 | |||
16:00 90mTutorial | [T1] The Current State of Automatic Differentiation TutorialFest Barak A. PearlmutterMaynooth University | ||
16:00 - 17:30 | |||
16:00 90mTutorial | [T2] Liquid Haskell: Refinement Type Checker for Haskell TutorialFest | ||
16:00 - 17:30 | |||
16:00 90mTutorial | [T3] Dynamic Data-Race Prediction : Fundamentals, Theory and Practice TutorialFest Pre-print Media Attached File Attached | ||
16:00 - 17:00 | |||
16:00 60mKeynote | Algebra-based Synthesis of Loops and their Invariants VMCAI I: Laura KovacsVienna University of Technology (TU Wien), Andreas HumenbergerVienna University of Technology Media Attached | ||
17:00 - 17:30 | Program LogicsCPP at CPP Chair(s): William ManskyUniversity of Illinois at Chicago Streamed session: https://youtu.be/poHYVOMQuro?t=3869 | ||
17:00 15mTalk | Contextual Refinement of the Michael-Scott Queue (Proof Pearl) CPP Pre-print Media Attached | ||
17:15 15mTalk | Reasoning About Monotonicity in Separation Logic CPP Pre-print Media Attached | ||
17:00 - 17:30 | |||
17:00 15mTalk | Runtime Abstract Interpretation for Numerical Accuracy and Robustness VMCAI Franck VédrineCEA LIST, Maxime JacqueminCEA LIST, France, Nikolai KosmatovThales Research and Technology, Julien SignolesCEA LIST Media Attached | ||
17:15 15mTalk | Twinning automata and regular expressions for string static analysis VMCAI Luca NegriniCa’ Foscari University of Venice, Julia S.r.l., Vincenzo ArceriCa’ Foscari University of Venice, Pietro FerraraUniversità Ca' Foscari, Venezia, Italy, Agostino CortesiUniversità Ca' Foscari Venezia Media Attached | ||
17:30 - 18:00 | |||
17:30 30mBreak | Monday Coffee Break 2 Workshops and Co-located Events | ||
18:00 - 18:45 | |||
18:00 15mTalk | A Coq Formalization of Data Provenance CPP Véronique BenzakenUniversité Paris Saclay, Sarah Cohen-BoulakiaLRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay, Evelyne ContejeanCNRS, Chantal KellerLRI, Univ. Paris-Sud, Rébecca ZucchiniLRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay Pre-print Media Attached | ||
18:15 15mTalk | Developing and certifying Datalog optimizations in Coq/MathComp CPP Pre-print Media Attached | ||
18:30 15mTalk | Machine-Checked Semantic Session TypingDistinguished Paper Award CPP Jonas Kastberg HinrichsenIT University of Copenhagen, Daniël LouwrinkUniversity of Amsterdam, Robbert KrebbersRadboud University Nijmegen, Jesper BengtsonIT University of Copenhagen Pre-print Media Attached | ||
18:00 - 19:30 | |||
18:00 30mResearch paper | A Family of Unification-oblivious Program Transformations and Their Applications PADL Paul TarauUniversity of North Texas | ||
18:30 30mResearch paper | On Adding Pattern Matching to Haskell-based Deeply Embedded Domain Specific Languages PADL David YoungUniversity of Kansas, USA, Mark GrebeUniversity of Central Missouri, USA, Andy GillUniversity of Kansas, USA | ||
18:00 - 19:30 | |||
18:00 45mTalk | Reasoning About Programs in Higher-Order Concurrent Separation Logic PLMW Amin TimanyAarhus University | ||
18:45 45mTalk | εσόμεθα πολλώ κάρρονες – making your way in a changing world PLMW Sophia DrossopoulouImperial College London | ||
18:00 - 19:30 | |||
18:00 90mTutorial | [T5] An Invitation to the Intersection of Quantum Computing and Programming Languages TutorialFest Xiaodi WuUniversity of Maryland, USA Pre-print | ||
18:00 - 19:30 | |||
18:00 90mTutorial | [T4] Iris – A Modular Foundation for Higher-Order Concurrent Separation Logic TutorialFest Tej ChajedMassachusetts Institute of Technology, USA, Ralf JungMPI-SWS, Joseph TassarottiBoston College Link to publication | ||
18:00 - 18:30 | |||
18:00 15mTalk | Unbounded Procedure Summaries from Bounded Environments VMCAI Lauren PickPrinceton University, Grigory FedyukovichFlorida State University, Aarti GuptaPrinceton University Media Attached | ||
18:15 15mTalk | Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking VMCAI Media Attached | ||
18:30 - 19:15 | |||
18:30 15mTalk | Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible VMCAI Marius KampFriedrich-Alexander University Erlangen-Nürnberg, Michael PhilippsenFriedrich-Alexander University Erlangen-Nürnberg (FAU) Media Attached | ||
18:45 15mTalk | Automated Repair of Heap-Manipulating Programs using Deductive Synthesis VMCAI Thanh-Toan NguyenNational University of Singapore, Quang-Trung TaNational University of Singapore, Ilya SergeyYale-NUS College and National University of Singapore, Wei-Ngan ChinNational University of Singapore Media Attached | ||
19:00 15mTalk | GPURepair: Automated Repair of GPU Kernels VMCAI Media Attached | ||
18:45 - 19:30 | Security, Blockchains, and Smart ContractsCPP at CPP Chair(s): Andreas LochbihlerDigital Asset Streamed session: https://youtu.be/Qak5mK92etU?t=2832 | ||
18:45 15mTalk | Extracting Smart Contracts Tested and Verified in Coq CPP Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Mikkel MiloConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University Pre-print Media Attached File Attached | ||
19:00 15mTalk | Formal Verification of Authenticated, Append-Only Skip Lists in Agda CPP Victor Cacciari MiraldoDFINITY Foundation, Harold CarrOracle Labs, USA, Mark MoirOracle Labs, New Zealand, Lisandra SilvaUniversity of Minho, Guy L. Steele Jr.Oracle Labs Pre-print Media Attached | ||
19:15 15mTalk | Towards formally verified compilation of tag-based policy enforcement CPP CHR ChhakPortland State University, Andrew TolmachPortland State University, Sean AndersonPortland State University Pre-print Media Attached | ||
19:30 - 20:00 | |||
19:30 30mSocial Event | Monday Shuffle-Space Time Workshops and Co-located Events | ||
20:00 - 21:00 | |||
20:00 60mSocial Event | POPL Card Game Workshops and Co-located Events | ||
20:00 - 21:00 | Lightning TalksCPP / CPP Lightning Talks at CPP Chair(s): Natarajan ShankarSRI International, USA Streamed sessions: https://youtu.be/sFMJBTtbjTc | ||
20:00 5mTalk | Certified Semantics for miniKanren CPP Lightning Talks Dmitry RozplokhasSaint Petersburg State University and JetBrains Research, Andrey VyatkinSaint Petersburg State University, Petr LozovSain Petersburg State University, SPbGU, Dmitri BoulytchevSaint Petersburg State University / JetBrains Research Media Attached | ||
20:05 5mTalk | Cameleer: a Deductive Verification Tool for OCaml CPP Lightning Talks Mário PereiraNOVA LINCS & Nova School of Sciences and Tecnhology, Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS | ||
20:10 5mTalk | Gradualizing the Calculus of Inductive Constructions CPP Lightning Talks Meven Lennon-BertrandInria – LS2N, Université de Nantes, Kenji MaillardInria Nantes & University of Chile, Nicolas TabareauInria, Éric TanterUniversity of Chile Pre-print | ||
20:15 5mTalk | Formally Verified Decentralized Exchange with Mi-Cho-Coq CPP Lightning Talks Arvid JakobssonNomadic Labs, Colin GonzálezUniversité de Paris, Irif -- Nomadic Labs, Bruno BernardoNomadic Labs, Raphaël CauderlierNomadic Labs | ||
20:20 5mTalk | A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers CPP Lightning Talks Sören BleikertzDigital Asset, Andreas LochbihlerDigital Asset, Ognjen MarićDigital Asset, Simon MeierDigital Asset, Phoebe NicholsDigital Asset, Matthias SchmalzDigital Asset, Ratko G. VeprekDigital Asset File Attached | ||
20:25 5mTalk | Specification and model checking of Tendermint consensus in TLA+ CPP Lightning Talks | ||
20:30 5mTalk | Formalization of Combinatorics on Words in Isabelle/HOL CPP Lightning Talks Štěpán HolubCharles University, Štěpán StarostaFaculty of Information Technology, Czech Technical University in Prague Link to publication Media Attached File Attached | ||
20:35 5mTalk | Formalising MPC-in-the-head-based zero-knowledge CPP Lightning Talks Nikolaj SidorencoAarhus University, Sabine OechsnerAarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University File Attached | ||
20:40 5mTalk | Mechanically-checked soundness of type-based null safety CPP Lightning Talks Alexander KogtenkovSchaffhausen Institute of Technology, Switzerland Media Attached File Attached | ||
20:45 5mTalk | Formalising MiniSail in Isabelle CPP Lightning Talks Mark WassellUniversity of Cambridge | ||
20:50 5mTalk | How to verify an ASN.1 Protocol C-language Stack in Coq? CPP Lightning Talks File Attached | ||
20:55 5mTalk | Monadic Second-Order Logic and Pomset Languages CPP Lightning Talks Tobias KappéCornell University | ||
20:00 - 21:00 | |||
20:00 60mLive Q&A | Panel: Doing Research in PL PLMW Greg MorrisettCornell Tech, Susan EisenbachImperial College London, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, Jeehoon KangKAIST, Delphine DemangeUniv Rennes, Inria, CNRS, IRISA, Kuen-Bang Hou (Favonia)University of Minnesota, Twin Cities | ||
Tue 19 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
04:30 - 05:30 | |||
04:30 60mSocial Event | Panel Discussion 2: Improving Peer Review POPL Meetups Hongseok YangKAIST, Ilya SergeyYale-NUS College and National University of Singapore, James NobleVictoria University of Wellington, Soham ChakrabortyIIT Delhi, India, Youyou CongTokyo Institute of Technology | ||
07:00 - 08:00 | |||
07:00 60mBreak | Tuesday Coffee Break 1 POPL Meetups | ||
14:30 - 15:30 | |||
14:30 60mKeynote | Verifying a compiler through equational means CoqPL Yannick ZakowskiInria | ||
14:30 - 15:30 | |||
14:30 60mKeynote | SMT-based Constraint Answer Set Solver EZSMT PADL Yuliya LierlerUniversity of Nebraska | ||
14:30 - 15:30 | |||
14:30 60mLive Q&A | Panel: Navigating PhD studies PLMW Hila PelegUniversity of California at San Diego, Nick GiannarakisUniversity of Wisconsin-Madison, Anne-Kathrin SchmuckMPI-SWS, Sacha-Élie AyounImperial College London, Farzaneh DerakhshanCarnegie Mellon University, Soham ChakrabortyIIT Delhi | ||
15:00 - 16:00 | Keynote 2PEPM at PEPM Chair(s): Torben MogensenDIKU, University of Copenhagen Live stream: https://www.youtube.com/watch?v=Ps_rUSG1yg0 | ||
15:00 60mKeynote | Erasure In Dependently Typed Programming PEPM Matúš TejiščákChordify | ||
15:30 - 16:00 | |||
15:30 30mSocial Event | Tuesday Shuffle-Space Time Workshops and Co-located Events | ||
16:00 - 16:45 | Compilers and InterpretersCPP at CPP Chair(s): Freek WiedijkRadboud University Nijmegen Streamed session: https://youtu.be/TVqCuMMTuos | ||
16:00 15mTalk | A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award CPP Magnus O. MyreenChalmers University of Technology Pre-print Media Attached | ||
16:15 15mTalk | Lutsig: A Verified Verilog Compiler for Verified Circuit Development CPP Andreas LööwChalmers University of Technology Pre-print Media Attached | ||
16:30 15mTalk | Towards Efficient and Verified Virtual Machines for Dynamic Languages CPP Martin DesharnaisUniversität der Bundeswehr München, Stefan BrunthalerUniversität der Bundeswehr München Pre-print Media Attached | ||
16:00 - 17:30 | |||
16:00 15mTalk | A Limited Case for Reification by Type Inference CoqPL Jason GrossMIT CSAIL Media Attached File Attached | ||
16:15 15mTalk | Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml CoqPL File Attached | ||
16:30 15mTalk | Record Updates in Coq CoqPL Tej ChajedMassachusetts Institute of Technology, USA Media Attached File Attached | ||
16:45 15mBreak | Break CoqPL | ||
17:00 15mTalk | The B+-tree Index as a Verified Software Unit CoqPL Anastasiya Kravchuk-KirilyukHarvard University, Andrew AppelPrinceton, Lennart BeringerPrinceton University File Attached | ||
17:15 15mTalk | Automated Synthesis of Verified Firewalls CoqPL Shardul ChiplunkarMassachusetts Institute of Technology, Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology File Attached | ||
16:00 - 17:30 | Declarative Approaches to Testing and DebuggingPADL at PADL Chair(s): Paul TarauUniversity of North Texas | ||
16:00 30mResearch paper | ConFuzz: Coverage-guided Property Fuzzing for Event-driven Programs PADL Link to publication | ||
16:30 30mResearch paper | Causal-Consistent Reversible Debugging: Improving CauDEr PADL Juan José González-AbrilMiST, VRAIN, Universitat Politecnica de Valencia, German VidalUniversitat Politecnica de Valencia | ||
17:00 30mResearch paper | Declarative Debugging of XML Queries PADL | ||
16:00 - 17:30 | |||
16:00 45mTalk | Connecting Information Flow Types to Runtime Monitors via Gradual Typing PLMW Limin JiaCarnegie Mellon University | ||
16:45 45mTalk | Emotional Machines PLMW Aaron TuronFastly | ||
16:00 - 17:00 | |||
16:00 60mKeynote | Generative Program Analysis and Beyond: The Power of Domain-Specific Languages VMCAI Media Attached | ||
16:30 - 17:30 | Session 4PEPM at PEPM Chair(s): Jeremy YallopUniversity of Cambridge Live stream: https://www.youtube.com/watch?v=BmBSJFkfL2M | ||
16:30 30mShort-paper | Staged Effects and Handlers for Modular Languages with Abstraction PEPM Casper Bach PoulsenDelft University of Technology, Cas van der RestDelft University of Technology, Tom SchrijversKU Leuven Media Attached File Attached | ||
17:00 30mShort-paper | Automatic Differentiation via Effects and Handlers: An Implementation in Frank PEPM Jesse SigalUniversity of Edinburgh Media Attached File Attached | ||
16:45 - 17:30 | Rewriting and Automated ReasoningCPP at CPP Chair(s): Cyril CohenUniversité Côte d’Azur, Inria, France Streamed session: https://youtu.be/TVqCuMMTuos?t=2806 | ||
16:45 15mTalk | A Modular Isabelle Framework for Verifying Saturation Provers CPP Pre-print Media Attached | ||
17:00 15mTalk | An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR CPP Pre-print Media Attached | ||
17:15 15mTalk | A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems CPP Alexander LochmannUniversity of Innsbruck, Aart MiddeldorpUniversity of Innsbruck, Fabian MitterwallnerUniversity of Innsbruck, Bertram Felgenhauer Pre-print Media Attached | ||
17:00 - 17:30 | |||
17:00 15mTalk | A Synchronous Effects Logic for Temporal Verification of Pure Esterel VMCAI Media Attached | ||
17:15 15mTalk | A Design of GPU-Based Quantitative Model Checking VMCAI Media Attached | ||
17:30 - 18:00 | |||
17:30 30mBreak | Tuesday Coffee Break 2 Workshops and Co-located Events | ||
18:00 - 18:30 | AI and Machine LearningCPP at CPP Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK Streamed session: https://youtu.be/6NJdWdiZEiA | ||
18:00 15mTalk | A Formal Proof of PAC Learnability for Decision Stumps CPP Joseph TassarottiBoston College, Koundinya VajjhaUniversity of Pittsburgh, Anindya BanerjeeIMDEA Software Institute, Jean-Baptiste TristanBoston College Pre-print Media Attached | ||
18:15 15mTalk | CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq CPP Koundinya VajjhaUniversity of Pittsburgh, Avraham ShinnarIBM Research, Barry TragerIBM Research, Vasily PestunIBM Research; IHES, Nathan FultonIBM Research Pre-print Media Attached | ||
18:00 - 18:45 | |||
18:00 15mTalk | Verification of Algorithm and Code Generation for Signal Transforms CoqPL File Attached | ||
18:15 15mTalk | An experience report on writing usable DSLs in Coq CoqPL File Attached | ||
18:30 15mBreak | Break CoqPL | ||
18:00 - 19:30 | Foundations and Programming Concepts at WorkPADL at PADL Chair(s): Mario AlvianoUniversity of Calabria | ||
18:00 30mResearch paper | Synchronous Message-Passing with Priority PADL Cheng-En ChuangUniversity at Buffalo, Grant IraciUniversity at Buffalo, Lukasz ZiarekSUNY Buffalo, USA | ||
18:30 30mResearch paper | Putting gradual types to work PADL Bhargav ShivkumarState University of New York - University at Buffalo, Enrique NaudonBloomberg, Lukasz ZiarekSUNY Buffalo, USA | ||
19:00 30mShort-paper | Psamathe: A DSL with Flows for Safe Blockchain Assets (extended abstract) PADL Reed OeiUniversity of Illinois at Urbana-Champaign, Michael CoblenzUniversity of Maryland at College Park, Jonathan AldrichCarnegie Mellon University File Attached | ||
18:00 - 19:00 | Session 5PEPM at PEPM Chair(s): Torben MogensenDIKU, University of Copenhagen Live stream: https://www.youtube.com/watch?v=VJZcAtvGOyE | ||
18:00 30mResearch paper | A Type-Safe Structure Editor Calculus PEPM Christian GodiksenDepartment of Computer Science, Aalborg University, Thomas HerrmannDepartment of Computer Science, Aalborg University, Hans HüttelDepartment of Computer Science, Aalborg University, Mikkel Korup LauridsenDepartment of Computer Science, Aalborg University, Iman OwliaieDepartment of Computer Science, Aalborg University Media Attached | ||
18:30 30mResearch paper | Strictly Capturing Non-Strict Closures PEPM Zachary SullivanUniversity of Oregon, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA Media Attached | ||
18:00 - 19:30 | |||
18:00 90mTalk | SRC Finalists Presentations Student Research Competition | ||
18:00 - 18:30 | Case StudiesVMCAI at VMCAI Chair(s): Roderick BloemInstitute of Software Technology, Graz University of Technology | ||
18:00 15mTalk | Formal Semantics and Verification of Network Based Biocomputation Circuits VMCAI Michelle Aluf-MedinaBar Ilan University, Till KortenTU Dresden, Avraham RavivBar Ilan University, Dan Nicolau Jr.Molecular Sense, Hillel KuglerBar Ilan University Media Attached | ||
18:15 15mTalk | Netter: Probabilistic, Stateful Network Models VMCAI Han ZhangCarnegie Mellon University, Chi Zhang, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Yuvraj AgarwalCarnegie Mellon University, Matt FredriksonCarnegie Mellon University, Limin JiaCarnegie Mellon University Media Attached | ||
18:30 - 19:30 | |||
18:30 60mTalk | Chairs' report and community meeting CPP Media Attached File Attached | ||
18:30 - 19:30 | |||
18:30 15mTalk | Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories VMCAI Martin BrombergerMPI-INF, Alberto FioriMax Planck Institute for Informatics, Christoph WeidenbachMPI-INF Media Attached | ||
18:45 15mTalk | Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching VMCAI Media Attached | ||
19:00 15mTalk | On Pre- and Inprocessing for Weighted MaxSAT VMCAI Tobias PaxianUniversity of Freiburg, Pascal RaiolaUniversity of Freiburg, Bernd BeckerAlbert-Ludwigs-University Freiburg Media Attached | ||
19:15 15mTalk | Compositional Satisfiability Solving in Separation Logic VMCAI Quang Loc LeUniversity College London, UK Media Attached | ||
18:45 - 19:30 | |||
18:45 45mDemonstration | Session with the Coq Development Team CoqPL | ||
19:30 - 20:00 | |||
19:30 30mBreak | Welcome to Copenhagen! Workshops and Co-located Events | ||
19:30 - 20:30 | Keynote 3PEPM at PEPM Chair(s): Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK Live stream: https://www.youtube.com/watch?v=MMq4J8eti1g | ||
19:30 60mKeynote | Hardware DSLs PEPM Pat HanrahanStanford University, USA | ||
Wed 20 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 20 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
04:30 - 05:30 | |||
04:30 60mSocial Event | Panel Discussion 3: Work/Life Balance POPL Meetups Andreea CosteaSchool of Computing, National University Of Singapore, Atsushi IgarashiKyoto University, Japan, KC SivaramakrishnanIIT Madras, Soham ChakrabortyIIT Delhi, India | ||
07:00 - 08:00 | |||
07:00 60mBreak | Wednesday Coffee Break POPL Meetups | ||
15:15 - 15:45 | |||
15:15 30mSocial Event | Wednesday Breakfast Tables POPL | ||
17:00 - 18:00 | |||
17:00 60mKeynote | The road to a Universal Internet Machine (Demystifying Blockchain Protocols)Invited Talk POPL Rachid GuerraouiEPFL Media Attached | ||
19:30 - 20:00 | |||
19:30 30mSocial Event | Happy Hour POPL | ||
19:30 - 20:00 | |||
19:30 30mIndustry talk | Sponsor Reception POPL Media Attached | ||
20:00 - 21:00 | |||
20:00 60mSocial Event | Trivia Night POPL | ||
20:00 - 20:30 | |||
20:00 30mMeeting | SIGPLAN CARES POPL P: Stephanie WeirichUniversity of Pennsylvania, P: Alexandra SilvaUniversity College London, P: Shriram KrishnamurthiBrown University, United States, P: David WalkerPrinceton University, USA | ||
Thu 21 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 21 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
02:00 - 03:00 | |||
02:00 60mSocial Event | POPL Cocktail Hour POPL | ||
04:00 - 04:30 | |||
04:00 30mMeeting | SIGPLAN CARES POPL P: Stephanie WeirichUniversity of Pennsylvania, P: Hongseok YangKAIST, P: Shriram KrishnamurthiBrown University, United States, P: David WalkerPrinceton University, USA | ||
04:30 - 05:30 | |||
04:30 60mSocial Event | Panel Discussion 4: Finding Friends and Collaborators in Academia POPL Meetups Aseem RastogiMicrosoft Research, Atsushi IgarashiKyoto University, Japan, Christine RizkallahUNSW Sydney, Jeehoon KangKAIST, Youyou CongTokyo Institute of Technology | ||
07:00 - 08:00 | |||
07:00 60mBreak | Thursday Coffee Break POPL Meetups | ||
15:15 - 15:45 | |||
15:15 30mSocial Event | Topic Oriented Discussions POPL | ||
15:45 - 15:55 | |||
15:45 10mAwards | Most Influential POPL Paper POPL Media Attached | ||
15:55 - 16:00 | |||
15:55 5mAwards | Student Research Competition Results Student Research Competition | ||
16:00 - 17:00 | |||
16:00 10mTalk | Verifying Observational Robustness Against a C11-style Memory Model POPL Link to publication DOI | ||
16:10 10mTalk | Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper POPL Link to publication DOI | ||
16:20 10mTalk | Modeling and Analyzing Evaluation Cost of CUDA Kernels POPL Link to publication DOI | ||
16:30 10mTalk | Optimal Prediction of Synchronization-Preserving Races POPL Umang MathurUniversity of Illinois at Urbana-Champaign, Andreas PavlogiannisAarhus University, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign Link to publication DOI Pre-print | ||
16:40 10mTalk | Taming x86-TSO Persistency POPL Link to publication DOI Pre-print | ||
16:50 10mBreak | Break POPL | ||
17:00 - 18:00 | |||
17:00 60mKeynote | Dynamical Systems and Program AnalysisInvited Talk POPL James WorrellUniversity of Oxford File Attached | ||
19:30 - 20:30 | |||
19:30 60mMeeting | Business Meeting & Townhall POPL | ||
20:30 - 21:30 | |||
20:30 60mMeeting | Iris meetup POPL Meetups | ||
21:00 - 22:00 | |||
21:00 60mSocial Event | Games Programming Languages BoF Session POPL Meetups | ||
Fri 22 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Fri 22 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
07:00 - 08:00 | |||
07:00 60mBreak | Friday Coffee Break POPL Meetups | ||
15:15 - 15:45 | |||
15:15 30mSocial Event | Friday Breakfast Tables POPL | ||
17:00 - 18:00 | |||
17:00 60mKeynote | Toward a Programmable Cloud: CALM Foundations and Open ChallengesInvited Talk POPL Media Attached File Attached | ||
18:30 - 19:00 | |||
18:30 10mTalk | Generating Collection Transformations from Proofs POPL Link to publication DOI | ||
18:40 10mTalk | Semantics-Guided Synthesis POPL Jinwoo KimUniversity of Wisconsin-Madison, Qinheping HuUniversity of Wisconsin-Madison, USA, Loris D'AntoniUniversity of Wisconsin-Madison, USA, Thomas RepsUniversity of Wisconsin--Madison Link to publication DOI | ||
18:50 10mTalk | Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis POPL Woosuk LeeHanyang University, South Korea Link to publication DOI | ||
18:30 - 19:00 | |||
18:30 10mTalk | Cyclic Proofs, System T, and the Power of Contraction POPL Link to publication DOI | ||
18:40 10mTalk | egg: Fast and Extensible Equality SaturationDistinguished Paper POPL Max WillseyUniversity of Washington, USA, Chandrakana NandiUniversity of Washington, USA, Yisu Remy WangUniversity of Washington, Oliver FlattUniversity of Utah, Zachary TatlockUniversity of Washington, Seattle, Pavel PanchekhaUniversity of Utah Link to publication DOI Pre-print | ||
18:50 10mTalk | Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS POPL David ZhaoThe University of Sydney, Pavle SuboticMicrosoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard ScholzUniversity of Sydney, Australia Link to publication DOI | ||
19:00 - 20:00 | |||
19:00 60mAwards | Robin Milner Award Talk: "Structural Language Models of Code" POPL Media Attached | ||
20:00 - 20:30 | |||
20:00 30mSocial Event | Farewell Reception POPL | ||
21:00 - 22:00 | |||
21:00 60mMeeting | Iris meetup #2 POPL Meetups | ||