Welcome!
With recent developments of modern theorem provers, the completely formal development of software is gradually becoming feasible. The aim of the AWE project is to increase this feasibility by developing a methodology for the reuse of formal developments under the slogan ``Abstraction for Reuse'': given a formal development we want to make it more abstract to be able to reuse it in many different, similar situations. This way, the effort of formal development can be reused, and hence gets reduced each time.
The project focusses on foundations in formal logic and developing tool support, using Isabelle as the implementation basis and theorem proving engine. The project has been supported by the German research council DFG from 2002 to 2008.
This Web Site
This site has been set up to disseminate the project results, and contains the following:
- more information about the project aims, the results and recent news;
- the software we have developed, including various Isabelle extensions and theories, such as adding notions of theory morphisms and parameterised theories to Isabelle, implementing monads and various well-known transformation rules;
- a bibliography of all the papers published during the project;
- and finally, contact information.
Latest Project News
- Maksym Bortin's PhD thesis, which describes both the underlying concepts
and theory of the AWE extensions and its usage, has been published. You can
order
it here.
26.07.10
- Release 0.9.1 of the AWE Extension Pack is now available for Isabelle
2009-1. Download it here.
19.03.10
- Release 0.9 of the AWE Extension Pack is now available for Isabelle 2009. Download it here.
10.08.08
- Release 0.5 of the AWE Extension Pack is now available for Isabelle 2007 or Isabelle 2005. Download it here.
12.01.08
- A new and improved version of the user and reference
manual is available.
10.08.07
- Moving with the times, the AWE repository has moved to
Subversion.
29.09.06
- Release 0.4 of the AWE Extension Pack for Isabelle available!
Download it here.
26.07.06
- The paper Structured Formal Development in Isabelle
(Bortin, Johnsen, Lüth) has been accepted for the
Nordic Journal of Computing.
14.06.06
- The second phase of the project has been granted funding from the
German Research Council.
11.11.05