Yarrow Home Page

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.

Acknowledgments

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.

Similar proof-assistants:

• Coq
• Lego
• Typelab