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:
This program has some disadvantages compared to other proof-assistants:
Yarrow is publicly available. Here follow links to more information.
This program was developed by Jan Zwanenburg. Questions and remarks will be gratefully received and answered.