Announcing the Proof Assistant Yarrow

To: types@cs.indiana.edu
Subject: Announcing the Proof Assistant Yarrow
From: janz@win.tue.nl (Jan Zwanenburg)
Date: Tue, 23 Sep 1997 16:55:01 +0200 (MET DST)
Delivery-Date: Tue, 23 Sep 1997 09:55:13 -0500

Announcing the Yarrow Proof Assistant

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

     http://www.win.tue.nl/cs/pa/janz/yarrow/index.html

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)