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.

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

### Acknowledgments

Thanks to Erik Poll and Martijn Oostdijk for suggestions concerning these web pages and the example sessions.

### References:

[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.