E.W.Ayers
Chapter 5
A graphical user interface framework for formal verification

In this chapter I present the 'ProofWidgets'In general software parlance, a widget is a graphical component from which to build GUIs. It can also sometimes mean a small piece of interactive user interface that is embedded in another application, for example iPhone widgets. framework for implementing general user interfaces within an interactive theorem prover. The framework uses web technology and functional reactive programming (FRP), as well as the metaprogramming features of advanced interactive theorem proving (ITP) systems such as Lean [EUR+17[EUR+17]Ebner, Gabriel; Ullrich, Sebastian; et al.A metaprogramming framework for formal verification (2017)] to allow for arbitrary interactive graphical user interfaces (GUIs) for representing the goal state of a theorem prover. Users of the framework can create user interfaces declaratively within the ITP's metaprogramming language, without having to develop in multiple languages and without coordinated changes across multiple projects, which improves development time for new designs. The ProofWidgets framework also allows GUIs to make use of the full context of the theorem prover and the specialised libraries that ITP systems offer, such as methods for dealing with expressions and tactics. The framework also includes an extensible structured pretty-printing engine that enables advanced interaction with expressions such as interactive term rewriting.

I have created an implementation of this framework: the ProofWidgets framework for the leanprover-community fork of Lean 3. Throughout the chapter I will use this implementation as an illustration of the principles of the framework. I also provide a practical tutorial to get started with the ProofWidgets framework in Appendix B.

The research contributions of this chapter are:

  • A new and general framework for creating portable, web-based, graphical user interfaces within a theorem prover.

  • A functional APIApplication programming interface. A set of protocols to allow two applications to communicate with each other. for creating widgets within the meta-programming framework of a theorem prover.

  • An implementation of this framework for the Lean theorem prover.

  • A new representation of structured expressions for use with widgets.

  • A description and implementation of a goal-state widget used to interactively show and explore goal states within the Lean theorem prover.

The work in this chapter is my own. A paper based on the content of this chapter has been accepted to ITP 2021. I would like to thank Gabriel Ebner, Brian Gin-ge Chen, and Daniel Fabian for helping with and reviewing the changes to Lean 3 and the VSCode extension needed to make the implementation possible. I would also like to thank Robert Y. Lewis; Markus Himmel; Minchao Wu; Kendall Frey; Patrick Massot; and Angela Li for providing feedback and creating their own lovely widgets (shown in Figure 5.14).

In this chapter I will state the research goals of this system and it fits with the rest of the thesis in Section 5.1. Section 5.3 details the abstract architecture of the framework. Section 5.4 presents a closer look at the mechanism for interactive pretty printing. Section 5.6 provides an overview of some of the practical considerations to do with implementation within a theorem prover, and in particular Lean. Section 5.7 details how ProofWidgets are applied to the task of creating a user interface for HumanProof. Section 5.8 looks at ways in which the system may be extended in the future.

5.1. Research goals

In terms of the broader research questions for the thesis given in Section 1.2, this chapter is mainly concerned with enabling Question 3: presenting human-like reasoning interactively. Specifically, interactively presenting the Box calculus developed in Chapter 3. The application of ProofWidgets to HumanProof is covered in Section 5.7.

See also Section 2.5 for the full background and literature review on the topic of user interfaces for theorem provers.

5.1.1. Motivation

APIs between ITP systems and code editors such as Emacs or VSCode are large and difficult to extend and port. The ProofWidgets protocol addresses this problem by allowing an ITP user to develop new interfaces for users to interact with provers without having to learn specialised knowledge of a particular editor or technology other than basic HTML and CSSHypertext Markup Language and Cascading Style Sheets. These are the languages that control the content and styling of webpages..

Modern ITP systems such as Isabelle, Coq and Lean use advanced language servers and protocols to interface with text editors to produce a feature-rich proving experience. These systems feature standard helpers such as syntax highlighting and type hover information as would be found in normal programming language tooling. They additionally include prover-specific features such as displaying the goal state and providing interactive suggestions of tactics to apply. ITP offers some additional UI challenges above what one might find in developing an editor extension for a standard programming language, because the process of proving is inherently interactive: the user is constantly observing the goal state of the prover and using this information to inform their next command.

The original motivation for ProofWidgets was to create a specific user interface for Box. However, while developing I became frustrated with the development workflow for prototyping the user interface in Lean: each time the interface changed, I would need to coordinate changes across three different codebases; the Lean core, the VSCode editor extension and the repository for Box. It became clear that any approach to creating user interfaces in which the editor code needed to be aware of the datatypes used within the ITP metalogic was doomed to require many coordinated changes across multiple codebases. This inspired my alternative approach; write a full-fledged GUIGraphical User Interface, pronounced 'gooey'. framework in the metalogic of the ITP itself. This approach has the advantage of tightening the development loop and has more general use outside of my particular project (as I will show in Section 5.6.4).

As Bertot and Théry [BT98[BT98]Bertot, Yves; Théry, LaurentA generic approach to building user interfaces for theorem provers (1998)] note, there are two approaches available to create a reusable user interface for a theorem prover:

Focussing on the second approach, the protocol used is typically high level. That is, the protocol is stated in terms of concepts in the prover; for example the SerAPI protocol [Gal16[Gal16]Gallego Arias, Emilio JesúsSerAPI: Machine-Friendly, Data-Centric Serialization for Coq (2016)] used by Coq provides a high level of granularity for extracting goal states and inspecting Coq expressions and proof objects. While such an API enables fine control over the prover through an external tool such as an editor, the API is large and any changes to the API or additional features will require changes in multiple places and potentially introduce incompatibilities.

I argue here that having a wide protocol such as this is detrimental to the agility of prover development. In contrast, the ProofWidgets framework provides a prover ↔ editor protocol that removes the need for an editor to be aware of the internal representations of the prover. This protocol works by reworking the client ↔ server API to instead support the rendering of arbitrary interactive user interfaces. In the ProofWidgets protocol, the code responsible for the layout and event handling of these interfaces is moved to the core ITP, instead of being the responsibility of the editor. This has the effect of creating a full, general purpose GUI framework within a theorem prover.

As a concrete example to motivate this design choice: in the development of the Lean VSCode extension, it was requested that it should be possible to filter some of the variables in the goal state to declutter the output window (see Figure 5.1). The Lean community originally achieved this by reparsing the textual goal state emitted by the Lean server component and removing the filtered items using regular expressions. This worked, but it required adding some specific code for the VSCode client -- supporting this feature in other editors would require rewriting this filtering code. Additionally, if the Lean server changes how the goal state is formatted, this filtering code would need to be rewritten. Even if an API which allows more semantic access to the expression structure is used such as SerAPI [Gal16[Gal16]Gallego Arias, Emilio JesúsSerAPI: Machine-Friendly, Data-Centric Serialization for Coq (2016)], we still have the problem that the filtering code has to be written multiple times for each supported editor. Using ProofWidgets, this filtering code can be written once in Lean itself and it works in any editor that supports the ProofWidgets API (at the time of writing VSCode and a prototype version of the web editor). Furthermore, Lean users are free to make any custom tweaks to the UI without needing to make any changes to editor code.

Figure 5.1.

Demonstration of hypothesis filtering in Lean. Selecting the items from the dropdown menu with show or hide the hypotheses of the goal state according to their type. The original version of this feature was implemented in JavaScript as part of the VSCode Lean. Now the same thing is implemented within Lean as a ProofWidget

Another motivation for ProofWidgets was to add 'structural pretty printing' or 'proof by pointing' as Théry and Bertot call it [BT98[BT98]Bertot, Yves; Théry, LaurentA generic approach to building user interfaces for theorem provers (1998)]. This is where pretty-printed strings have information attached to them that provides detail on the structure of the original expression that produced the string. In other frameworks that implement this such as KeY [ABB+16[ABB+16]Ahrendt, Wolfgang; Beckert, Bernhard; et al.Deductive Software Verification - The KeY Book (2016)] and later versions of Proof General [Asp00[Asp00]Aspinall, DavidProof General: A generic tool for proof development (2000)], this requires a tight integration between the code editor used by the ITP and the pretty-printing system. As is shown in Section 5.4, design of ProofWidgets means that all of the code for creating and interacting with these complex structures can be handled within the ITP system's metalogic.

The three enabling technologies of the widgets framework are

5.1.2. Design goals

The ProofWidgets framework has the following design goals:

  • Programmers write GUIs using the metaprogramming framework of the ITP.

  • Programmers are given an API that can produce arbitrary DOM fragments, including inline CSS styles.

  • No cross-compilation to JavaScript or WebAssembly: the GUI-generating code must run in the same environment as the tactic system. This ensures that the user interaction handlers have full access to the tactic execution context, including the full database of definitions and lemmas, as well as all of the metaprogramming library. In a cross-compilation based approach (implementation difficulty notwithstanding), the UI programmer would have to choose which parts of this context to export to the client.

  • To support interactively discoverable tactics, the system needs to be able to command the client text editor to modify its sourcetext. I'll expand on this point in Section 5.1.3.

  • The pretty printer must be extended to allow for 'interactive expressions': expressions whose tree structure may be explored interactively. I'll expand on this point in Section 5.1.4.

  • Programmers should be able to create visualisations of their data.

  • It should be convenient for programmers to be able to style their GUIs in a consistent manner.

  • The GUI programming model should include some way of managing local UI state, for example, whether or not a tooltip is open.

  • The GUI should be presented in the same output panel that the plaintext goal state was presented in.

  • The framework should be backwards compatible with the plaintext goal state system. Users should be able to opt out of the GUI if they do not like it or want to use a non web-app editor such as Emacs.

While all of these could be implemented by suitably extending the Lean server and client, but as discussed in Section 5.1.1 this would cause the size of the API to balloon significantly. These features require the context of Lean's goal state and tactics engine and all of the information needed to produce a UI would need to be propagated from the server to the client through a JSONJavaScript Object Notation. A text format for representing structured data. intermediary. The server/client API would become wide. Any new idea for improving the interface would require inventing a new part of the server/client API and an implementation spanning many different languages: Lean, C++, JavaScript, and possibly other dependants such as the web-editor and the Python API. Further, the implementation would have to occur in the Lean 3 core codebase, not an external library.

Instead, the goal of the widgets system is to sidestep this by giving the ITP system's metaprogramming framework full control over the UI of the goal state. By choosing this lower level of abstraction, the time required to create new and experimental interactive features is drastically reduced, because widgets can be developed in real time by just editing the code in a single code file within the prover's project. This has already proved useful several times in the Lean implementation of this protocol, for example, a go-to-definition button for expressions in the type information viewer was added by just changing a few lines of code in the mathlib codebase.

5.1.3. Discoverable tactics

Often a beginner to ITP will be confronted with a goal state where they don't know which tactic could be used to progress, at which point they may bug their nearest supervisor. A key tenet of making a user interface intuitive to use is to make available actions discoverable (also called learnability within the HCI literature [GFA09[GFA09]Grossman, Tovi; Fitzmaurice, George; et al.A survey of software learnability: metrics, methodologies and guidelines (2009)]). As shown in Figure 5.2 widgets allow one to make a goal state which actively suggests available tactics to the user.

Figure 5.2.

Example of a suggested tactic widget for a goal. Clicking the apply H button will insert apply H into the proof document and advance the tactic state. TODO: too cryptic, show a wider screenshot.

5.1.4. Interactive term rewriting

Currently in Lean, if one wants to solve an equality problem such as (x + 3) * (x + 1) = x * x + 4 * x + 3 without resorting to a specialised tactic such as ring or a full-blown solver, you have the option of using a general equational rewriting tactic rewrite or simp. The tactic rewrite h where h : Π ..𝑥𝑠, 𝑙𝑕𝑠 = 𝑟𝑕𝑠 will find a subterm of the goal which the 𝑙𝑕𝑠Left Hand Side of h matches with and replaces it with the 𝑟𝑕𝑠 with appropriate substitutions of the variables 𝑥𝑠. Similarly, simp repeatedly performs rewrites of the goal from a curated set of lemmas.

These tactics do not give an easy way to explore subterms of an expression to interactively find where to apply rewrites. With widgets, one can build a tool where one can click directly on a subterm of a goal state and see the available rewrites at that point, or to see what an expression will look like after applying simp. An example of this is shown in Figure 5.3.

Figure 5.3.

A widget goal view with subterm-sensitive suggestions of rewriting lemmas. Clicking on the subterm (x * y)⁻¹ suggests the rewrite rule shown in purple.

Since the widgets system is also able to influence the code editor, it is also possible to build user interfaces that interactively build the proof script in the Lean document.

5.1.5. Non-goals

In order to scope the design of the system, I specify some features that are not a requirement for the design of widgets.

No animation and time-continuous interactions: I don't address the task of creating a framework that is capable of complex reactive animation or continuous, mouse and touch driven interactions like pinching and dragging. Although many existing FRPFunctional Reactive Programming, see Section 5.2.2 for more details. frameworks are built for these, it seems unlikely that Lean 3's VMVirtual Machine. Lean 3 compiles to bytecode which is run in its VM. is going to be performant enough to support them. This does not mean that no animations are possible in widgets, however. Complex animations are possible through CSS transitions without needing to involve a programmatic event at all.

No concurrency and asynchronous tasks: By this I mean the ability for the Lean server to 'push' events to the client after some long-running task has completed. In Section 5.8 I offer some thoughts on how this could be implemented.

No compilation to javascript: This may become possible in Lean 4 with the help of Lean 4's compiler and WebAssembly, but for now the UI logic of widgets should run entirely on the (local) Lean server. This has a number of advantages: it is much less complex than a cross-compilation approach and it allows for the entirety of Lean's proof state and prover apparatus to be available.

Don't support all user interface modalities: Modern browser user interfaces offer many different methods of interaction; drag and drop, touch gestures such as pinch to zoom. For now, the widgets framework only offers a small subset of these, namely mouse events and text input. However HTML ARIA attributes are supported by widgets so that they can be made accessible to differently-abled people.

Performance should be 'good enough': Typically the performance bottleneck for web apps is the layout and painting stages of the browser rendering pipeline (see this chromium documentation entry for more details). Using a client-side framework such as ReactJS to minimise the number of changes to the browser's DOMDocument Object Model. An abstract tree of HTML that, along with CSS, dictates how a webpage should be rendered. This is described further in Section 5.2.1. gives acceptable performance for most use cases. In Section 5.8 I also provide some ideas on how to improve the performance of widgets.

5.2. Background

5.2.1. Anatomy of a web-app

Web-apps are ubiquitous in modern software. By a web-app, we mean any software that uses modern browser technology to implement a graphical application. Web-apps are attractive targets for development because they are platform independent and can be delivered from a server on the internet using a browser or be packaged as an entirely local app using a packaging framework such as electron. Many modern desktop and mobile applications such as VSCode are thinly veiled browser windows.

The structure of a web-page is dictated by a tree structure called the Document Object Model (DOM), which is an abstract representation of the tree structure of an XML or HTML document with support for event handling as might occur as a result of user interaction.

A fragment is a valid subtree structure that is not the entire document (Figure 5.4). So for example an 'HTML fragment' is used to denote a snippet of HTML that could be embedded within an HTML document.

With the help of a CSS style sheet, the web browser paints this DOM to the screen in a way that can be viewed and interacted with by a user (see Figure 5.5). Through the use of JavaScript and event handlers, a webpage may manipulate its own DOM in response to events to produce interactive web-applications. The performance bottleneck in web-apps is usually the layout and painting stages of the browser rendering pipeline; the process by which the abstract DOM is converted to pixels on a screen.See this chromium documentation entry for more information on critical paths in browser rendering. https://www.chromium.org/developers/the-rendering-critical-path

Modern browsers support W3C standards for many advanced features: video playback, support for touch and ink input methods, drag and drop, animation, 3D rendering and many more. HTML also has a set of widely supported accessibility features called ARIA which can be used to ensure that apps are accessible to all. The power of web-apps to create portable, fully interactive user interfaces has clear applications for ITP and indeed many have already been created (see Section 2.5 for a review).

Figure 5.4.

Anatomy of an HTML fragment.

Figure 5.5.

Interaction loop for a typical web-app. A DOM tree is painted using a CSS file to produce a viewable webpage. User interaction invokes event handlers which manipulate the DOM, causing a repaint.

The widgets framework places an ITP system within this interaction loop by providing a metaprogramming interface to create DOM fragments and to update the DOM in response to user interaction. Here, a fragment is any potential subtree of a full document. These fragments are then sent to the client editor which mounts this fragment within an embedded web-browser for viewing. If the user interacts with the resulting view, these interactions are sent back to the server and used to compute a new DOM fragment and update the interface.

5.2.2. Functional GUI frameworks

Most meta-level programming languages for ITPs are functional programming languagesML and Scala for Isabelle, OCaml for Coq, Lean for Lean.. However GUIs are inherently mutable objects that need to react to user interaction. Fortunately, there is a long tradition of user interface frameworks for pure-functional programming. Reactive programming [BCC+13[BCC+13]Bainomugisha, Engineer; Carreton, Andoni Lombide; et al.A survey on reactive programming (2013)]The term 'reactive programming' generally refers to a kind of declarative programming where variable assignments are automatically updated when the variables it depends on update. The classic example is an Excel spreadsheet, where value changes in cells propagate to dependent cells. enables the control of the inherently mutating GUI within a pure functional programming interface. The ideas of reactive programming have achieved a wide level of adoption in web-app development thanks to the popularity of tools such as the React JavaScript library and the Elm programming language [CC13[CC13]Czaplicki, Evan; Chong, StephenAsynchronous functional reactive programming for GUIs (2013)].

Elm and React are UI frameworks for creating web-apps. The programming model used by these reactive frameworks is to model a user interface as a pure view function from a data source (e.g., a shopping list is rendered to an <li> HTML fragment) to a representation of the DOM called the Virtual DOM (VDOM). The VDOM is a shadow tree isomorphic to the DOM.

To modify the UI's data in response to user interactions, an update function for converting user input events to a new version of the data (adding an item to the shopping list). Once the update function is applied and the data has been updated, the system reevaluates the view function on the new data to create a new VDOM. The browser's real DOM is then mutated to match this updated VDOM tree. This may sound inefficient - recomputing the entire VDOM tree each time - but there is an optimisation available: if the view function contains nested view functions, one can memoise these functions and avoid updating the parts of the VDOM that have not changed.

The VDOM is used because directly updating the browser's DOM is costly: as mentioned in Section 5.2.1, a bottleneck in performance for websites can be the repainting phase. When the data updates, the view function creates a new VDOM tree. This tree is then diffed with the previous VDOM tree to produce a minimal set of changes to the real DOM. General tree diffing is known to be NP-hard [Bil05[Bil05]Bille, PhilipA survey on tree edit distance and related problems (2005)], so a simplified algorithm is used. In React, this diffing algorithm is called reconciliation.

In turn, Elm and React are inspired by ideas from Functional Reactive Programming (FRP). FRP was first invented by Elliot [EH97[EH97]Elliott, Conal; Hudak, PaulFunctional reactive animation (1997)]. FRP is distinguished from general reactive programming by the explicit modelling of time. FRP has found use in UI programming but also more broadly in fields such as robotics and signal processing. A modern example of a FRP framework is netwire.

I have elected to use an API for creating user interfaces that is closer to the features I found that the full-FRP paradigm, where the programmer has to explicitly create programs with time, was too complex for the purposes of making a simple UI framework, and in any case the design requirement that the UI logic take place in the Lean VM but rendered by the client means that the modes of iteration are limited to the point where FRP offers no advantages over simpler paradigms. If not used carefully, full-FRP can also introduce 'time-leaks' which is where a cycle of events trigger each other, causing the program to max out CPU and lock up. As is investigated in Appendix C, ProofWidgets use a weaker algebra than FRP which prevents time-leaks from occurring.

5.2.3. Code editors and client-server protocols

Some modern code editors such as Atom and VSCode are built using web technology. In order to support tooling features such as go-to-definition and hover information, these editors act as the client in a client/server relationship with an independently running a process called a language server. As the user modifies the code in the client editor, the client communicates with the server: notifying it when the document changes and sending requests for specific information based on the user's interactions. In ITP this communication is more elaborate than in a normal programming language, because the process of proving is inherently interactive: the user is constantly observing the goal state of the prover and using this information to inform their next command in the construction of a proof.

The most important thing to note here is that changing the communication protocol between the client and the server is generally hard, because the developer has to update the protocol in both the server and the client. There may even be multiple clients. This makes it difficult to quickly iterate on new user interface designs. A way of solving this protocol problem is to offer a much tighter integration by combining the codebases for the editor and the ITP. This is the approach taken by Isabelle/PIDE/jEdit [Wen12[Wen12]Wenzel, MakariusIsabelle/jEdit-A Prover IDE within the PIDE Framework. (2012)] and has its own trade-offs as discussed further in Section 2.5.

5.3. System description

The design goals discussed in Chapter 1 led me to design ProofWidgets to use a declarative VDOM-based architecture (see Section 5.2.2) similar to that used in the Elm programming language [CC13[CC13]Czaplicki, Evan; Chong, StephenAsynchronous functional reactive programming for GUIs (2013)] and the React JavaScript library as discussed in Section 5.2.2. By using the same programming model, we can leverage the familiarity with commonly used React and Elm. In the following subsections we will detail the design of ProofWidgets, starting with the UI programming model Section 5.3.1 and the client/server protocol Section 5.3.2.

5.3.1. UI programming model

This section is about the API that users of the ITP system can use to implement user interfaces to be returned using the protocol given in Section 5.3.2.

Most meta-level programming languages for ITPs are functional programming languagesML and Scala for Isabelle, OCaml for Coq, Lean for Lean. So the mutable DOM paradigm shown in Section 5.2.1 is going to not be suitable for our purposes. Fortunately, as discussed in Section 5.2.2, there are a number of functional paradigms available for building user interfaces in an immutable way. I summarise their operation here and a more detailed overview of the API is given in Appendix C. The design of the UI building API is inspired by the design used in the Elm programming language [CC13[CC13]Czaplicki, Evan; Chong, StephenAsynchronous functional reactive programming for GUIs (2013)].

New user interfaces are created using the Html and Component types. A user may define an HTML fragment by constructing a member of the inductive datatype Html, which is either an element (e.g., <div></div>), a string or a Component object to be discussed shortly.

These fragments can have event handlers attached to them. For example, in (5.6), a button is created by defining a handler : Unitα sending the unit type to a member of some type α. When this interface is rendered in the client and the button is clicked, the server is notified and causes the node to emit the element () : α. In (5.6), when the button is pressed it will emit 4 : . The value of () is then propagated towards the root of the Html tree until it reaches a component.

(5.6).

Simple example of an event handler. The function button takes an event handler and some text for the button content. The value the handler returns will be emitted in the event of a button click.

button : ( : Unitα)StringHtml α
exampleButton : Html := button (()4) "click me"

Now we need to provide a mechanism for doing something with this emitted object. A component is an inductive datatype taking two type parameters: π (the props type) and α (the action type)This is designed to be familiar to those who use React components: https://reactjs.org/docs/components-and-props.html.. It represents a stateful object in the user interface tree where the state s : σ can change as a result of a user interaction event. By 'stateful' we mean an object which holds some mutating state for the lifetime of the user interface. Through the use of components, it is possible to describe the behaviour of this state without having to leave the immutable world of a pure functional programming language. Three functions determine the behaviour of a component:

  • init : πσ initialises the state.

  • view : πσHtml α maps the state to a VDOM tree.

  • update : πασσ × Option β is run when a user event is triggered in the child HTML tree returned by view. The emitted value 𝑎 : α is used to produce a tuple σ × Option β consisting of a new state 𝑠 : σ and optionally, a new event 𝑏 : β to emit. If the new event is provided, it will propagate further towards the root of the VDOM tree and be handled by the next component in the sequence.

A simple example of a counter component is shown in (5.7) and Figure 5.8. In (5.7), the component has an integer s : for a state, and updating the state is done through clicking on the 'increment' and 'decrement' buttons which will emit 1 and -1 when clicked. The values a are used to update the state to a + s. Creating stateful components in this way has a variety of practical uses when building user interfaces for inspecting and manipulating the goal state. We will see in Section 5.4 that a state is used to represent which expression the user has clicked. Indeed, an entire tactic state can be stored as the state of the component. Then the update function runs various tactics to update the tactic state and output the new result.

(5.7).

Code for a simple counter app showcasing statefulness. The output is shown in Figure 5.8

σ :=
, s:= 0
, view := s
<div>
button (()1) "increment"
<span>{to_string s}</span>
button (()-1) "decrement"
</div>
, update := (a : )(s : )a + s
Figure 5.8.

The resulting view of a simple counter component.

0

5.3.2. The server protocol

The communication protocol between the client editor and the ITP server is illustrated in Figure 5.9. A more detailed overview on the specifics for the Lean implementation can be found in the leanprover-community documentation.

Figure 5.9.

The architecture of the ProofWidgets client/server communication protocol. My contribution is present in the section marked 'ProofWidgets protocol'. Arrows that span the dividing lines between the client and server components are API requests and responses. The arrows crossing the boundary between the client and server applications are sent in the form of JSON messages. Rightward arrows are requests and leftward arrows are responses.

Once the programmer has built an interface using the API introduced in Section 5.3.1, it needs to be rendered and delivered to the browser output window. ProofWidgets extends the architecture discussed in Section 5.2.3 with an additional protocol for controlling the life-cycle of a user interface rendered in the client editor. When a sourcefile for the prover is opened (in Figure 5.9, myfile.lean), the server begins parsing, elaborating and verifying this sourcefile as usual. The server incrementally annotates the sourcetext as it is processed and these annotations are stored in memory. The annotations include tracing diagnostics messages as well as thunksA thunk is a lazily evaluated expression. of the goal states at various points in a proof. When the user clicks on a particular piece of sourcecode in the editor ('text cursor move' in Figure 5.9), the client makes an info request for this position to the server, which responds with an ok response containing the logs at that point.

The ProofWidgets protocol extends the info messages to allow the prover to similarly annotate various points in the document with VDOM trees (Section 5.2.2) created from components. These annotating components (see Section 5.3.1) have the type Component TacticState Empty where TacticState is the current state of the prover and Empty is the uninhabited type. A default component for rendering goals of proof scripts is provided, but users may override this with their own components. The VDOM trees are derived from this component, where the VDOM has the same tree structure as the Html datatype (i.e., a tree of elements, strings and components), but the components in the VDOM tree also contain the current state and the current child subtree of the component. This serves the purpose of storing a model of the current state of the user interface. These VDOMs can be rendered to HTML fragments that are sent to the client editor and presented in the editor's output window.

There are two ways to create a VDOM tree from a component: from scratch using initialisation or by updating an existing VDOM tree using reconciliation.

Initialisation is used to create a fresh VDOM tree. To initialise a component, the system first calls init to produce a new state 𝑠. 𝑠 is fed to the view method to create an Html tree 𝑡. Any child components in 𝑡 are recursively initialised.

The inputs to reconciliation are an existing VDOM tree 𝑣 and a new Html tree 𝑡. 𝑡 is created when the view function is called on a parent component. The goal of reconciliation is to create a new VDOM tree matching the structure of 𝑡, but with the component states from 𝑣 transferred over. The tree diffing algorithm that determines whether a state should be transferred is similar to the React reconciliation algorithm and so we will omit a discussion of the details here. The main point is that when a user interface changes, the states of the components are preserved to give the illusion of a mutating user interface.

For interaction, the HTML fragment returned from the server may also contain event handlers. Rather than being calls to JavaScript methods as in a normal web-app, the client editor intercepts these events and forwards them to the server using a widget_event request. The server then updates the component according to the event to produce a new Html tree that is reconciled with the current VDOM tree. The ProofWidgets framework then responds with the new HTML fragment derived from the new VDOM tree. In order to ensure that the correct event handler is fired, the client receives a unique identifier for each handler that is present on the VDOM and returns this identifier upon receiving a user interaction. So, in effect, the ITP server performs the role of an event handler: processing a user interaction and then updating the view rendered to the screen accordingly. In addition to updating the view, the response to a widget_event request may also contain effects. These are commands to the editor, for example revealing a certain position in the file or inserting text at the cursor position. Effects are used to implement features such as go-to definition and modifying the contents of sourcefiles in light of a suggested modification to advance the proof state. If a second user interaction event occurs while the first is being handled, the server will queue these events.

The architecture design presented above is a different approach to how existing tools handle the user interface. It offers a much smaller programming API consisting of Component and Html and a client/server protocol that supports the operation of arbitrary user interfaces controlled by the ITP server. Existing tools (Section 2.5) instead give fixed APIs for interaction with the ITP, or support rendering of custom HTML without or with limited interactivity.

To implement ProofWidgets for an ITP system, it is necessary to implement the three subsystems that have been summarised in this section: a programming API for components; the client editor code (i.e., the VSCode extension) that receives responses from the server and inserts HTML fragments to the editors output window; and the server code to initialise, reconcile and render these components.

5.4. Interactive expressions

This section is about using the widgets system to perform 'interactive pretty printing' where expressions are rendered to HTML with explicit structure information. As discussed in Section 2.5, structural pretty printing is not a novel feature, however the way in which it is designed here makes structural pretty printing extensible and accessible to the metaprogramming framework. The ability to interactively pretty print expressions is a critical part of the implementing the design goal of interactive term rewriting discussed in Section 5.1.4.

An example of the system in operation is given in Figure 5.10: as one hovers over the various expressions and subexpressions in the infoview, one gets semantically correct highlighting for the expressions, and when you click on a subexpression, a tooltip appears containing type information. This tooltip is itself a widget and so can also be interacted with, including opening a nested tooltip.

Figure 5.10.

Screenshot showing the interactive expression view in action within the Lean theorem prover. The left-hand pane is the Lean source document and the right-hand pane is the infoview showing the context and expected type at the editor's cursor. There are two black tooltips giving information about an expression in the infoview.

A number of other features are demonstrated in Figure 5.10:

  • Hovering over subterms highlights the appropriate parts of the pretty printed string.

  • The buttons in the top right of the tooltip activate effects including a "go to definition" button and a "copy type to clipboard" button.

  • Expressions within the tooltip can also be explored in a nested tooltip. This is possible thanks to the state tracking system detailed in the previous section.

Note that the Lean editor already had features for displaying type information for the source document with the help of hover info, however this tooltip mechanism is only textual (not interactive) and only works on expressions that have been written in the source document. Prior to widgets there was no way to inspect expressions as they appeared in the infoview.

All of the code which dictates the appearance and behaviour of the infoview widget is written in Lean and live-reloads when its code is changed. This means that users can produce their own custom tooltips and improve upon the infoview experience without needing to leave the project.

5.4.1. Tagged strings

Before I modified it, the Lean pretty-printer would take an expression and a context for the expression and produce an member of the format type. This is implemented as a symbolic expression (shortened to 'sexpr') a la LISP [McC60[McC60]McCarthy, JohnRecursive functions of symbolic expressions and their computation by machine, Part I (1960)].

I modified Lean's C++ pretty printer so that it would also tag certain sexprs with two pieces of data: the subexpression that produced the substring and an expression address indicating where the subexpression lies in the parent expression. The expression address is a list of expression coordinates used to reference subterms of an expression. An expression coordinate is a number that indexes the recursive arguments in the constructors for an expression. In this sense it is doing the same job as the coordinates defined in Section 2.3.2. That is, parametrising the lenses that are available for subexpressions.

Here is a simplified example in pseudocode.

(5.11).
Expr ::=
| var : StringExpr
| app : ExprExprExpr
| lam : StringExprExpr
| const : StringExpr
Coord ::=
| f | a | lam_body
Address := List Coord
get : AddressExprOption Expr
| []𝑒some 𝑒
| [f, ..𝑡]app 𝑙 𝑟get 𝑡 𝑙
| [a, ..𝑡]app 𝑙 𝑟get 𝑡 𝑟
| [lam_body, ..𝑡]lam 𝑠 𝑏get 𝑡 𝑏
| __none
set : AddressExprExprExpr := ...
coords : ExprList Address := ...
TaggedString ::=
| tag : (Expr × Address)TaggedStringTaggedString
| append : TaggedStringTaggedStringTaggedString
| of_string : StringTaggedString
pretty_print : ExprTactic TaggedString

In this way, the TaggedString acts as a reversed source-map between the resulting sexpr and the original expression. Even when using specialised syntax such as lists [1,2,3] and set comprehensions. This tagged string is used to create widgets that allow users to interactively inspect various parts of the expression in the infoview.

In the case of a subexpression being below a binder (for example in the body of a lambda expression) the pretty printer instantiates the de-Bruijn variable with a dummy local variable, so the given subexpression doesn't contain free de-Bruijn variables and still typechecks without having to know the binders above the subexpression.

Below are some diagrams to illustrate the relationship between a TaggedString and an Expr.

Figure 5.12.

An expression tree for (x ++ y) ++ [1,2]. Each f or a above the lines is an expression coordinate. The red [a,a,f,a] example of an expression address, corresponding to the red line on the tree. Each green circle in the tree will pretty-print to a string independent of the expression tree above it.

Figure 5.13.

The TaggedString tree produced by pretty-printing the expresssion (x ++ y) ++ [1,2]. The green circles are TaggedString.tag constructors and the blue address text within is the relative address of the tag in relation to the tag above it. So that means that the full expression address for a subterm can be recovered by concatenating the Addresses above it in the tree, for example the 2 subexpression is at [] ++ [a] ++ [a,f,a] = [a,a,f,a]

There are two versions of the code for interactive expression rendering: the original core Lean version and the more experimental mathlib version.

To render an interactive expression given a TaggedString, define a stateful Component (TacticState × Expr) Empty. The TacticState object includes the metavariable context and a local context in which the given expression is valid. The state of the component includes an optional Address of the subexpression. When the user hovers over a particular point in the printed TaggedString, the expression address corresponding to that part of the string is calculated using the tags and this address is set as the state of the component. This address is then used to colour in the portion of the string that is currently hovered over by the user's mouse cursor which gives the semantic-aware highlighting effect.

When the user clicks on a subexpression, a tooltip appears containing type information as well as some details on it such as the type and the available explicit arguments. Users can create their own tooltips using attr.popper. The stateful component framework developed in the last section means that these expressions can themselves be interactive expressions and we can recursively expand the selection, as shown in Figure 5.10 earlier.

Using this address information, it is also possible to construct subexpression-aware tactics such as finding rewrites for a particular subterm.

5.5. Related work

In Section 2.5 I covered other graphical user interfaces for proof assistants. Here I will relate them to ProofWidgets. As discussed in Section 5.1.1, the main differentiating feature of ProofWidgets is in its use of web technology for rendering and in allowing the metaprogramming language of the thoerem prover to take full responsibility for constructing the DOM of the GUI and handling user interactions. This contrasts with the two other approaches to constructing GUIs for theorem provers; which I dub the monolithic approach and

The first related architecture is the monolithic approach (see Section 5.1.1) of which the primary example is Isabelle's Prover IDE (PIDE). An advantage of the ProofWidgets approach compared to PIDE's is that the API between the editor and the prover can be smaller since, in ProofWidgets, the appearance and behaviour is entirely dictated by the server. In contrast, the implementation of PIDE is tightly coupled to the bundled jEdit editor, which has some advantages over ProofWidgets in that it gives more control to the developer to create new GUIs. The downside of PIDE's approach here is that one must maintain this editor and so supporting any other editor with feature-parity becomes difficult. ProofWidgets also makes use of modern web technology which is ubiquitously supported. In contrast, PIDE uses a Java GUI library called Swing Creating custom UIs in PIDE requires coding in both Scala and StandardML, and the result does not easily generalise to the VSCode Isabelle extension.

The example of the protocol approach that I will elect to compare ProofWidgets with is the SerAPI protocol for Coq. SerAPI is a library for machine-machine interaction with the Coq theorem prover. SerAPI contrasts to ProofWidgets in that it expects another program to be responsible for displaying graphical elements such as goal states and visualisations; in the ProofWidgets architecture all of the UI appearance and behaviour code is also written in Lean, and the web-app client can render general GUIs emitted by the system.

Theorema [BJK+16[BJK+16]Buchberger, Bruno; Jebelean, Tudor; et al.Theorema 2.0: computer-assisted natural-style mathematics (2016)] is a tool integrated into Wolfram MathematicaMathematica is a proprietary computer algebra system.. Mathematica comes with its own widget system, which can also be used in a web setting, and so by allowing Mathematica do the heavy-lifting, Theorema is able to have fine-grained control over its GUI whilst remaining portable. However, this approach means that it is tied to the proprietary Mathematica ecosystem, wheras ProofWidgets only depends on web standards which are open.

As discussed in Section 2.5, there is a cohort of now extinct theorem provers that had a great deal of focus on graphical, multimodal representations of data; LΩUI for Ωmega [BCF+97[BCF+97]Benzmüller, Christoph; Cheikhrouhou, Lassaad; et al.Omega: Towards a Mathematical Assistant (1997), SHB+99[SHB+99]Siekmann, Jörg; Hess, Stephan; et al.LOUI: Lovely OMEGA user interface (1999)], HyperProof [BE92[BE92]Barwise, Jon; Etchemendy, JohnHyperproof: Logical reasoning with diagrams (1992)] and XBarnacle [LD97[LD97]Lowe, Helen; Duncan, DavidXBarnacle: Making theorem provers more accessible (1997)] for the CLAM prover. I hope that ProofWidgets can enable a rekindling of research into these more inventive and visual representations of proof states.

5.6. Implementation of Widgets in Lean 3

This section explains the underlying model for how widgets are created and mutated as the user interacts with them.

As discussed in Section 5.3.2 Lean has a in server mode in which Lean works with a code editor such as VSCode or Emacs to provide an interactive editing environment. In server mode, Lean monitors open sourcefiles in the open project and maintains a structure called the log tree which attaches information providers to locations in the sourcefiles. For instance, the log tree will hold the goal state of an interactive-mode proof and logging information which will be revealed to the user when they navigate their cursor to that position.

Thanks to Lean's extensive meta-programming features [EUR+17[EUR+17]Ebner, Gabriel; Ullrich, Sebastian; et al.A metaprogramming framework for formal verification (2017)], the Lean programmer can attach their own messages with the tactic.save_info_thunk : thunk formattactic unit function. save_info_thunk will attach a thunk to the log tree containing a procedure to generate a logging message, when the user clicks over that particular part of the document in the client, the Lean server will evaluate the thunk and produce a formatted piece of text to display to the user in the infoview. This process is shown in the dashed part of Figure 5.9.

The widgets framework adds an additional kind of object to the log tree using tactic.save_widget : (tactic_stateempty)tactic unit with take a component as it's argument. As discussed in Section 5.3.1, the log tree entry that is created through save_widget attaches some state to the object which does mutate. In this way, it is possible to model ephemeral UI state such as whether the user has opened a tooltip. The implementation code can be found in the widget.cpp file in the leanprover-community/lean GitHub repository.

5.6.1. Reconcilation of HTML

Informally, the purpose of the reconciliation step is to compare an old tree and a new tree and try to find a way of matching up the new tree to the old tree. This is required to make sure that the internal states of sub-components in the tree are preserved even if the ordering of the components is changed. For example, suppose we had a list of counter subcomponents each with an integer state. Then if we reorder these components in the list we should expect that these counter states are not lost or scrambled. The general version of this problem is a tree-editing problem, which is known to be NP-hard [Bil05[Bil05]Bille, PhilipA survey on tree edit distance and related problems (2005)], however as noted by ReactJS, we can get acceptable performance with heuristics and by allowing the UI created to add an identifying attribute called a key to elements.

In the Lean implementation, if the system is reconciling a list of child attributes, it will reconcile pairs of elements from the old and the new tree that share a key. Behaviour in the unrecommended case of more than a pair having the same key is handled by pairing off the first in the list. Any remaining pairs of elements are reconciled in the order they appear in the list.

5.6.2. CSS

The Lean widgets system per se only emits JSON that is roughly isomorphic to HTML. But for the web-client and viewer implementations it also necessary to include a style sheet to make it look half-decent. Rather than providing a mechanism for including stylesheets, the implementations load a stylesheet library called Tachyons.

Tachyons is a 'functional CSS' library, which means that CSS classes each perform one very precise job. So for example, if you want to render a purple button with rounded corners and padding you would include the attribute className "link pa2 br2 white bg-purple". Tachyons then has some small CSS class selectors (e.g. .pa2 { padding: .5rem; }) that style the DOM element appropriately. These CSS classes have a couple of benefits over inline styles: they are terser and they enforce a set of standardised colours and spacing that make it easier to provide a more consistent appearance. By using this approach to styling one can remove the need for a specially tailored stylesheet, which is perfect for the use case of widgets.

One drawback of rendering expressions in HTML is that the CSS typesetting paradigm is very different to the Wadler-style linebreaking algorithm [Wad03[Wad03]Wadler, PhilipA prettier printer (2003)] that Lean's normal pretty printer uses. Daniel Fabian discovered a CSS trick to automatically linebreak expressions properly if the content box is too narrow.

5.6.3. Supported Effects

There is an additional hook for dealing with side-effects: changes to the client editor document state in response to widget events. Currently the supported effects are: highlighting a portion of the document; inserting text into the document; putting text into the paste buffer; opening a file (to implement go-to-definition).

This is the final piece of the puzzle to produce an interactive proof production experience: allowing widgets to affect the proof script. In the context of the Lean implementation, the framework allows a Lean programmer to embed an interactive GUI at any point in the Lean document. Thanks to Lean's extensive metaprogramming features [EUR+17[EUR+17]Ebner, Gabriel; Ullrich, Sebastian; et al.A metaprogramming framework for formal verification (2017)], the user can write their GUI code in Lean itself. Widgets are already being used in mathlib, the Lean mathematics library [Com20[Com20]The Mathlib CommunityThe Lean Mathematical Library (2020)].

5.6.4. Community-built widgets

The framework has already found use within the wider Lean community. See Figure 5.14 for a quilt of projects that people have made using ProofWidgets. Of particular note is the Mathematica Bridge by Lewis and Wu [Lew17[Lew17]Lewis, Robert Y.An Extensible Ad Hoc Interface between Lean and Mathematica (2017)], which connects Lean to Wolfram Mathematica and uses the ProofWidgets framework to show Lean functions plotted by Mathematica.

Figure 5.14.

Community-made projects using ProofWidgets, in order these are: explode proof viewer by Minchao Wu. Mathematica bridge by Robert Y Lewis and Minchao Wu. Sudoku solver and visualiser by Markus Himmel. Rubik's cube formalisation by Kendall Frey.

5.7. Visualising Boxes

In this section, I am going to discuss how ProofWidgets are used to create an interactive Box element. Boxes were introduced in Chapter 3 and are the development calculus of the HumanProof system. The first component, the visualisation system, follows the same visual rules as defined in (3.10). This is used to create a visualisation of a box.

In order to correctly print bound variables, the visualisation code has a metavariable context as an input, this is updated with new metavariables and local contexts as 𝒤 and 𝒢 Boxes are traversed. This is an example of something that is simple to implement in ProofWidgets because all of the usual theorem proving apparati are available whilst constructing the user interface. In contrast, this would be cumbersome to achieve with the 'wide API' approach discussed in Section 5.1.1.

To implement interactivity, the main component for rendering the Box is stateful, with the state being a Box and an undo stack of Boxes indicating the box-tactics that have been applied so far. Interactivity is implemented by defining a precondition test for each box-tactic. For example, the intro box-tactic (Section 3.5.3) has a precondition of the goal type being a binder. If the precondition holds, the view function renders a button next to the selected goal indicating that a box-tactic is available for application on that goal or hypothesis. The button's event handler (Section 5.3.1) then performs the box-tactic and produces a new Box which is emitted to be picked up by the main component and added to the undo stack. An example of this can be seen in Figure 5.2.

The precondition system is needed because in some cases the box-tactic applications can take a long enough time that a noticeable lag will appear in the systemThe rule of thumb that I use is that any delay of more than half a second without a visual cue after clicking a button is jarring.

The contextual bookkeeping of performing box-tactics on a Box Zipper as worked out in Appendix A is needed to ensure that the box-tactic is sound.

5.8. Future work

In the future, I wish to improve Lean ProofWidgets in a number of ways. One simple way is in improving documentation, Appendix B provides a tutorial on using ProofWidgets in Lean that I hope to expand to more examples later.

In terms of performance, in order to produce responsive interfaces that use long-running tactics (for example: searching a library or running a solver) it will be necessary to provide a mechanism for allowing concurrency. At the moment, if a long-running operation is needed to produce output, this will block the rendering process and the UI will become unresponsive for the length of the operation. Currently Lean has a task type which represents a 'promise' to the result of a long-running operation, which could be utilised to solve this problem. This could be cleanly integrated with ProofWidgets by providing an additional hook with_task:

(5.15).

Adding concurrency to components with the help of with_task.

component.with_task
(get_task : πtask τ)
: (Component ((option τ) × π) α)(Component π α)

Here (5.15), get_task would return a long-running task object and the props for the inner component would transition from none to some 𝑡 upon the completion of the task. Cancelling a task is implemented simply by causing a rerender.

There are also many features of web-browsers that would be worth implementing such as drag-and-drop, sliders and mouse position events. There is also currently no support for adding third party libraries such as the data visualisation library D3. Allowing support for including arbitrary JavaScript libraries to run on the client would allow this, but making such a system portable and robust is more challenging, because they would require JavaScript glue code in order to work correctly with the system. Another aesthetic consideration is finding a principled way of implementing a Wadler-style pretty printer [Wad03[Wad03]Wadler, PhilipA prettier printer (2003)] within CSS and HTML.

Currently, the server sends an entire DOM tree in every event loop, this could be replaced with a JSON patch file to save bandwidth.

I wish to reimplement ProofWidgets in Lean 4. Lean 4 has a bootstrapped compiler, so the reconciling code would can be written in Lean 4 itself without having to modify the core codebase as was necessary for Lean 3. I hope that the pseudocode written in Appendix C will assist in this project. Lean 4 has an overhauled, extensible parser system [UM20[UM20]Ullrich, Sebastian; de Moura, LeonardoBeyond Notations: Hygienic Macro Expansion for Theorem Proving Languages (2020)] which should allow a JSX-like HTML syntax to be used directly within Lean documents.

Bibliography for this chapter

  • [ABB+16]Ahrendt, Wolfgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H.; Ulbrich, MattiasDeductive Software Verification - The KeY Book (2016)publisher Springerdoi 10.1007/978-3-319-49812-6isbn 978-3-319-49811-9view online
  • [Asp00]Aspinall, DavidProof General: A generic tool for proof development (2000)International Conference on Tools and Algorithms for the Construction and Analysis of Systemspages 38--43organization Springerview online
  • [BCC+13]Bainomugisha, Engineer; Carreton, Andoni Lombide; Cutsem, Tom van; Mostinckx, Stijn; Meuter, Wolfgang deA survey on reactive programming (2013)ACM Computing Surveys (CSUR)volume 45number 4pages 1--34publisher ACM New York, NY, USAview online
  • [BCF+97]Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; Fiedler, Armin; Huang, Xiaorong; Kerber, Manfred; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Schaarschmidt, Wolf; Siekmann, Jörg H.; Sorge, VolkerOmega: Towards a Mathematical Assistant (1997)Automated Deduction - CADE-14volume 1249pages 252--255editor McCune, Williampublisher Springerdoi 10.1007/3-540-63104-6_23view online
  • [BE92]Barwise, Jon; Etchemendy, JohnHyperproof: Logical reasoning with diagrams (1992)Working Notes of the AAAI Spring Symposium on Reasoning with Diagrammatic Representationsview online
  • [BJK+16]Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, WolfgangTheorema 2.0: computer-assisted natural-style mathematics (2016)Journal of Formalized Reasoningvolume 9number 1pages 149--185view online
  • [BT98]Bertot, Yves; Théry, LaurentA generic approach to building user interfaces for theorem provers (1998)Journal of Symbolic Computationvolume 25number 2pages 161--194publisher Elsevierview online
  • [Bil05]Bille, PhilipA survey on tree edit distance and related problems (2005)Theoretical computer sciencevolume 337number 1-3pages 217--239publisher Elsevierview online
  • [CC13]Czaplicki, Evan; Chong, StephenAsynchronous functional reactive programming for GUIs (2013)ACM SIGPLAN Conference on Programming Language Design and Implementationpages 411--422editors n.b.publisher ACMdoi 10.1145/2491956.2462161view online
  • [Com20]The Mathlib CommunityThe Lean Mathematical Library (2020)Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofspages 367–381publisher Association for Computing Machinerydoi 10.1145/3372885.3373824isbn 9781450370974view online
  • [EH97]Elliott, Conal; Hudak, PaulFunctional reactive animation (1997)Proceedings of the second ACM SIGPLAN international conference on Functional programmingpages 263--273view online
  • [EUR+17]Ebner, Gabriel; Ullrich, Sebastian; Roesch, Jared; Avigad, Jeremy; de Moura, LeonardoA metaprogramming framework for formal verification (2017)Proceedings of the ACM on Programming Languagesvolume 1number ICFPpages 1--29publisher ACM New York, NY, USAview online
  • [GFA09]Grossman, Tovi; Fitzmaurice, George; Attar, RamtinA survey of software learnability: metrics, methodologies and guidelines (2009)Proceedings of the SIGCHI Conference on Human Factors in Computing Systemspages 649--658view online
  • [Gal16]Gallego Arias, Emilio JesúsSerAPI: Machine-Friendly, Data-Centric Serialization for Coq (2016)institution MINES ParisTechview online
  • [LD97]Lowe, Helen; Duncan, DavidXBarnacle: Making theorem provers more accessible (1997)Automated Deduction—CADE-14pages 404--407publisher Springerview online
  • [Lew17]Lewis, Robert Y.An Extensible Ad Hoc Interface between Lean and Mathematica (2017)Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017volume 262pages 23--37editors n.b.doi 10.4204/EPTCS.262.4view online
  • [McC60]McCarthy, JohnRecursive functions of symbolic expressions and their computation by machine, Part I (1960)Communications of the ACMvolume 3number 4pages 184--195publisher ACM New York, NY, USAview online
  • [SHB+99]Siekmann, Jörg; Hess, Stephan; Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fiedler, Armin; Horacek, Helmut; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Pollet, Martin; Sorge, VolkerLOUI: Lovely OMEGA user interface (1999)Formal Aspects of Computingvolume 11number 3pages 326--342publisher Springerview online
  • [UM20]Ullrich, Sebastian; de Moura, LeonardoBeyond Notations: Hygienic Macro Expansion for Theorem Proving Languages (2020)Automated Reasoningpages 167--182editors n.b.publisher Springer International Publishingview online
  • [Wad03]Wadler, PhilipA prettier printer (2003)The Fun of Programming, Cornerstones of Computingpages 223--243editors n.b.publisher Palgrave MacMillanview online
  • [Wen12]Wenzel, MakariusIsabelle/jEdit-A Prover IDE within the PIDE Framework. (2012)AISC/MKM/Calculemuspages 468--471organization Springerview online
  • [Wen18]Wenzel, MakariusIsabelle/PIDE after 10 years of development (2018)UITP workshop: User Interfaces for Theorem Provers. view online
© 2021 E.W.Ayers. Built with Gatsby