Jape - A Framework for building Interactive Proof Editors

Richard Bornat & Bernard Sufrin

Distributions

• The distribution site is www.jape.org.uk

A Selection of Documents and Papers

Guided Tour

A Guided tour of

Essential Documentation for Jape

• Roll Your Own Jape Logic -- A description of the Jape metalanguage(s) which explains the implementations of several logics.
  
  
• The Unix Jape Companion -- A description of the Unix Jape interface, together with a description of the Unix software which may be used for editing Jape theories, printing proofs and theories, and embedding proofs in Latex documents. This used to be shipped with the machine-independent parts of the old Jape releases.
  
  

September 29th 1997: the documents mentioned immediately below are a little out of date, but may be a useful complement the Unix Jape Companion. They are useable as they stand, but may contain one or two inaccuracies.

• Unix Jape Interface Documentation -- The X Jape Interface at work in a functional programming theory.
  
  
• The Revised Gist of Jape -- The X Jape interface at work in a propositional theory.
  
  

Jape links worth a visit

• Richard Bornat's QMW Jape Site. (Includes MacOS distribution of Jape)
  
  
• ``Jape's Quiet Interface'' The philosophy behind the design of Jape. (July 2nd 1996)
  
  
• ``J'n'J in Jape'' A description of the Jape implementation of the natural deduction logic from Woodcock and Davies's book: Using Z.
  
  
• ``Using J'n'J in Unix/X Jape'' Case studies in using the Jape implementation of the natural deduction logic from Woodcock and Davies's book: Using Z. Includes a short account of the most recent Unix/X Jape interface.
  
  
• ``User Interfaces to Generic Theorem Provers. Part I: Interpreting Gestures'' A description of (and rationale for) some of the key features of Jape's tactic language.
  
  
• ``User Interfaces to Generic Theorem Provers. Part II: Displaying Proofs'' A discussion of (and rationale for) some of the facilities which Jape provides for displaying proofs at an appropriate level of abstraction.
  
  
• ``Animating Operational Semantics with Jape'' Incomplete (Oct 1998) draft of a paper which shows various ways of animating the Structured Operational Semantics (Plotkin) and Natural Semantics (Kahn) of programming languages. There is also a discussion of an environment-based semantics.

  The paper is an account of the material which appears in the theory file named lambda.jt which is distributed with Jape 3.3xd
  
  

Email the Japers