VenueWestin Philadelphia
Room nameSalon III
Room InformationNo extra information available
Program

This program is tentative and subject to change.

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 - 09:45
Research keynoteProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
09:00
45m
Keynote
Research keynote -- Programming Languages and Law: A Research Agenda for a New FieldRemote
ProLaLa
James Grimmelmann Cornell University
File Attached
09:45 - 10:05
Long talks #1ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
09:45
20m
Talk
Legal CalculiInPerson
ProLaLa
Shrutarshi Basu Harvard University, Anshuman Mohan Cornell University, James Grimmelmann Cornell University, Nate Foster Cornell University
File Attached
10:20 - 12:00
Long talks #2ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
10:20
20m
Talk
Position Paper: LLD is All You NeedRemote
ProLaLa
L. Thorne McCarty Rutgers, The State University of New Jersey
Pre-print
10:40
20m
Talk
Logical English as a Programming Language for the LawRemote
ProLaLa
Robert Kowalski Imperial College London, Jacinto Dávila Contratos Lógicos. C.A. and Universidad de Los Andes, Miguel Calejo logicalcontracts.com
File Attached
11:00
20m
Talk
Introduction of PROLEG (PROlog-based LEGal reasoning support system)Remote
ProLaLa
Ken Satoh National Institute of Informatics, Wachara Fungwacharakorn National Institute of Informatics, Kanae Tsushima National Institute of Informatics, Japan
File Attached
11:20
20m
Talk
DPCL: a Language Template for Normative SpecificationsRemote
ProLaLa
Giovanni Sileno University of Amsterdam, Thomas van Binsbergen University of Amsterdam, Matteo Pascucci Slovak Academy of Science, Tom van Engers Leibniz Institute / University of Amsterdam / TNO
Pre-print
11:40
20m
Talk
Reflections on the design and application of eFLINTRemote
ProLaLa
Pre-print File Attached
13:30 - 14:10
Short talksProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
13:30
10m
Talk
Littleton: An Educational Environment for Property LawRemote
ProLaLa
Shrutarshi Basu Harvard University, Anshuman Mohan Cornell University, James Grimmelmann Cornell University, Nate Foster Cornell University
File Attached
13:40
10m
Talk
Modeling Administrative Discretion Using Goal-Directed Answer Set ProgrammingRemote
ProLaLa
Joaquín Arias Universidad Rey Juan Carlos, Mar Moreno-Rebato Universidad Rey Juan Carlos, José Antonio Rodríguez-García Universidad Rey Juan Carlos, Sascha Ossowski Universidad Rey Juan Carlos
Pre-print Media Attached File Attached
13:50
10m
Talk
Probabilistic programming for Employment Tribunal remediesRemote
ProLaLa
James Cheney University of Edinburgh; Alan Turing Institute
14:00
10m
Talk
Prevalence of Expression Types in Legislative TextRemote
ProLaLa
Jason Morris Service Canada, Lexpedite Legal Technology
14:10 - 14:50
Long talks #3ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
14:10
20m
Talk
Law Smells: Defining and Detecting Problematic Patterns in Legal DraftingRemote
ProLaLa
Corinna Coupette Max Planck Institute for Informatics, Saarbrücken, Germany, Dirk Hartung Center for Legal Technology and Data Science, Bucerius Law School, Hamburg, Germany, Janis Beckedorf Ruprecht-Karls-Universität Heidelberg, Heidelberg, Germany, Maximilian Böther Hasso Plattner Institute, University of Potsdam, Potsdam, Germany, Daniel Martin Katz Illinois Tech – Chicago Kent College of Law, Chicago, IL, USA
Pre-print File Attached
14:30
20m
Talk
Cod(e)ifying The LawInPerson
ProLaLa
Nel Escher University of Michigan, Jeffrey Bilik University of Michigan, Alexander Miller University of Michigan, Jennifer Jiyoung Huseby University of Michigan, Divya Ramesh University of Michigan, Alice Liu University of Michigan, Sam Mikell University of Michigan, Nina Cahill University of Michigan, Ben Green University of Michigan, Nikola Banovic University of Michigan
File Attached
15:05 - 15:25
Long talks #4ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
15:05
20m
Talk
Stipula: a domain specific language for legal contractsRemote
ProLaLa
Silvia Crafa University of Padova, Cosimo Laneve University of Bologna, Giovanni Sartor University of Bologna
Pre-print File Attached
15:25 - 16:10
Industry keynoteProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
15:25
45m
Industry talk
Industry keynote -- What does a toolchain for legislation eventually become?Remote
ProLaLa
Davin Fifield Oracle, Surend Dayal Australian National University, Don Syme Microsoft
16:10 - 16:30
Long talks #5ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
16:10
20m
Talk
Ergo - a programming language for Smart Legal ContractsRemote
ProLaLa
Niall Roche Mishcon de Reya,University College London,Accord Project, Jerome Simeon Clause, Walter Hernandez Mishcon de Reya,Accord Project, Eason Chen Accord Project, Dan Selman Docusign,Accord Project
Pre-print File Attached
16:40 - 17:40
Long talks #6ProLaLa at Salon III
Chair(s): Shrutarshi Basu Harvard University
16:40
20m
Talk
A General Library of Legal ComponentsRemote
ProLaLa
Chris Bailey University of Illinois College of Law
Link to publication
17:00
20m
Talk
Overview of the CCLAW L4 projectRemote
ProLaLa
Avishkar Mahajan Singapore Management University, Martin Strecker Singapore Management University, Meng Weng Wong Singapore Management University
17:20
20m
Talk
Turning Catala into a Proof Platform for the LawRemote
ProLaLa
Alain Delaët INRIA, ENS Lyon, Denis Merigoux INRIA, Aymeric Fromherz Inria
Pre-print

Mon 17 Jan

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

08:50 - 09:00
Welcome from the chairsCPP at Salon III
Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania
09:00 - 10:00
Invited TalkCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
09:00
60m
Talk
Coq’s vibrant ecosystem for verification engineeringInPerson
CPP
I: Andrew Appel Princeton
13:30 - 15:10
Semantics and Program VerificationCPP at Salon III
Chair(s): Benjamin Delaware Purdue University
13:30
25m
Talk
A Compositional Proof Framework for FRETish RequirementsRemote
CPP
Esther Conrad NASA LaRC, Laura Titolo NIA/NASA LaRC, Dimitra Giannakopoulou NASA Ames Research Center, Thomas Pressburger NASA ARC, Aaron Dutle NASA Langley Research Center
Pre-print Media Attached
13:55
25m
Talk
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with DerivativesRemote
CPP
Derek Egolf Northeastern University, Sam Lasser Tufts University, Kathleen Fisher Tufts University
Media Attached
14:20
25m
Talk
Formally Verified Superblock SchedulingInPerson
CPP
Cyril Six Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Leo Gourdin Université Grenoble-Alpes, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Justus Fasse Université Grenoble-Alpes; KU Leuven, Nicolas Nardino École normale supérieure de Lyon
DOI Pre-print
14:45
25m
Talk
Overcoming Restraint: Composing Verification of Foreign Functions with CogentRemote
CPP
Louis Cheung University of Melbourne, Liam O'Connor University of Edinburgh, Christine Rizkallah University of Melbourne
Pre-print
15:30 - 17:10
Security and Distributed SystemsCPP at Salon III
Chair(s): Alwyn Goodloe NASA Langley Research Center
15:30
25m
Talk
Reflection, Rewinding, and Coin-Toss in EasyCryptRemote
CPP
Denis Firsov Tallinn University of Technology, Dominique Unruh University of Tartu
Pre-print Media Attached
15:55
25m
Talk
A verified algebraic representation of Cairo program executionRemote
CPP
Jeremy Avigad Carnegie Mellon University, USA, Lior Goldberg Starkware Industries Ltd., David Levit Starkware Industries Ltd., Yoav Seginer cdl-lang.org, Netherlands, Alon Titelman Starkware Industries Ltd.
16:20
25m
Talk
Formal Verification of a Distributed Dynamic Reconfiguration ProtocolInPerson
CPP
William Schultz Northeastern University, Ian Dardik Northeastern University, Stavros Tripakis Northeastern University
Pre-print
16:45
25m
Talk
Forward build systems, formallyInPerson
CPP
Sarah Spall Indiana University, Neil Mitchell Meta, Sam Tobin-Hochstadt Indiana University
17:30 - 18:30
Invited TalkCPP at Salon III
Chair(s): Andrei Popescu University of Sheffield
17:30
60m
Talk
The seL4 verification: the art and craft of proof and the reality of commercial supportRemote
CPP
I: June Andronick Proofcraft, UNSW and seL4 Foundation

Tue 18 Jan

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

09:00 - 10:00
Invited TalkCPP at Salon III
Chair(s): Laura Titolo NIA/NASA LaRC
09:00
60m
Talk
Structural Embeddings RevisitedRemote
CPP
10:20 - 12:00
Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
10:20
25m
Talk
CertiStr: A Certified String SolverDistinguished Paper AwardRemote
CPP
Shuanglong Kan Technische Universität Kaiserslautern, Anthony Widjaja Lin Technische Universität Kaiserslautern and Max-Planck Institute for Software Systems, Philipp Ruemmer Uppsala University, Micha Schrader Technische Universität Kaiserslautern
DOI Pre-print Media Attached
10:45
25m
Talk
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingRemote
CPP
Michael Färber Universität Innsbruck, Austria
DOI Pre-print Media Attached File Attached
11:10
25m
Talk
An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote
CPP
Pre-print Media Attached
11:35
25m
Talk
A Drag-and-Drop Proof TacticRemote
CPP
Benjamin Werner Ecole polytechnique, Pablo Donato Ecole polytechnique, Pierre-Yves Strub Ecole Polytechnique
DOI Pre-print Media Attached
15:30 - 16:10
Chairs' Report and Business MeetingCPP at Salon III
Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania
16:30 - 18:10
Category Theory, HoTT, Number TheoryCPP at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota, Twin Cities
16:30
25m
Talk
Implementing a category-theoretic framework for typed abstract syntaxRemote
CPP
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm University
DOI Pre-print Media Attached
16:55
25m
Talk
(Deep) Induction Rules for GADTsRemote
CPP
Patricia Johann Appalachian State University, Enrico Ghiorzi Italian Institute of Technology
Pre-print Media Attached
17:20
25m
Talk
On homotopy of walks and spherical maps in homotopy type theoryRemote
CPP
Jonathan Prieto-Cubides University of Bergen
Pre-print
17:45
25m
Talk
Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote
CPP
Hing Lun Chan Australian National University
DOI Pre-print Media Attached File Attached

Wed 19 Jan

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

10:20 - 12:00
Separation LogicPOPL at Salon III
Chair(s): James Riely DePaul University
10:20
25m
Talk
A Separation Logic for Heap Space under Garbage CollectionRemote
POPL
10:45
25m
Research paper
Simuliris: A Separation Logic Framework for Verifying Concurrent Program OptimizationsDistinguished PaperRemote
POPL
Lennard Gäher MPI-SWS & Saarland University, Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Ralf Jung MIT, Hoang-Hai Dang MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
11:10
25m
Research paper
Concurrent Incorrectness Separation LogicRemote
POPL
Azalea Raad Imperial College London, Josh Berdine Facebook, Derek Dreyer MPI-SWS, Peter W. O'Hearn Facebook and University College London
11:35
25m
Research paper
On Incorrectness Logic and Kleene Algebra With Top and TestsInPerson
POPL
Cheng Zhang Boston University, Arthur Azevedo de Amorim Boston University, USA, Marco Gaboardi Boston University
13:30 - 14:45
Weak Memory ModelsPOPL at Salon III
Chair(s): Mae Milano University of California, Berkeley
13:30
25m
Research paper
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory ConcurrencyInPerson
POPL
Alan Jeffrey Roblox, James Riely DePaul University, Mark Batty University of Kent, Simon Cooksey University of Kent, Ilya Kaysin JetBrains Research; University of Cambridge, Anton Podkopaev HSE University; JetBrains Research
Pre-print
13:55
25m
Research paper
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-Temporal StoresRemote
POPL
Azalea Raad Imperial College London, Luc Maranget Inria Paris, Viktor Vafeiadis MPI-SWS
14:20
25m
Research paper
Truly Stateless, Optimal Dynamic Partial Order ReductionRemote
POPL
Michalis Kokologiannakis MPI-SWS, Germany, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS, JetBrains Research and St Petersburg University, Viktor Vafeiadis MPI-SWS
15:05 - 16:20
Concurrency and ParallelismPOPL at Salon III
Chair(s): Andrew C. Myers Cornell University
15:05
25m
Research paper
Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote
POPL
Joakim Öhman IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute
15:30
25m
Research paper
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote
POPL
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University, USA, Robbert Krebbers Radboud University Nijmegen
15:55
25m
Research paper
Static Prediction of Parallel Computation GraphsInPerson
POPL
Stefan K. Muller Illinois Institute of Technology
16:40 - 17:30
Reasoning about Probabilistic Programs and AlgorithmsPOPL at Salon III
Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology
16:40
25m
Research paper
A Separation Logic for Negative DependenceRemote
POPL
Jialu Bao Cornell University, Marco Gaboardi Boston University, Justin Hsu University of Wisconsin-Madison, USA, Joseph Tassarotti Boston College
17:05
25m
Research paper
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and RecursionRemote
POPL
Yizhou Zhang University of Waterloo, Nada Amin Harvard University

Thu 20 Jan

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

10:20 - 12:00
Quantum ComputingPOPL at Salon III
Chair(s): Michael Hicks University of Maryland at College Park
10:20
25m
Research paper
Quantum Information EffectsRemote
POPL
Robin Kaarsgaard University of Edinburgh, Chris Heunen University of Edinburgh
10:45
25m
Research paper
Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson
POPL
Charles Yuan Massachusetts Institute of Technology, Christopher McNally MIT, Michael Carbin Massachusetts Institute of Technology
11:10
25m
Research paper
Quantum Separation Logic: A Framework for Local Reasoning of Quantum ProgramsRemote
POPL
Xuan-Bach Le , Jun Sun Singapore Management University, Shang-Wei Lin Nanyang Technological University, Singapore, David Sanan Nanyang Technological University
11:35
25m
Research paper
Semantics for Variational Quantum ProgrammingRemote
POPL
Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius Tulane University, Michael Mislove Tulane, Vladimir Zamdzhiev Inria
13:30 - 14:45
Dynamic AnalysisPOPL at Salon III
Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology
13:30
25m
Research paper
A formal foundation for symbolic evaluation with mergingRemote
POPL
Sorawee Porncharoenwase University of Washington, Luke Nelson University of Washington, Xi Wang University of Washington, Emina Torlak University of Washington
13:55
25m
Research paper
Logarithm and Program TestingInPerson
POPL
Kuen-Bang Hou (Favonia) University of Minnesota, Twin Cities, Zhuyang Wang University of Minnesota
Pre-print
14:20
25m
Research paper
Profile Inference RevisitedRemote
POPL
Wenlei He Facebook, Juli\'{a}n Mestre Facebook, Sergey Pupyrev Facebook, Lei Wang Facebook, Hongtao Yu Facebook
15:05 - 16:20
MetaprogrammingPOPL at Salon III
Chair(s): Stephanie Weirich University of Pennsylvania
15:05
25m
Research paper
Staging with ClassInPerson
POPL
Ningning Xie University of Cambridge, Matthew Pickering University of Bristol, UK, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, UK, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol
Pre-print
15:30
25m
Research paper
Moebius: Metaprogramming using Contextual TypesRemote
POPL
Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University
15:55
25m
Research paper
Type-Level Programming with Match TypesRemote
POPL

Fri 21 Jan

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

10:20 - 12:00
Semantics 1POPL at Salon III
Chair(s): Alan Jeffrey Roblox
10:20
25m
Research paper
From Enhanced Coinduction towards Enhanced InductionRemote
POPL
Davide Sangiorgi University of Bologna
10:45
25m
Research paper
A Fine-Grained Computational Interpretation of Girard's Intuitionistic Proof-NetsInPerson?
POPL
Delia Kesner IRIF, France / University of Paris Diderot, France
11:10
25m
Research paper
Fully abstract models for effectful λ-calculi via category-theoretic logical relationsRemote
POPL
Philip Saville University of Oxford, Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics
11:35
25m
Research paper
Layered and Object-Based Game SemanticsInPerson
POPL
Arthur Oliveira Vale Yale University, Paul-André Melliès CNRS - Université de Paris, France, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS
13:30 - 14:45
Semantics 2POPL at Salon III
Chair(s): Marco Gaboardi Boston University
13:30
25m
Research paper
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming LanguagesInPerson
POPL
Vikraman Choudhury Indiana University & University of Cambridge, Jacek Karwowski University of Warsaw, Amr Sabry Indiana University
Pre-print
13:55
25m
Research paper
A Relational Theory of Effects and CoeffectsRemote
POPL
Ugo Dal Lago University of Bologna, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis
14:20
25m
Research paper
Effectful Program DistancingRemote
POPL
Ugo Dal Lago University of Bologna, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis
15:05 - 16:20
Type TheoryPOPL at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota, Twin Cities
15:05
25m
Research paper
A cost-aware logical frameworkInPerson
POPL
Yue Niu Carnegie Mellon University, Jonathan Sterling Aarhus University, Denmark, Harrison Grodin Carnegie Mellon University, Robert Harper Carnegie Mellon University, USA
Pre-print Media Attached
15:30
25m
Research paper
Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote
POPL
Marcelo Fiore Computer Laboratory, University of Cambridge, Dmitrij Szamozvancev University of Cambridge
15:55
25m
Research paper
Observational Equality: Now For GoodDistinguished PaperRemote
POPL
Loïc Pujet Gallinette Project-Team, Inria, Nicolas Tabareau Inria
16:40 - 17:30
SynthesisPOPL at Salon III
Chair(s): Paul Downen University of Massachusetts Lowell
16:40
25m
Research paper
Learning Formulas in Finite Variable LogicsDistinguished PaperInPerson
POPL
Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
17:05
25m
Research paper
Bottom-up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote
POPL
Anders Miltner The University of Texas at Austin, Texas, USA, Adrian Trejo Nuñez The University of Texas at Austin, Ana Brendel UT Austin, Swarat Chaudhuri Rice University, Isil Dillig University of Texas at Austin

Sat 22 Jan

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

09:00 - 10:00
Session 1WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
09:00
15m
Talk
CN: A Refinement Type System for CRemote
WITS
Christopher Pulte University of Cambridge, UK, Dhruv Makwana University of Cambridge, Kayvan Memarian University of Cambridge, Jean Pichon-Pharabod Aarhus University, Peter Sewell University of Cambridge, Neel Krishnaswami Computer Laboratory, University of Cambridge
09:15
45m
Other
Type-aware equational rewriting (discussion)In-Person
WITS
09:15
45m
Other
Multi case trees: confluence and coverage (discussion)In-Person
WITS
Tesla Zhang The Pennsylvania State University
09:15
45m
Other
Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)Remote
WITS
Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
09:15
45m
Other
The Expression Problem and Theorem Proving (discussion)Remote
WITS
Yao Li University of Pennsylvania, Nick Rioux University of Pennsylvania, Stephanie Weirich University of Pennsylvania
13:30 - 14:45
Session 3WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
13:30
15m
Talk
Tries that matchRemote
WITS
Sebastian Graf Karlsruhe Institute of Technology
13:45
15m
Talk
Gotta prove fast: building an ecosystem for effortless native compilation of tacticsRemote
WITS
Sebastian Ullrich KIT, Germany
14:00
45m
Other
Benchmarking Binding (discussion)
WITS
Stephanie Weirich University of Pennsylvania
14:00
45m
Other
Fancy module systems (discussion)Remote
WITS
Jesper Cockx TU Delft
15:05 - 16:20
Session 4WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
15:05
15m
Talk
Using Dependent Types at Scale: Maintaining the Agda Standard LibraryIn-Person
WITS
Matthew L. Daggitt Heriot-Watt University, Guillaume Allais University of St Andrews
15:20
15m
Talk
Understandable and Useful Error Messages for Liquid TypesIn-Person
WITS
Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa, Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, João David LASIGE, Faculdade de Ciências da Universidade de Lisboa, Guilherme Espada LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa
15:35
15m
Talk
Deciding type equivalence with simple grammarsIn-Person
WITS
Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon
15:50
15m
Talk
Typechecking up to CongruenceIn-Person
WITS
Jad Elkhaleq Ghalayini University of Cambridge
16:05
15m
Talk
À bas l’η — Coq’s troublesome η-conversionRemote
WITS
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes
16:40 - 17:30
Session 5WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
16:40
15m
Talk
mitten: A Flexible Multimodal Proof AssistantRemote
WITS
Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University
16:55
15m
Talk
Setting the Record Straight with SingletonsIn-Person
WITS
Reed Mullanix University of Minnesota
17:10
15m
Talk
First-class pattern synonymsIn-Person
WITS
Tesla Zhang The Pennsylvania State University
Hide past events

Mon 17 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

Room10:003011:003012:003013:003014:003015:003016:0030
Salon III

Fri 21 Jan

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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Salon III

Sat 22 Jan

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Salon III
Hide past events

Sun 16 Jan

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

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

Sat 22 Jan

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Salon III
Hide past events