Announcing the Proof Assistant Yarrow
Subject: Announcing the Proof Assistant Yarrow
From: email@example.com (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
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 (firstname.lastname@example.org)