POPL 2022 (series) / WITS 2022 (series) / WITS 2022 / Understandable and Useful Error Messages for Liquid Types
Understandable and Useful Error Messages for Liquid TypesRemote
This talk addresses the challenges of providing useful error messages in languages with Liquid Types. Error messages are essential for a productive development process, moreso in advanced type systems, where there is more indirection in the type system.
We draw from our experience developing three programming languages with Liquid Types: Aeon, designed for usable synthesis, LiquidJava, for which we conducted an usability study, and MLVP, a visual programming for machine learning. We share the common and different challenges in designing error messages, and discuss future work. For this, we also build a bridge between the development experience of liquid types and interactive theorem provers, such as Coq or Lean.
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change
15:05 - 16:20 | |||
15:05 15mTalk | mitten: A Flexible Multimodal Proof AssistantRemote WITS Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University | ||
15:20 15mTalk | 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 15mTalk | 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 15mTalk | Typechecking up to CongruenceIn-Person WITS Jad Elkhaleq Ghalayini University of Cambridge | ||
16:05 15mTalk | À bas l’η — Coq’s troublesome η-conversionRemote WITS Meven Lennon-Bertrand Inria – LS2N, Université de Nantes | ||