2 Search Results for "Ni, Wode"

Document
DOI: 10.4230/LIPIcs.ITP.2023.24
An Extensible User Interface for Lean 4

Authors: Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Contemporary proof assistants rely on complex automation and process libraries with millions of lines of code. At these scales, understanding the emergent interactions between components can be a serious challenge. One way of managing complexity, long established in informal practice, is through varying external representations. For instance, algebraic notation facilitates term-based reasoning whereas geometric diagrams invoke spatial intuition. Objects viewed one way become much simpler than when viewed differently. In contrast, modern general-purpose ITP systems usually only support limited, textual representations. Treating this as a problem of human-computer interaction, we aim to demonstrate that presentations - UI elements that store references to the objects they are displaying - are a fruitful way of thinking about ITP interface design. They allow us to make headway on two fronts - introspection of prover internals and support for diagrammatic reasoning. To this end we have built an extensible user interface for the Lean 4 prover with an associated ProofWidgets 4 library of presentation-based UI components. We demonstrate the system with several examples including type information popups, structured traces, contextual suggestions, a display for algebraic reasoning, and visualizations of red-black trees. Our interface is already part of the core Lean distribution.
Cite as

Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nawrocki_et_al:LIPIcs.ITP.2023.24,
  author =	{Nawrocki, Wojciech and Ayers, Edward W. and Ebner, Gabriel},
  title =	{{An Extensible User Interface for Lean 4}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{24:1--24:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.24},
  URN =		{urn:nbn:de:0030-drops-183991},
  doi =		{10.4230/LIPIcs.ITP.2023.24},
  annote =	{Keywords: user interfaces, human-computer interaction, Lean}
}
Document
DOI: 10.4230/OASIcs.PLATEAU.2019.4
Designing Declarative Language Tutorials: A Guided and Individualized Approach

Authors: Anael Kuperwajs Cohen, Wode Ni, and Joshua Sunshine

Published in: OASIcs, Volume 76, 10th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2019)

Abstract
The ability to declare what a program should include rather than how these features should be implemented makes declarative languages very useful in many visual output programs. The wide-ranging uses of these programs, in domains ranging from architecture to web programming to data visualization, encourages us to find an effective method to teach them. Traditional tutorial systems are usually non-interactive and have a gap between the learning and application. This can leave the user frustrated without a way to move forward in the learning process. A general lack of guidance can lead the student down an incorrect path. To prevent these difficulties, we propose a guided tour followed by novel question types that both direct the student’s learning and creates a focused environment to practice individual skills. Lastly, we propose a study to test the hypothesis that this tutorial is quicker to complete and results in a greater understanding of the declarative language.
Cite as

Anael Kuperwajs Cohen, Wode Ni, and Joshua Sunshine. Designing Declarative Language Tutorials: A Guided and Individualized Approach. In 10th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2019). Open Access Series in Informatics (OASIcs), Volume 76, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cohen_et_al:OASIcs.PLATEAU.2019.4,
  author =	{Cohen, Anael Kuperwajs and Ni, Wode and Sunshine, Joshua},
  title =	{{Designing Declarative Language Tutorials: A Guided and Individualized Approach}},
  booktitle =	{10th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2019)},
  pages =	{4:1--4:6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-135-1},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{76},
  editor =	{Chasins, Sarah and Glassman, Elena L. and Sunshine, Joshua},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.PLATEAU.2019.4},
  URN =		{urn:nbn:de:0030-drops-119589},
  doi =		{10.4230/OASIcs.PLATEAU.2019.4},
  annote =	{Keywords: Declarative Programming, Programming Language Tutorial, Visualizations}
}
  • Refine by Author
  • 1 Ayers, Edward W.
  • 1 Cohen, Anael Kuperwajs
  • 1 Ebner, Gabriel
  • 1 Nawrocki, Wojciech
  • 1 Ni, Wode
  • Show More...

  • Refine by Classification
  • 1 Applied computing → Interactive learning environments
  • 1 Human-centered computing → Visualization systems and tools
  • 1 Software and its engineering → Functional languages

  • Refine by Keyword
  • 1 Declarative Programming
  • 1 Lean
  • 1 Programming Language Tutorial
  • 1 Visualizations
  • 1 human-computer interaction
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2020
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact