Re: [isabelle] Advertise your work on the mailing list
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Advertise your work on the mailing list
- From: Lucas Dixon <ldixon at inf.ed.ac.uk>
- Date: Tue, 09 Nov 2010 00:25:03 +0000
- In-reply-to: <AD3C3C71-141A-4CBF-897B-6B751CB9C6A9@in.tum.de>
- References: <AD3C3C71-141A-4CBF-897B-6B751CB9C6A9@in.tum.de>
- User-agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; en-US; rv:220.127.116.11) Gecko/20101027 Thunderbird/3.1.6
On 25/10/2010 16:55, Jasmin Christian Blanchette wrote:
Now it's your turn!
Some stuff I'm involved with in Edinburgh...
Automated theory exploration:
We have two systems based on Isabelle/IsaPlanner which carry out
automated theory exploration (IsaScheme and IsaCoSy). The idea is to see
how much of in inductive theory can be generated automatically. It turns
out by using counter example finding and generating only irreducible
terms you get some cool stuff:
The IsaCoSy papers to read for this stuff are:
(preprint available at:
and the IsaScheme stuff is described here:
An experiment using Isabelle by a working mathematician:
This has resulted in two things. 1) a formalization of convex analysis,
(I'll let Bogdan say more about this) and 2) an "Isabelle Primer for
Mathematicians" which is a quick introduction to Isabelle, highlighting
some of the common difficulties and how to get around them. :)
The Isabelle primer can be downloaded from:
The formalisation will be released in due course.
Proof Planning/Inductive Theorem Proving in Isabelle:
we've been developing an automated inductive theorem prover
(IsaPlanner). This is based on Rippling, and is primarily a research
tool for exploring extensions to the technique. We've also been
experimenting with proof-plan/tactic languages a bit too, and with
synthesis techniques based on Isabelle's schematic variables (and
machinery to manage working with them). Some info and papers are
Formalisation of Intuitionistic Linear Logic in Isabelle.
We've carried out various formalisations of fragments of
(Intuitionistic) Linear Logic, with proof terms, in Isabelle using the
nominal package, and also experimented with some other forms of handling
binding (Randy Pollack can say more about this perhaps?) We really ought
to tidy the linear logic stuff up and submit it to the AFP... (suddenly
In the pipeline: we're hoping to provide some re-factoring tools for
(Isar) proof scripts... still early days on that.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and