English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

To improve on existing models of interaction with a proof assistant (PA), inparticular for storage and replay of proofs, we in- troduce three relatedconcepts, those of: a proof movie, consisting of frames which record both userinput and the corresponding PA response; a camera, which films a user'sinteractive session with a PA as a movie; and a proviola, which replays a movieframe-by-frame to a third party. In this paper we describe the movie datastructure and we discuss a proto- type implementation of the camera andproviola based on the ProofWeb system. ProofWeb uncouples the interaction witha PA via a web- interface (the client) from the actual PA that resides on theserver. Our camera films a movie by "listening" to the ProofWeb communication.The first reason for developing movies is to uncouple the reviewing of a formalproof from the PA used to develop it: the movie concept enables users todiscuss small code fragments without the need to install the PA or to load awhole library into it. Other advantages include the possibility to develop aseparate com- mentary track to discuss or explain the PA interaction. We assertthat a combined camera+proviola provides a generic layer between a client(user) and a server (PA). Finally we claim that movies are the right type ofdata to be stored in an encyclopedia of formalized mathematics, based on ourexperience in filming the Coq standard library.

Proviola: A Tool for Proof Re-animation