[isabelle] (no subject) · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] (no subject)

Email Gateway (Aug 17 2022 at 13:27):

From: ajp@inf.ed.ac.uk
CMCS 2006

8th International Workshop on Coalgebraic Methods in Computer Science
http://conferences.inf.ed.ac.uk/cmcs06/cmcs06.html

Vienna, Austria
March 25-27, 2006

The workshop will be held in conjunction with the 9th European Joint
Conferences on Theory and Practice of Software ETAPS 2006
March 25 - April 2, 2006

Aims and Scope

During the last few years, it has become increasingly clear that a
great variety of state-based dynamical systems, like transition
systems, automata, process calculi and class-based systems, can be
captured uniformly as coalgebras. Coalgebra is developing into a
field of its own interest presenting a deep mathematical foundation, a
growing field of applications and interactions with various other
fields such as reactive and interactive system theory, object oriented
and concurrent programming, formal system specification, modal logic,
dynamical systems, control systems, category theory, algebra,
analysis, etc. The aim of the workshop is to bring together
researchers with a common interest in the theory of coalgebras and its
applications.

The topics of the workshop include, but are not limited to:

the theory of coalgebras (including set theoretic and
categorical approaches);
coalgebras as computational and semantical models (for
programming languages, dynamical systems, etc.);
coalgebras in (functional, object-oriented, concurrent) programming;
coalgebras and data types;
(coinductive) definition and proof principles for coalgebras
(with bisimulations or invariants);
coalgebras and algebras;
coalgebraic specification and verification;
coalgebras and (modal) logic;
coalgebra and control theory (notably of discrete event and
hybrid systems).

The workshop will provide an opportunity to present recent and ongoing
work, to meet colleagues, and to discuss new ideas and future trends.

Previous workshops of the same series have been organized in Lisbon,
Amsterdam, Berlin, Genova, Grenoble, Warsaw and Barcelona. The
proceedings appeared as Electronic Notes in Theoretical Computer
Science (ENTCS) Volumes 11,19, 33, 41, 65.1, 82.1 and 106. You can get
an idea of the types of papers presented at the meeting by looking at
the tables of contents of the ENTCS volumes from those workshops ENTCS

Location

CMCS 2006 will be held in Vienna on March 25-27, 2006. It will be a
satellite workshop of ETAPS 2006, the European Joint Conferences on
Theory and Practice of Software.

Programme Committee

John Power (chair,Edinburgh), Luis Barbosa (Minho), Neil Ghani
(Nottingham), H. Peter Gumm (Marburg), Marina Lenisa (Udine), Stefan
Milius (Braunschweig), Larry Moss (Bloomington), Jan Rutten
(Amsterdam), Hendrik Tews (Dresden), Tarmo Uustalu (Tallinn), Hiroshi
Watanabe (Osaka).

Keynote Speaker: Peter O'Hearn (Queen Mary, University of London)

Invited Speakers: Corina Cirstea (University of Southampton)
Alexander Kurz (University of Leicester)

Submissions

Two sorts of submissions will be possible this year:

Papers to be evaluated by the programme committee for inclusion in the
ENTCS proceedings:

These papers must be written using ENTCS style files and be of length
no greater than 20 pages. They must contain original contributions, be
clearly written, and include appropriate reference to and comparison
with related work. If a submission describes software, software tools,
or their use, it should include all source code that is needed to
reproduce the results but is not publicly available. If the additional
material exceeds 5 MB, URL's of publicly available sites should be
provided in the paper.

Short contributions:

These will not be published but will be compiled into a technical
report of the University of Nottingham. They should be no more than
two pages and may describe work in progress, summarise work submitted
to a conference or workshop elsewhere, or in some other way appeal to
the CMCS audience.

Both sorts of submission should be submitted in postscript or pdf form
as attachments to an email to cmcs06@cs.nott.ac.uk. The email should
include the title, corresponding author, and, for the first kind of
submission, a text-only one-page abstract.

After the workshop, we expect to produce a journal proceedings of
extended versions of selected papers to appear in Theoretical Computer
Science.

Important Dates

Deadline for submission of regular papers: January 8, 2006.
Notification of acceptance of regular papers: February 6, 2006.
Final version for the preliminary proceedings: February 13, 2006.

Deadline for submission of short contributions: February 28, 2006.
Notification of acceptance of short contributions: March 6, 2006.

For more information, please write to cmcs06@cs.nott.ac.uk.

Email Gateway (Aug 17 2022 at 14:14):

From: John Matthews <matthews@galois.com>
Hi all,

Matt Kaufmann and I are interested in how Isabelle's simplifier
handles the case where there are multiple congruence rules that match
a particular subterm. Does it try all the rules in some order, or
does it just pick one?

Thanks,
-john

Email Gateway (Aug 17 2022 at 14:14):

From: Stefan Berghofer <berghofe@in.tum.de>
John Matthews wrote:
The simplifier currently only allows one congruence rule per constant.
See section 10.2.6 of the Isabelle reference manual for more information.

Greetings,
Stefan

Email Gateway (Aug 18 2022 at 09:57):

From: Priya Gopalan <priya.g@ed.ac.uk>
Hello,

I am compiling Isabelle using a flavour of ML called alice.
While loading the ROOT.ML file (src/Pure/ROOT.ML) at the alice ML shell-level,
it interprets most of it fine, and gets stuck at the point when the
following is invoked:

=========
use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;

use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
=========

Here are the details:

On giving the shell
=============
use_thy "Pure";
=============

it gives

=============
Uncaught exception
ERROR
=============

with this message:
=============
Loading theory "Pure"
*** Uninitialized theory data "Isar/attributes"
*** At command "lemma" (line 18 of
"~/Priya/Work/IsabelleTest/Isabelle2005/src/Pure/Pure.thy")
=============

I will be grateful for any info on the possible reasons for a message
like this and how it can be fixed.

Thanks,

Priya

Email Gateway (Aug 18 2022 at 09:57):

From: Makarius <makarius@sketis.net>
On Mon, 27 Nov 2006, Priya Gopalan wrote:

I am compiling Isabelle using a flavour of ML called alice. While
loading the ROOT.ML file (src/Pure/ROOT.ML) at the alice ML shell-level,
it interprets most of it fine, and gets stuck at the point when the
following is invoked:

use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;

Building Isabelle requires an incremental compiler, where new code can be
processed at runtime. Both sml/nj and Poly/ML support this, but many more
recent ML implementations don't -- I am unsure about Alice ML.

Basically Pure is a plain static compile until the very end, where
theories "Pure" and "CPure" are loaded. You should still be able to get
past this point, but the real trouble will start when object-logics are
bootstrapped. (It might be better to try FOL first before attempting
HOL.)

Loading theory "Pure"
*** Uninitialized theory data "Isar/attributes"
*** At command "lemma" (line 18 of
"~/Priya/Work/IsabelleTest/Isabelle2005/src/Pure/Pure.thy")

I wonder how you even got that far. Did you change anything in the Pure
sources (and startup scripts)?

Makarius

Email Gateway (Aug 18 2022 at 10:41):

From: RF Todd <s0456778@sms.ed.ac.uk>
Hi,

I have got Fedora recently installed and am trying to install Isabelle
on it. I have downloaded Isabelle and Proof General in the compressed
zip file onto my desktop. I then tried typing in the commands given
under the 'Install' file into the terminal, but it does not seem to
work.

I wonder if i should download anything else or could you give me advice
on what i am doing wrong.

Rachel

Email Gateway (Aug 18 2022 at 12:19):

From: Jan-Georg Smaus <smaus@informatik.uni-freiburg.de>
Hello,

I would like to point out that in the Isabelle 2008 library, in

http://isabelle.in.tum.de/library/HOL/Transitive_Closure.html it says that

"uses ($ISABELLE_HOME/src/Provers/trancl.ML)"

but in fact, this is a dead link.

Best regards,
Jan Smaus

Email Gateway (Aug 18 2022 at 12:20):

From: Makarius <makarius@sketis.net>
Thanks. We have noticed already that all ML links are broken, and fixed
it recently, i.e. it will work again in the next release.

Makarius

Email Gateway (Aug 19 2022 at 13:02):

From: li yongjian <lyj238@gmail.com>
Dear experts:
I download the latest version of Isabelle, and
I use the emacs interface of Isabelle, and type the following command:
isabelle emacs&

but I meet such a problem as follows:
How to solve it, can Isabelle support the calssical Emacs interface?

regards!

Loading /usr/share/emacs/site-lisp/site-start.d/focus-init.el
(source)...done
Loading /usr/share/emacs/site-lisp/site-start.d/php-mode-init.el
(source)...done
Loading /usr/share/emacs/site-lisp/site-start.d/po-mode-init.el
(source)...done
Loading /usr/share/emacs/site-lisp/site-start.d/rpm-spec-mode-init.el
(source)...done
For information about GNU Emacs and the GNU system, type C-h C-a.
Loading
/home/lyj/Isabelle2013-2/contrib/ProofGeneral-4.2/generic/proof-site.el
(source)...done
Scratch.thy has auto save data; consider M-x recover-this-file
Loading /home/lyj/Isabelle2013-2/contrib/ProofGeneral-4.2/isar/isar.el
(source)...
File mode specification error: (wrong-number-of-arguments
called-interactively-p 1)

Email Gateway (Aug 19 2022 at 13:02):

From: li yongjian <lyj238@gmail.com>
Dear experts:
I download the latest version of Isabelle, and
I use the emacs interface of Isabelle, and type the following command:
isabelle emacs&

but I meet such a problem as follows:
How to solve it, can Isabelle support the calssical Emacs interface?

regards!

Email Gateway (Aug 19 2022 at 13:02):

From: Lawrence Paulson <lp15@cam.ac.uk>
Maybe it’s incompatible with the version of emacs on your machine.

Try reading this page: http://proofgeneral.inf.ed.ac.uk/download

You need GNU Emacs 23.3 or later.

Larry Paulson

Email Gateway (Aug 19 2022 at 13:02):

From: Lawrence Paulson <lp15@cam.ac.uk>
Maybe it’s incompatible with the version of emacs on your machine.

Try reading this page: http://proofgeneral.inf.ed.ac.uk/download

You need GNU Emacs 23.3 or later.

Larry Paulson

Last updated: Nov 21 2024 at 12:39 UTC