Computer Aided Formal Reasoning Group

Homepages of group members

• Matthias Anlauff
• Florian Kammüller
• Martin Simons

Papers

[BRS93]

M. Biersack, R. Raschke, and M. Simons. The DevaWEB System: Introduction, Tutorial, User Manual, and Implementation. Technical Report 93-39, TU Berlin, 1993.
[PostScript source]

[WSL93]

M. Weber, M. Simons, and Ch. Lafontaine. The Generic Development Language Deva: Presentation and Case Studies, volume 738 of LNCS. Springer-Verlag, 1993.

[AJS94]

M. Anlauff, S. Jähnichen, and M. Simons. A support system for formal mathematical reasoning. In M. Naftalin, T. Denvir, and M. Bertran, editors, FME'94: Industrial Benefits of Formal Methods, pages 421--440. Springer-Verlag, 1994.
[Complete PostScript source] [PostScript source without screendumps] [Figure 2] [Figure 3]

[Kam94]

F. Kammüller. Lazy lists as a case study of constructing datatypes. Studienarbeit, TU Berlin, Fachbereich Informatik, 1994.
[PostScript source]

[Kam95]

F. Kammüller. Experimental support of a proof programming language with Isabelle. Diplomarbeit, TU Berlin, Fachbereich Informatik, 1995.
Kel94]

G. Keller. An experimental system for the production and presentation of formal proofs. Studienarbeit, TU Berlin, Fachbereich Informatik, 1994.

[SBR94]

M. Simons, M. Biersack, and R. Raschke. Literate and structured presentation of formal proofs. In E.-R. Olderog, editor, IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET'94), pages 61--81. North Holland, 1994.
[DVI source] [PostScript source]

[Anl95]

M. Anlauff. Rechnerunterstützung formaler Beweissprachen. Number 244 in GMD-Bericht. Oldenbourg Verlag, 1995. to appear.

[HJSW95b]

M. Heisel, S. Jähnichen, M. Simons, and M. Weber. Embedding Mathematical Techniques into System Engineering. In M. Wirsing, editor, ICSE-17 Workshop on Formal Methods Application in Software Engineering Practice, 1995.
[DVI source] [PostScript source]

[SW95]

M. Simons and M. Weber. Case Studies in Literate and Structured Formal Developments. Technical Report 95-6, TU Berlin, 1995.
[PostScript source]

[KKSW95]

F. Kammüller, G. Keller, M. Simons and M. Weber. Structured Presentation of Formal Proofs - Experiments with Isabelle. Isabelle User Workshop 1995.
[PostScript source]

Software

• Devil

Pointers into the World-Wide Web

Institutions

• The Cambridge's Automated Reasoning Group is concerned with the development and application of theorem proving methodologies. The Automated Reasoning Group uses primarily the proof environments HOL and Isabelle.
• A page on mechanized deduction in the German-speaking region carries information on organizations and infrastructure of the German deduction community and links to the major research groups.
• The ESPRIT working group CCL (Construction of Computational Logics) WWW access to publications of the participating sites.
• Frank Pfennig of CMU maintans a bibliography on logical frameworks.
• LICS maintains a www page.
• University of Edinburgh Department of Computer Science features a page on Logic and Proof.
• University of Glasgow, Department of Computing Science
• Imperial College, Theory and Formal Methods Section
• HOL mechanical theorem proving system.
• IMPS is an Interactive Mathematical Proof System intended to provide organizational and computational support for the traditional techniques of mathematical reasoning. In particular, the logic of IMPS allows functions to be partial and terms to be undefined.
• The major goals of NASA Langley's Formal Methods Program are to make formal methods practical for use on life-critical systems developed in the United States, and to orchestrate the transfer of this technology to industry through use of carefully designed demonstration projects.
• Documents related to an ongoing conference on New Mathematical Foundations for Computer Science moderated by Christopher Landauer and Kristie Bellman.
• The Programming Research Group (PRG) at Oxford.
• Dale Miller maintains a page on lambda Prolog.
• SRI International has two intersting research groups: Formal Methods and Dependable Systems and Linear Logic and Proof Theory.
• The Formal Reasoning Group at Stanford's Computer Science Department provides a page on Theorem Provers. There also is Stanford's Theory Division.
• Tübingen's group has this ftp-directory
• Philosophy, Utrecht University

Systems

• Isabelle: the ftp area and bibliography.

People

• Jochen Burghardt has a nice collection of relevant links in the area of automated reasoning.

The World-Wide Web Virtual Library

• Formal Methods

Journals

• Formal Methods in System Design
• Formal Aspects of Computing
• Information and Computation