VenueWestin Philadelphia
Room nameSalon III
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 - 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
Link to publication
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
08:50
10m
Talk
Chairs' report
CPP

File Attached
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
Link to publication
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
Link to publication 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
DOI Pre-print Media Attached
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.
Pre-print
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
Link to publication
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
Media Attached

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 TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, 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
15:30
40m
Talk
Chairs' Report
CPP

File Attached
16:30 - 18:10
Category Theory, HoTT, Number TheoryCPP at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
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 Media Attached
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

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
DOI Media Attached
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, Viktor Vafeiadis MPI-SWS
DOI Media Attached
14:20
25m
Research paper
Truly Stateless, Optimal Dynamic Partial Order ReductionRemote
POPL
Michalis Kokologiannakis MPI-SWS, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS; St. Petersburg University; JetBrains Research, Viktor Vafeiadis MPI-SWS
DOI Media Attached
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; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute
DOI Media Attached
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, Robbert Krebbers Radboud University Nijmegen
DOI Media Attached
15:55
25m
Research paper
Static Prediction of Parallel Computation GraphsInPerson
POPL
Stefan K. Muller Illinois Institute of Technology
DOI Media Attached
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 Cornell University, Joseph Tassarotti Boston College
DOI Media Attached
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
DOI Media Attached

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
Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Edinburgh
DOI Media Attached
10:45
25m
Research paper
Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson
POPL
Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
DOI Media Attached
11:10
25m
Research paper
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation LogicRemote
POPL
Xuan-Bach Le Nanyang Technological University, Shang-Wei Lin Nanyang Technological University, Jun Sun Singapore Management University, David Sanan Nanyang Technological University
DOI Media Attached
11:35
25m
Research paper
Semantics for Variational Quantum ProgrammingRemote
POPL
Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius JKU Linz, Michael Mislove Tulane University, Vladimir Zamdzhiev Inria
DOI Media Attached
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
DOI Media Attached
13:55
25m
Research paper
Logarithm and Program TestingInPerson
POPL
Kuen-Bang Hou (Favonia) University of Minnesota, Zhuyang Wang University of Minnesota
DOI Media Attached
14:20
25m
Research paper
Profile Inference RevisitedRemote
POPL
Wenlei He Facebook, Julián Mestre Facebook; University of Sydney, Sergey Pupyrev , Lei Wang Facebook, Hongtao Yu Facebook
DOI Media Attached
15:05 - 16:20
MetaprogrammingPOPL at Salon III
Chair(s): Stephanie Weirich University of Pennsylvania
15:05
25m
Research paper
Staging with Class: A Specification for Typed Template HaskellInPerson
POPL
Ningning Xie University of Cambridge, Matthew Pickering Well-Typed LLP, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol
DOI Media Attached
15:30
25m
Research paper
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on ItselfRemote
POPL
Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University
DOI Media Attached
15:55
25m
Research paper
Type-Level Programming with Match TypesRemote
POPL
DOI Media Attached

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; Inria
DOI Media Attached
10:45
25m
Research paper
A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-NetsInPerson
POPL
Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France
DOI Media Attached
11:10
25m
Research paper
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical RelationsRemote
POPL
Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics, Philip Saville University of Oxford
DOI Media Attached
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, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS
DOI Media Attached
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
Link to publication DOI Media Attached
13:55
25m
Research paper
A Relational Theory of Effects and CoeffectsRemote
POPL
Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria
DOI Media Attached
14:20
25m
Research paper
Effectful Program DistancingRemote
POPL
Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria
DOI Media Attached
15:05 - 16:20
Type TheoryPOPL at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
15:05
25m
Research paper
A Cost-Aware Logical FrameworkInPerson
POPL
Yue Niu Carnegie Mellon University, Jonathan Sterling Aarhus University, Harrison Grodin Carnegie Mellon University, Robert Harper Carnegie Mellon University
DOI Media Attached
15:30
25m
Research paper
Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote
POPL
Marcelo Fiore University of Cambridge, Dmitrij Szamozvancev University of Cambridge
DOI Media Attached
15:55
25m
Research paper
Observational Equality: Now for GoodDistinguished PaperRemote
POPL
DOI Media Attached
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
DOI Media Attached
17:05
25m
Research paper
Bottom-Up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote
POPL
Anders Miltner University of Texas at Austin, Adrian Trejo Nuñez University of Texas at Austin, Ana Brendel University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Işil Dillig University of Texas at Austin
DOI Media Attached

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 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
File Attached
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 Karlsruhe Institute of Technology
14:00
45m
Other
Benchmarking Binding (discussion)In-Person
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
mitten: A Flexible Multimodal Proof AssistantRemote
WITS
Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University
15:20
15m
Talk
Understandable and Useful Error Messages for Liquid TypesRemote
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
Using Dependent Types at Scale: Maintaining the Agda Standard LibraryIn-Person
WITS
Matthew L. Daggitt Heriot-Watt University, Guillaume Allais University of St Andrews
16:55
15m
Talk
Setting the Record Straight with SingletonsRemote
WITS
Reed Mullanix University of Minnesota
17:10
15m
Talk
First-class pattern synonymsIn-Person
WITS
Tesla Zhang The Pennsylvania State University

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

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