[Prev][Next][Index][Thread]
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)

DeliveryDate: 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 proofassistant 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
CurryHoward isomorphism is required. Yarrow is similar to the proofassistants
Coq and Lego.
The main features of Yarrow are:
* A particular Pure Type System can be chosen at runtime.
* It has the usual tactics for proving propositions.
* There are special rewriting tactics for the Leibnizequality, 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 builtin help system.
Jan Zwanenburg (janz@win.tue.nl)