VenueWestin Philadelphia
Room nameSalon I
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited TalkVMCAI at Salon I
Chair(s): Thomas Wies New York University
09:00
60m
Keynote
Sequential Information FlowRemote
VMCAI
Thomas A. Henzinger IST Austria, Austria
10:20 - 11:50
Static Analysis and Abstract InterpretationVMCAI at Salon I
Chair(s): Thomas Wies New York University
10:20
30m
Paper
Relational String Abstract DomainsRemote
VMCAI
Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences, Martina Olliaro Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and Statistics, Agostino Cortesi Università Ca' Foscari Venezia, Pietro Ferrara Università Ca' Foscari, Venezia, Italy
10:50
30m
Paper
Lightweight Shape Analysis based on Physical TypesInPerson
VMCAI
Olivier Nicole CEA LIST, France, Matthieu Lemerre CEA LIST, France, Xavier Rival INRIA/CNRS/ENS Paris
11:20
30m
Paper
A Flow-Insensitive-Complete Program RepresentationRemote
VMCAI
Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Facebook Paris
13:30 - 14:30
Privacy and SecurityVMCAI at Salon I
Chair(s): Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences
13:30
30m
Paper
Verifying Pufferfish Privacy in Hidden Markov ModelsRemote
VMCAI
Depeng Liu Institute of Software, Chinese Academy of Sciences, Bow-Yaw Wang Academia Sinica, Lijun Zhang Institute of Software, Chinese Academy of Sciences
14:00
30m
Paper
Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACERemote
VMCAI
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Jorge A. Navas Certora, inc., Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys, Arie Gurfinkel University of Waterloo
15:05 - 16:35
Satisfiability Modulo TheoriesVMCAI at Salon I
Chair(s): Natarajan Shankar SRI International, USA
15:05
30m
Paper
Generalized Arrays for Stainless FramesRemote
VMCAI
Georg Stefan Schmid EPFL, Switzerland, Viktor Kunčak EPFL, Switzerland
15:35
30m
Paper
NP Satisfiability for Arrays as PowersInPerson
VMCAI
Rodrigo Raya EPFL, Viktor Kunčak EPFL, Switzerland
16:05
30m
Paper
Bit-Precise Reasoning via Int-BlastingRemote
VMCAI
Yoni Zohar Bar Ilan University, Ahmed Irfan Stanford University, Makai Mann Stanford University, Aina Niemetz Stanford University, Andres Nötzli Stanford University, USA, Mathias Preiner Stanford University, Andrew Reynolds University of Iowa, Clark Barrett Stanford University, Cesare Tinelli University of Iowa

Mon 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited TalkVMCAI at Salon I
Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security
09:00
60m
Keynote
Back to the Future: A Fresh Look at Linear Temporal LogicRemote
VMCAI
10:20 - 11:50
Model CheckingVMCAI at Salon I
Chair(s): Arie Gurfinkel University of Waterloo
10:20
30m
Paper
Automata-Driven Partial Order Reduction and Guided Search for LTL Model CheckingRemote
VMCAI
Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba Aalborg University, Nikolaj Jensen Ulrik Aalborg University, Simon Mejlby Virenfeldt Aalborg University
10:50
30m
Paper
Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not TerminateRemote
VMCAI
Rahmadi Trimananda University of California at Irvine, USA, Weiyu Luo University of California, Irvine, Brian Demsky University of California at Irvine, Harry Xu University of California, Los Angeles (UCLA)
Link to publication DOI Pre-print Media Attached File Attached
11:20
30m
Paper
Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsInPerson
VMCAI
Landon Taylor Utah State University, Zhen Zhang Utah State University
13:30 - 14:30
Formal Methods in Machine LearningVMCAI at Salon I
Chair(s): Rupak Majumdar MPI-SWS
13:30
30m
Paper
Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned SystemsRemote
VMCAI
David Bayani Carnegie Mellon University's School of Computer Science, Stefan Mitsch Carnegie Mellon University, USA
14:00
30m
Paper
Bisimulations for Neural Network ReductionInPerson
VMCAI
Pavithra Prabhakar Kansas State University
15:05 - 16:35
Program VerificationVMCAI at Salon I
Chair(s): Elizabeth Polgreen University of Edinburgh
15:05
30m
Paper
High Assurance Software for Financial Regulation and Business PlatformsRemote
VMCAI
Stephen Goldbaum Morgan Stanley, Attila Mihaly Morgan Stanley, Tosha Ellison Fintech Open Source Foundation, Earl Barr UCL, Mark Marron Microsoft Research
15:35
30m
Paper
Loop Verification with Invariants and ContractsRemote
VMCAI
Gidon Ernst Ludwig Maximilian University of Munich
Pre-print
16:05
30m
Paper
Making PROGRESS in Property Directed ReachabilityRemote
VMCAI
Tobias Seufert University of Freiburg, Christoph Scholl University of Freiburg, Arun Chandrasekharan OneSpin Solutions, Munich, Sven Reimer OneSpin Solutions, Munich, Tobias Welp OneSpin Solutions, Munich

Tue 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
SynthesisVMCAI at Salon I
Chair(s): Viktor Kunčak EPFL, Switzerland
09:00
30m
Paper
Gradient-Descent for Randomized Controllers under Partial ObservabilityInPerson
VMCAI
Jip Spel RWTH Aachen University, Linus Heck RWTH Aachen University, Sebastian Junges University of California, Berkeley, Joshua Moerman Open University of the Netherlands, Joost-Pieter Katoen RWTH Aachen University
09:30
30m
Paper
Satisfiability and Synthesis Modulo OraclesRemote
VMCAI
Elizabeth Polgreen University of Edinburgh, Andrew Reynolds University of Iowa, Sanjit Seshia UC Berkeley
10:20 - 11:50
Probabilistic SystemsVMCAI at Salon I
Chair(s): Pavithra Prabhakar Kansas State University
10:20
30m
Paper
Out of Control: Reducing Probabilistic Models by Control-State EliminationInPerson
VMCAI
Tobias Winkler RWTH Aachen University, Johannes Lehmann RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University
10:50
30m
Paper
STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model CheckingRemote
VMCAI
Riley Roberts Utah State University, Thakur Neupane The MathWorks, Inc., Lukas Buecherl University of Colorado, Boulder, Chris Myers University of Colorado, Boulder, Zhen Zhang Utah State University
11:20
30m
Paper
EPMC Gets Knowledge in Multi-Agent SystemsRemote
VMCAI
Chen Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Ernst Moritz Hahn University of Twente, Yong Li Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Meng Sun Peking University, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
13:30 - 14:30
Invited TalkVMCAI at Salon I
Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security
13:30
60m
Keynote
Simplifying Concurrent Programming via Synchronization SynthesisRemote
VMCAI
Işıl Dillig University of Texas at Austin
15:05 - 16:05
Static Analysis and Hybrid SystemsVMCAI at Salon I
Chair(s): Yoni Zohar Bar Ilan University
15:05
30m
Paper
Fast Three-Valued Abstract Bit-Vector ArithmeticInPerson
VMCAI
Jan Onderka Czech Technical University in Prague, Stefan Ratschan The Czech Academy of Sciences
15:35
30m
Paper
Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid AutomataRemote
VMCAI
Yuming Wu Nanjing University, Lei Bu Nanjing University, Jiawan Wang Nanjing University, Xinyue Ren Nanjing University, Wen Xiong Nanjing University, Xuandong Li Nanjing University

Wed 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

08:50 - 09:00
WelcomePOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania, Hongseok Yang KAIST
09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania
09:00
60m
Keynote
Principles of Programming Language TranslatorsRemoteInvited Talk
POPL
Alfred V. Aho Columbia University
10:20 - 12:00
Automated VerificationPOPL at Salon I
Chair(s): Roberto Giacobazzi University of Verona
10:20
25m
Research paper
Software Model-Checking as Cyclic-Proof SearchRemote
POPL
Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI Media Attached
10:45
25m
Research paper
Induction Duality: Primal-Dual Search for InvariantsRemote
POPL
Oded Padon VMware Research; Stanford University, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford University
DOI Media Attached
11:10
25m
Research paper
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive FunctionsRemote
POPL
Hari Govind V K University of Waterloo, Sharon Shoham Tel Aviv University, Arie Gurfinkel University of Waterloo
DOI Media Attached
11:35
25m
Research paper
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and VariablesRemote
POPL
Taolue Chen Birkbeck University of London, Alejandro Flores Lamas Royal Holloway University of London, Matthew Hague Royal Holloway University of London, Zhilei Han Tsinghua University, Denghang Hu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
DOI Media Attached
13:30 - 14:45
Program AnalysisPOPL at Salon I
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign; VMware
13:30
25m
Research paper
Property-Directed Reachability as Abstract Interpretation in the Monotone TheoryRemote
POPL
Yotam M. Y. Feldman Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv University, James R. Wilcox Certora
DOI Media Attached
13:55
25m
Research paper
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program AnalysisInPerson
POPL
Marco Campion University of Verona, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Verona
DOI Media Attached
14:20
25m
Research paper
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented ProgramsInPerson
POPL
Minseok Jeon Korea University, Hakjoo Oh Korea University
DOI Media Attached
15:05 - 16:20
Algorithmic Verification 1POPL at Salon I
Chair(s): Qirun Zhang Georgia Institute of Technology
15:05
25m
Research paper
Efficient Algorithms for Dynamic Bidirected Dyck-ReachabilityRemote
POPL
Yuanbo Li Georgia Institute of Technology, Kris Satya Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
DOI Media Attached
15:30
25m
Research paper
The Decidability and Complexity of Interleaved Bidirected Dyck ReachabilityRemote
POPL
Adam Husted Kjelstrøm Aarhus University, Andreas Pavlogiannis Aarhus University
DOI Media Attached
15:55
25m
Research paper
Subcubic Certificates for CFL ReachabilityRemote
POPL
Dmitry Chistikov University of Warwick, Rupak Majumdar MPI-SWS, Philipp Schepper CISPA
DOI Media Attached
16:40 - 17:30
Algorithmic Verification 2POPL at Salon I
Chair(s): Qirun Zhang Georgia Institute of Technology
16:40
25m
Research paper
Context-Bounded Verification of Thread PoolsRemote
POPL
DOI Media Attached
17:05
25m
Research paper
What’s Decidable about Linear Loops?InPerson
POPL
Toghrul Karimov MPI-SWS, Engel Lefaucheux MPI-SWS, Joël Ouaknine MPI-SWS, David Purser MPI-SWS, Anton Varonka MPI-SWS, Markus A. Whiteland MPI-SWS, James Worrell University of Oxford
DOI Pre-print Media Attached

Thu 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Michael Hicks University of Maryland at College Park
09:00
60m
Keynote
Better Learning through Programming LanguagesInvited TalkInPerson
POPL
Armando Solar-Lezama Massachusetts Institute of Technology
10:20 - 12:00
Foundation and Verification of Machine-Learning SystemsPOPL at Salon I
Chair(s): Gilbert Bernstein University of California at Berkeley
10:20
25m
Research paper
A Dual Number Abstraction for Static Analysis of Clarke JacobiansInPerson
POPL
Jacob Laurel University of Illinois at Urbana-Champaign, Rem Yang University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Sasa Misailovic University of Illinois at Urbana-Champaign
DOI Media Attached
10:45
25m
Research paper
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote
POPL
Faustyna Krawiec University of Cambridge, Simon Peyton Jones Microsoft Research, Neel Krishnaswami University of Cambridge, Tom Ellis Microsoft Research, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Graphcore
DOI Media Attached
11:10
25m
Research paper
Interval Universal Approximation for Neural NetworksInPerson
POPL
Zi Wang University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison, Gautam Prakriya Chinese University of Hong Kong, Somesh Jha University of Wisconsin
DOI Media Attached
11:35
25m
Research paper
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull ApproximationsInPerson
POPL
Mark Niklas Müller ETH Zurich, Gleb Makarchuk ETH Zurich, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich
DOI Media Attached
13:30 - 14:45
TypesPOPL at Salon I
Chair(s): Stephanie Weirich University of Pennsylvania
13:30
25m
Research paper
On Type-Cases, Union Elimination, and Occurrence TypingInPerson
POPL
Giuseppe Castagna CNRS; Université de Paris, Mickaël Laurent Université de Paris, Kim Nguyễn Université Paris-Saclay, Matthew Lutze Université de Paris
DOI Media Attached
13:55
25m
Research paper
Oblivious Algebraic Data TypesInPerson
POPL
Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
DOI Media Attached
14:20
25m
Research paper
SolType: Refinement Types for Arithmetic Overflow in SolidityRemote
POPL
Bryan Tan University of California at Santa Barbara, Benjamin Mariano University of Texas at Austin, Shuvendu K. Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara
DOI Media Attached
15:05 - 16:20
SystemsPOPL at Salon I
Chair(s): Arthur Azevedo de Amorim Boston University
15:05
25m
Research paper
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFIInPerson
POPL
Matthew Kolosick University of California at San Diego, Shravan Ravi Narayan University of California at San Diego, Evan Johnson University of California at San Diego, Conrad Watt University of Cambridge, Michael LeMay Intel Labs, Deepak Garg MPI-SWS, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego
DOI Media Attached
15:30
25m
Research paper
Relational E-matchingRemote
POPL
Yihong Zhang University of Washington, Yisu Remy Wang University of Washington, Max Willsey University of Washington, Zachary Tatlock University of Washington
DOI Media Attached
15:55
25m
Research paper
Linked Visualisations via Galois DependenciesRemote
POPL
Roly Perera Alan Turing Institute, Minh Nguyen University of Bristol, Tomas Petricek University of Kent, Meng Wang University of Bristol
DOI Media Attached
16:40 - 18:00
POPL Business Meeting and SIGPLAN AwardsPOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania
16:40
10m
Meeting
General Chair ReportInPerson
POPL
Rajeev Alur University of Pennsylvania
16:50
10m
Meeting
Program Chair ReportRemote
POPL
17:00
10m
Meeting
Virtualization Chair ReportRemote
POPL
Adam Chlipala Massachusetts Institute of Technology
17:10
5m
Meeting
POPL 2023 ReportInPerson
POPL
Andrew Myers Cornell University
17:15
3m
Awards
Student Research Competition WinnersRemote
POPL
Azalea Raad Imperial College London
17:18
3m
Awards
POPL'22 Distinguished PapersRemote
POPL
17:21
3m
Awards
SIGPLAN Reynolds Dissertation AwardRemote
POPL
Işıl Dillig University of Texas at Austin
17:24
3m
Awards
POPL Most Influential Paper AwardRemote
POPL
Tony Hosking Australian National University
17:27
3m
Awards
SIGPLAN Programming Languages Achievements AwardRemote
POPL
Işıl Dillig University of Texas at Austin
17:30
10m
Awards
Remarks by SIGPLAN PL Achievements Award WinnerRemote
POPL

17:40
20m
Meeting
Open Forum for Q&AInPerson
POPL
Rajeev Alur University of Pennsylvania

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Adam Chlipala Massachusetts Institute of Technology
09:00
60m
Keynote
Coalgebra for the working programming languages researcherRemoteInvited Talk
POPL
Alexandra Silva Cornell University
10:20 - 12:00
Distributed or Network ProgramsPOPL at Salon I
Chair(s): J. Garrett Morris The University of Iowa
10:20
25m
Research paper
Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson
POPL
Andrew K. Hirsch MPI-SWS, Deepak Garg MPI-SWS
DOI Media Attached
10:45
25m
Research paper
Fair Termination of Binary SessionsRemote
POPL
Luca Ciccone University of Turin, Luca Padovani University of Turin
DOI Media Attached
11:10
25m
Research paper
Safe, Modular Packet Pipeline ProgrammingRemote
POPL
Devon Loehr Princeton University, David Walker Princeton University
DOI Media Attached
11:35
25m
Research paper
Dependently-Typed Data Plane ProgrammingRemote
POPL
Matthias Eichholz TU Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt
DOI Media Attached
12:30 - 13:30
ShutdownPLDiversity, Equity and Inclusion at Salon I
Chair(s): David Justo Microsoft Azure
12:30
60m
Talk
Designing and Developing for the Black ExperienceRemote
Diversity, Equity and Inclusion
Brittany Johnson George Mason University
13:30 - 14:45
TOPLAS SessionPOPL at Salon I
Chair(s): Andrew Myers Cornell University
13:30
25m
Talk
Armed cats: formal concurrency modelling at ArmRemote
POPL
Jade Alglave University College London, Will Deacon ARM Ltd., Richard Grisenthwaite , Antoine Hacquard EPITA, LRDE, Luc Maranget Inria
13:55
25m
Talk
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs Remote
POPL
Emanuele D’Osualdo MPI-SWS, Julian Sutherland Imperial College London, Azadeh Farzan University of Toronto, Philippa Gardner Imperial College London
DOI
14:20
25m
Talk
Gradualizing the Calculus of Inductive ConstructionsRemote
POPL
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Kenji Maillard Inria Nantes & University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile
15:05 - 16:20
Verification 1POPL at Salon I
Chair(s): Lennart Beringer Princeton University
15:05
25m
Research paper
Certifying Derivation of State Machines from CoroutinesInPerson
POPL
Mirai Ikebuchi National Institute of Informatics, Andres Erbsen Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology
DOI Media Attached
15:30
25m
Research paper
VIP: Verifying Real-World C Idioms with Integer-Pointer CastsRemote
POPL
Rodolphe Lepigre MPI-SWS, Michael Sammler MPI-SWS, Kayvan Memarian University of Cambridge, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Peter Sewell University of Cambridge
DOI Media Attached
15:55
25m
Research paper
Verified Compilation of C Programs with a Nominal Memory ModelRemote
POPL
Yuting Wang Shanghai Jiao Tong University, Ling Zhang Shanghai Jiao Tong University, Zhong Shao Yale University, Jérémie Koenig Yale University
DOI Media Attached
16:40 - 17:30
Verification 2POPL at Salon I
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
16:40
25m
Research paper
Verified Tensor-Program Optimization Via High-Level Scheduling RewritesRemote
POPL
Amanda Liu Massachusetts Institute of Technology, Gilbert Bernstein University of California at Berkeley, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
DOI Media Attached
17:05
25m
Research paper
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding ModesDistinguished PaperRemote
POPL
Jay P. Lim Rutgers University, Santosh Nagarakatte Rutgers University
DOI Media Attached

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited Talk ICoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
09:00
60m
Keynote
Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofsRemote
CoqPL
10:20 - 12:00
Contributed Talks (Morning)CoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
10:20
20m
Talk
A Visual Ltac Debugger in CoqIDERemote
CoqPL
S: Jim Fehrle None
File Attached
10:40
20m
Talk
Scrap your boilerplate definitions in 10 lines of Ltac!InPerson
CoqPL
S: Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
File Attached
11:00
20m
Talk
Tealeaves: Categorical structures for syntaxInPerson
CoqPL
S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USA
File Attached
11:20
20m
Talk
Towards a Formalization of Nominal Sets in CoqRemote
CoqPL
S: Fabrício S. Paranhos Universidade Federal de Goiás, Daniel Ventura Universidade Federal de Goiás
File Attached
11:40
20m
Talk
A Case for Lightweight Interfaces in CoqInPerson
CoqPL
David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems
File Attached
13:30 - 14:30
Invited Talk IICoqPL at Salon I
Chair(s): Amin Timany Aarhus University
13:30
60m
Keynote
Verifying Concurrent, Crash-Safe Systems with PerennialRemote
CoqPL
I: Joseph Tassarotti Boston College
14:30 - 14:50
Contributed Talk (Afternoon)CoqPL at Salon I
Chair(s): Amin Timany Aarhus University
14:30
20m
Talk
A Verified Pipeline from a Specification Language to Optimized, Safe RustRemote
CoqPL
S: Rasmus Holdsbjerg-Larsen Aarhus University, Bas Spitters Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University
Pre-print File Attached
15:05 - 15:50
Session with the Coq Development TeamCoqPL at Salon I
Chair(s): Amin Timany Aarhus University
15:05
45m
Panel
Session with the Coq Development TeamRemote
CoqPL
S: Matthieu Sozeau Inria, S: Yves Bertot INRIA, S: Hugo Herbelin , S: Emilio Jesús Gallego Arias INRIA, S: Jason Gross MIT CSAIL

Sun 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

Mon 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

Tue 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

Wed 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

Thu 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

Thu 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Salon I