Posted on Monday, 9 August 2004
ProB is an animator and model checker for the B-Method. It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for errors. ProB is maintained by Michael Leuschel. It is based on research and implementation effort by Michael Leuschel, Michael Butler, Carla Ferreira, Leonid Mikhailov, Edward Turner, Phil Turner, and Laksono Adhianto. Part of the research and development was conducted within the EPSRC funded projects ABCD and iMoc.
ProB can be dowloaded here.
Posted on Wednesday, 4 August 2004
Three packages for easy typesetting of proof trees are available at LaTeX for Logicians. The link contains a brief comparison of the packages together with the documatation.
Thanks Jan Meier for the link!
Posted on Wednesday, 21 July 2004
Carl Adam Petri will give a one-week course on his work from 27 September to 1 October. These will be 2 hour lectures in the afternoon (to be held in German) at:
University of Hamburg
Department of Informatics
Vogt-Kölln-Str. 30
22527 Hamburg
Further details are available from http://www.informatik.uni-hamburg.de.
Posted on Wednesday, 21 July 2004
The release of version 2.0 of the
Java-based Petri net tool Renew has been announced.
It is available from the homepage http://www.renew.de where you will also find more information about Renew. You can download the ready-to-install archives of the new version 2.0 and the source code at your option.
The main improvement over earlier versions is a plug-in system that increases the tool's flexibility.
Note that starting with version 2.0, at least Java 1.4 is required to run or compile Renew.
Posted on Tuesday, 6 July 2004
A new book on Linear Logic in Computer Science is to be published by Cambridge University Press in September.
From the publisher's announcement:
Linear Logic in Computer Science
Edited by Paul Ruet, Thomas Erhard, Jean-Yves Girard, Phil Scott
Publication is planned for September 2004
400 pages, 75 exercises, 150 figures, 50 worked examples
Paperback, ISBN: 0521608570
Linear Logic is a branch of proof theory which provides refined tools for the study of the computational aspects of proofs. These tools include a duality-based categorical semantics, an intrinsic graphical representation of proofs, the introduction of well-behaved non-commutative logical connectives, and the concepts of polarity and focalisation. These various aspects are illustrated here through introductory tutorials as well as more specialised contributions, with a particular emphasis on applications to computer science: denotational semantics, lambda-calculus, logic programming and concurrency theory. The volume is rounded-off by two invited contributions on new topics rooted in recent developments of linear logic. The book derives from a summer school that was the climax of the EU Training and Mobility of Researchers project Linear Logic in Computer Science. It is an excellent introduction to some of the most active research topics in the area.
Contents
Part I. Tutorials: 1. Category theory for linear logicians R. Blute and Ph. Scott; 2. Proof nets and the x-calculus S. Guerrini; 3. An overview of linear logic programming D. Miller; 4. Linearity and nonlinearity in distributed computation G. Winskel; 5. An axiomatic approach to structural rules for locative linear logic J. M. Andreoli; 6. An introduction to uniformity in ludics C. Faggian, M. R. Fleury-Donnadieu and M. Quatrini; 7. Slicing polarized addictive normalization O. Laurent and L. Toratora De Falco; 8. A topological correctness criterion for muliplicative noncommutative logic P.A. Mellies; 9. Bicategories in algebra and linguistics J. Lambek; 10. Between logic and quantic: a tract J. Y. Girard.
Contributors
J. M. Andreoli, R. Blute, C. Faggian, M. R. Fleury-Donnadieu, J. Y. Girard, S. Guerrini, J. Lambek, O. Laurent, P. A. Mellies, D. Miller, M. Quayrini, Ph. Scott, L. Tortora de Falco, G. Winskel
Posted on Tuesday, 29 June 2004
Added a section on object Petri nets (OPNs) accessible from the main site menu. To start with, it only contains some informal chit-chat on the concepts ... more to be added gradually.
A list of references is given.
Posted on Sunday, 27 June 2004
New Version of the site launched with additional features. Details to be announced soon ... |
|
|
|
- The ProB animator and model checker for the B method.
Version 1.1 available for download.
- LaTeX Packages for Proof Trees
- Forthcoming Lectures of C. A. Petri
- New Version of Renew Released
- Book on Linear Logic
- Section on Object Petri Nets
- Site Relaunch
- Entries 1 - 7
|
