A *proof-assistant* is a computer program with which a user can
construct completely formal mathematical proofs in some kind of logical
system. In contrast to a
*theorem prover*, a proof-assistant cannot find proofs on its own.

Yarrow is a proof-assistant for *Pure Type Systems*
(PTSs) with several extensions.
A PTS is a particular kind of logical system, defined in
[Bar92]. In Yarrow you can experiment with various
pure type systems, representing different logics and programming languages.
A basic knowledge of Pure Type Systems and the Curry-Howard-de Bruijn
isomorphism is required. (This isomorphism says how you can interpret types
as propositions.) Experience with similar
proof-assistants can be useful.

There are three extensions of PTSs implemented in Yarrow.
First, we have definitions. Definitions are
indispensable for any practical use of PTSs.
Pure Type Systems with definitions (DPTs) are defined in
[SP93];
the most important property of these systems is that apart from
*global* definitions definitions in the context, also *local*
definitions within terms are admitted.

Second, we have subtyping. Subtyping makes the type system more flexible.
In particular, it can be used with records to allow formalization of
Object-Oriented Programming to a certain degree.
Pure Type Systems with Subtyping are defined in
[Zwa99].

Third, we have records. Records are useful for defining programs in a PTS,
in particular Object-Oriented programs.

The main features of Yarrow are:

- A particular pure type system (with subtyping) can be chosen at run-time.
- There are general tactics for proving theorems.
- Tactics for forward reasoning.
- Special rewriting tactics for the Leibniz-equality, and tactics for propositional and predicate logic.
- An easy-to-use system for infix notation, implicit arguments and binders.
- It is portable, because it runs on any platform on which Haskell runs. This includes most Unix systems.
- It has a built-in help system.

This program has some disadvantages compared to other proof-assistants:

- No automatic proof-search tactics.
- No inductive types, since they do not belong to PTSs.
- No mouse-control, but some effort has been spent to make the keyboard-interface user-friendly.

Yarrow is publicly available. Here follow links to more information.

- User Guide
- Installation guide
- Release notes
- Example sessions in Yarrow, including a small tutorial.
- Articles about the implementation of Yarrow
- An example by Herman Geuvers (added April 2006) showing the inconsistency of the PTS with rules: * : square (*,*), (square, *), (*,square,*)

This program was developed by Jan Zwanenburg. Questions and remarks will be gratefully received and answered.

- [Bar92]
- Henk Barendregt. Lambda Calculi with Types. In D.M. Gabbai, S. Abramsky,
and T.S.E. Maibaum, editors,
*Handbook of Logic in Computer Science*, volume 1. Oxford University Press, 1992. - [SP93]
- Paula Severi and Erik Poll.
*Pure Type Systems with Definitions*. Computing Science Note 93/24. Eindhoven University of Technology, 1993. - [Zwa99]
- Jan Zwanenburg.
*Object-Oriented Concepts and Proof Rules: Formalization in Type Theory and Implementation in Yarrow*. Ph.D. thesis. Eindhoven University of Technology, 1999.