Pinpointing the Learning Obstacles of an Interactive Theorem Prover
This program is tentative and subject to change.
Interactive theorem provers (ITPs) are programming languages which allow users to reason about and verify their programs. Although they promise strong correctness guarantees and expressive type annotations which can act as code summaries, they tend to have a steep learning curve and poor usability. Unfortunately, there is only a vague understanding of the underlying causes for these problems within the research community. To pinpoint the exact usability bottlenecks of ITPs, we conducted an online survey among 41 computer science bachelor students, asking them to reflect on the experience of learning to use the Agda ITP and to list the obstacles they faced during the process. Qualitative analysis of the responses revealed confusion among the participants about the role of ITPs within software development processes as well as design choices and tool deficiencies which do not provide an adequate level of support to ITP users. To make ITPs more accessible to new users, we recommend that ITP designers look beyond the language itself and also consider its wider contexts of tooling, developer environments, and larger software development processes.
This program is tentative and subject to change.
Sun 27 AprDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | Education, Debugging, Dynamic AnalysisResearch Track / Early Research Achievements (ERA) / Replications and Negative Results (RENE) / Tool Demonstration at 205 | ||
14:00 10mTalk | JavaWiz: A Trace-Based Graphical Debugger for Software Development Education Research Track Markus Weninger JKU Linz, Simon Grünbacher Institute for System Software; Johannes Kepler University Linz, Austria, Herbert Prähofer Johannes Kepler University Linz | ||
14:10 10mTalk | Pinpointing the Learning Obstacles of an Interactive Theorem Prover Research Track Sára Juhošová Delft University of Technology, Andy Zaidman Delft University of Technology, Jesper Cockx Delft University of Technology Pre-print | ||
14:20 10mTalk | AI-based automated grading of source code of introductory programming assignments Research Track Jayant Havare Indian Institute of technology - Bombay, Varsha Apte Indian Institute of technology - Bombay, Kaushikraj Maharajan Indian Institute of technology - Bombay, Nithin Chandra Gupta Samudrala Indian Institute of technology - Bombay, Ganesh Ramakrishnan Indian Institute of technology - Bombay, Srikanth Tamilselvam IBM Research, Sainath Vavilapalli Indian Institute of Technology - Bombay | ||
14:30 10mTalk | An Analysis of Students' Program Comprehension Processes in a Large Code Base Research Track Anshul Shah University of California, San Diego, Thanh Tong University of California, San Diego, Elena Tomson University of California, San Diego, Steven Shi University of California, San Diego, William G. Griswold University of California San Diego, Gerald Soosairaj University of California, San Diego | ||
14:40 6mTalk | OVERLORD: A C++ overloading inspector Tool Demonstration Botond Horváth ELTE Eötvös Loránd University, Budapest, Hungary, Richárd Szalay Eötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers, Zoltán Porkoláb ELTE Eötvös Loránd University, Budapest, Hungary | ||
14:46 6mTalk | Optimizing Code Runtime Performance through Context-Aware Retrieval-Augmented Generation Early Research Achievements (ERA) Manish Acharya Vanderbilt University, Yifan Zhang Vanderbilt University, Kevin Leach Vanderbilt University, Yu Huang Vanderbilt University | ||
14:52 6mTalk | Investigating Execution-Aware Language Models for Code Optimization Replications and Negative Results (RENE) Federico Di Menna University of L'Aquila, Luca Traini University of L'Aquila, Gabriele Bavota Software Institute @ Università della Svizzera Italiana, Vittorio Cortellessa University of L'Aquila Pre-print | ||
14:58 6mTalk | Understanding Data Access in Microservices Applications Using Interactive Treemaps Early Research Achievements (ERA) Maxime ANDRÉ Namur Digital Institute, University of Namur, Marco Raglianti Software Institute - USI, Lugano, Anthony Cleve University of Namur, Michele Lanza Software Institute - USI, Lugano Pre-print | ||
15:04 6mTalk | Divergence-Driven Debugging: Understanding Behavioral Changes Between Two Program Versions Early Research Achievements (ERA) Rémi Dufloer Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France, Imen Sayar Univ. Lille, CNRS, Inria, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France, Anne Etien Université de Lille, CNRS, Inria, Centrale Lille, UMR 9189 –CRIStAL, Steven Costiou INRIA Lille | ||
15:10 10mTalk | KotSuite: Unit Test Generation for Kotlin Programs in Android Applications Research Track Feng Yang Wuhan University, Qi Xin Wuhan University, Zhilei Ren Dalian University of Technology, Jifeng Xuan Wuhan University | ||
15:20 10mLive Q&A | Session's Discussion: "Education, Debugging, Dynamic Analysis" Research Track | ||