Announcing the Proof Assistant Yarrow

Announcing the Yarrow Proof Assistant

I announce the availability of the Proof Assistant Yarrow at the URL


Short system description:

Yarrow is a proof-assistant for Pure Type Systems (PTSs). Well known PTSs
are the second order lambda calculus F, the higher order lambda calculus
F_omega, and the calculus of constructions.
In Yarrow you can experiment with various PTSs, representing different logics
and programming languages. A basic knowledge of Pure Type Systems and the
Curry-Howard isomorphism is required. Yarrow is similar to the proof-assistants
Coq and Lego.

The main features of Yarrow are:
* A particular Pure Type System can be chosen at run-time.
* It has the usual tactics for proving propositions.
* There are special rewriting tactics for the Leibniz-equality, and tactics for
  propositional and predicate logic.
* Infix notation and implicit arguments are supported
* 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.

Jan Zwanenburg (janz@win.tue.nl)