Roberto Sebastiani | 1 Apr 2009 18:51
Picon
Favicon

FroCoS'09 Call for Papers

-------------------------------------------------------------------------
       WE APOLOGIZE IF YOU RECEIVE MULTIPLE COPIES OF THIS MESSAGE
-------------------------------------------------------------------------

                       Final Call for Papers

                 7th International Symposium on
            FRONTIERS OF COMBINING SYSTEMS (FroCoS’09)

              Trento, Italy, September 16-18th, 2009 
                http://events.unitn.it/en/frocos09/

MOTIVATIONS 
In various areas of computer science, such as logic, computation,
program development and verification, artificial intelligence, knowledge
representation, and automated reasoning, there is an obvious need for
using specialized formalisms and inference mechanisms for special
tasks. In order to be usable in practice, these specialized systems
must be combined with each other, and they must be integrated into
general purpose systems. The development of general techniques and
methods for the combination and integration of special formally defined
systems, as well as for the analysis and modularization of complex
systems has been initiated in many areas. The International Symposium
on Frontiers of Combining Systems (FROCOS) traditionally focuses on
this type of research questions and activities and aims at promoting
progress in the field. 
Like its predecessors, FROCOS’09 wants to offer a common forum for
research activities in the general area of combination, modularization
and integration of systems (with emphasis on logic-based ones), and of
their practical use.  
(Continue reading)

David Pichardie | 1 Apr 2009 21:57
Picon
Favicon

First CFP: PCC 2009

(We apologize if you receive multiple copies of this message)

============================================================

                        CALL FOR PAPERS
                           PCC 2009

                3rd International Workshop on 
        Proof Carrying Code and Software Certification

                      August 15, 2009 
                  Affiliated with LICS'09
               Los Angeles, California, USA

             http://ti.arc.nasa.gov/event/pcc09/

============================================================

IMPORTANT DATES
---------------
Papers due:   May 29, 2009
Notification of acceptance:     June 22, 2009
Final version due:  July 10, 2009


SCOPE
-----
Software certification demonstrates the reliability, safety, or
security of software systems in such a way that it can be checked by
an independent authority with minimal trust in the techniques and
tools used in the certification process itself. It can build on
existing validation and verification (V&V) techniques but introduces
the notion of explicit software certificates, which contain all the
information necessary for an independent assessment of the
demonstrated properties. One such example is proof-carrying code (PCC)
which is an important and distinctive approach to enhancing trust in
programs. It provides a practical framework for independent assurance
of program behaviour; especially where source code is not available,
or the code author and user are unknown to each other.

The workshop will address theoretical foundations of logic-based
software certification as well as practical examples and work on
alternative application domains. Here "certificate" is construed
broadly, to include not just mathematical derivations and proofs but
also safety and assurance cases, or any formal evidence that supports
the semantic analysis of programs: that is, evidence about an
intrinsic property of code and its behaviour that can be independently
checked by any user, intermediary, or third party. These guarantees
mean that software certificates raise trust in the code itself,
distinct from and complementary to any existing trust in the creator
of the code, the process used to produce it, or its distributor.

In addition to the contributed talks, the workshop will feature two
invited talks.


SUBMISSION
----------
Two types of submissions are solicited:
- Standard papers (at most 10 pages) describing novel research results.
- Short papers (at most 5 pages) describing a novel idea that is 
work-in-progress.

Additional material intended for the referees but not for publication
in the final version may be placed in a clearly marked appendix that
is not included in the page limit.

Authors are invited to submit their papers electronically, in PDF
format via the EasyChair submission web page:
http://www.easychair.org/conferences/?conf=pcc09

All submissions will be fully reviewed.


PUBLICATION
-----------
Proceedings will be made available in electronic format as a technical
report. A follow-up special issue of a journal on the topics of
proof-carrying code and software certification is under consideration.


PROGRAM COMMITTEE
-----------------
David Aspinall, University of Edinburgh
Gilles Barthe, IMDEA Software
Ewen Denney, RIACS/NASA Ames, co-chair
Bernd Fischer, University of Southampton
Sofia Guerra, Adelard
Kelly Hayhurst, NASA Langley
Thomas Jensen, IRISA/CNRS, co-chair
David Pichardie, INRIA
German Puebla, Technical University of Madrid
Ian Stark, University of Edinburgh
S B Cooper | 2 Apr 2009 00:04
Picon
Favicon

CiE 2009 - Call for Participation and Informal Presentations


                  CiE 2009: COMPUTABILITY IN EUROPE 2009 -
              Mathematical Theory and Computational Practice
                             Heidelberg, Germany
                              19 - 24 July 2009

       ************************************************************
            Call for Participation and Informal Presentations
       ************************************************************

            http://www.math.uni-heidelberg.de/logic/cie2009/

***********************************************************************

CALL FOR INFORMAL PRESENTATIONS AT CiE 2009:

There is a remarkable difference in conference style between computer 
science and mathematics conferences. Mathematics conferences allow for 
informal presentations that are prepared very shortly before the 
conference and inform the participants about current research and work 
in progress. The format of computer science conferences with 
pre-conference proceedings is not able to accommodate this form of 
scientific communication.

Again continuing the tradition of past CiE conferences, this year's CiE 
conference endeavours to get the best of both worlds. In addition to 
the formal presentations based on our LNCS proceedings volume, we 
invite researchers to present informal presentations. For this, please 
send us a brief description of your talk (between one paragraph and 
half a page) by the DEADLINE:

                               1 JUNE 2009.

Please submit your abstract by sending an informal email to our 
contact address:

                        logic <at> math.uni-heidelberg.de

You will be notified whether your talk has been accepted for informal 
presentation usually within a week after your submission.

Let us remind you that we are planning several post-conference 
publications, which will contain full articles of selected CiE 2009 
presentations, including informal presentations.

***********************************************************************
IMPORTANT DATES:

Submission of applications for ASL Student Grants: APRIL 19
Early registration deadline: MAY 15
Submission of informal presentations: JUNE 1
Late registration deadline: JULY 12

***********************************************************************
DETAILS OF PROGRAMME:

TUTORIALS: Pavel Pudlak (Prague), Luca Trevisan (Berkeley).

INVITED SPEAKERS: Manindra Agrawal (Kanpur), Jeremy Avigad (Pittsburgh), 
Phokion Kolaitis (San Jose), Peter Koepke (Bonn), Andrea Sorbi (Siena), 
Rafael D. Sorkin (Syracuse), Vijay Vazirani (Atlanta).

SPECIAL SESSIONS:

Algorithmic Randomness (Chairs: E. Mayordomo, W. Merkle). 
Confirmed invited speakers: Laurent Bienvenu, Bjoern Kjos-Hanssen, 
Jack Lutz, Nikolai Vereshchagin.

Computational Model Theory (Chairs: J. Knight, A. Morozov). 
Confirmed invited speakers: Ekaterina Fokina, Sergey Goncharov, 
Russell Miller, Antonio Montalban.

Computation in Biological Systems - Theory and Practice (Chairs: A. 
Carbone, E. Csuhaj-Varju). 
Confirmed invited speakers: Ion Petre, Alberto Policriti, 
Francisco J. Romero-Campero, David Westhead.

Optimization and Approximation (Chairs: M. Halldorsson, G. Reinelt). 
Cornfirmed invited speakers: Jean Cardinal, Friedrich Eisenbrand, Harald 
Raecke, Marc Uetz.

Philosophical and Mathematical Aspects of Hypercomputation (Chairs: J. 
Ladyman, P. Welch). 
Confirmed invited speakers: Tim Button, Samuel Coskey, Mark Hogarth.

Relative Computability (Chairs: R. Downey, A. Soskova). 
Confirmed invited speakers: Hristo Ganchev, Keng Meng Ng, Richard Shore, 
George Barmpalias.

For details of accepted contributed papers for CiE 2009 see:

http://www.math.uni-heidelberg.de/logic/cie2009/pr_contributed.php

***********************************************************************
PROGRAMME COMMITTEE:

Klaus Ambos-Spies (Heidelberg, co-chair), Giorgio Ausiello (Rome), Andrej
Bauer (Ljubljana), Arnold Beckmann (Swansea), Olivier Bournez (Palaiseau),
Vasco Brattka (Cape Town), Barry Cooper (Leeds), Anuj Dawar (Cambridge),
Jacques Duparc (Lausanne), Pascal Hitzler (Karlsruhe), Rosalie Iemhoff
(Utrecht), Margarita Korovina (Siegen/Novosibirsk), Hannes Leitgeb
(Bristol), Daniel Leivant (Bloomington), Benedikt Loewe (Amsterdam),
Giancarlo Mauri (Milan), Elvira Mayordomo (Zaragoza), Wolfgang Merkle
(Heidelberg, co-chair), Andrei Morozov (Novosibirsk), Dag Normann (Oslo),
Isabel Oitavem (Lisbon), Luke Ong (Oxford), Martin Otto (Darmstadt),
Prakash Panangaden (Montreal), Ivan Soskov (Sofia), Viggo
Stoltenberg-Hansen (Uppsala), Peter van Emde Boas (Amsterdam), Jan van
Leeuwen (Utrecht), Philip Welch (Bristol), Richard Zach (Calgary)

***********************************************************************
Contact: logic <at> math.uni-heidelberg.de
***********************************************************************


------------------------------------------------------------------------------
Sandip Ray | 2 Apr 2009 06:18
Picon

ACL2 2009 Call for Participation

[ Apologies if you get several copies of this call for participation.
  Please share it with students and colleagues who may be interested
  in the workshop. ]

===============================================================================
                         CALL FOR PARTICIPATION
===============================================================================
                            ACL2 2009
International Workshop on the ACL2 Theorem Prover and Its Applications
                           May 11-12, 2009
                   Northeastern University, Boston, MA, USA
                     http://www.cs.utexas.edu/~sandip/acl2-09/

                        In cooperation with ACM SIGPLAN

           ----------------------------------------------------
                Early Registration Deadline: April 12, 2009
           ----------------------------------------------------

ACL2 2009 is the eighth in a series of workshops on the ACL2 Theorem
Prover and Its Applications.  ACL2 is the most recent incarnation of
the Boyer-Moore family of theorem provers, for which Robert Boyer,
Matt Kaufmann, and J Moore received the 2005 ACM Software System Award.
It is a state-of-the-art automated reasoning system that has been
successfully used in academia, government, and industry for
specification and verification of computing systems.  The ACL2
workshops occur at approximately 18-month intervals and provide a
major technical forum for researchers to present and discuss
improvements and extensions to the theorem prover, comparisons of ACL2
with other systems, and applications of ACL2 in formal verification.

Invited Keynote
========================================================================
Clarke Barrett (NYU)
>From SAT to SMT: Successes and Challenges

Panel
=======================================================================
What is the Future of Theorem Proving?

PROGRAM 

Monday May 11

8:30 - 8:50 Registration/Coffee

8:50 - 9:00  Sandip Ray and David Russinoff
             Welcome and Opening Remarks

Session 1

9:00 - 9:25 Rob Sumners
            User Control and Direction of a More Efficient Simplifier in ACL2

9:25 - 9:50  J Moore
             Automatically Computing Functional Instantiations

9:50 - 10:05 Robert Boyer and Warren Hunt
             Symbolic Simulation in ACL2

10:05 - 10:20 Hanbing Liu
              Proving A Specific Type Of Inequality Theorems in ACL2: a bind-free experience report

10:20 - 10:35 (Short Break)

Session 2

10:35 - 10:50 Rex Page
             Computational Logic in the Undergraduate Curriculum

10:50 - 11:15 Carl Eastlund and Matthias Felleisen
              Automatically Verified GUI Programs

11:15 - 11:30 Carl Eastlund
              DoubleCheck Your Theorems

11:30 - 11:55 Antonio Garcia-Dominguez, Francisco Palomo-Lozano and Inmaculada Medina-Bulo
              Hypertext Navigation of ACL2 Proofs with XMLEye

11:55 - 1:25 (Lunch)

Session 3

1:25 - 1:50 Ruben Gamboa and John Cowles
            Inverse Functions in ACL2(r)

1:50 - 2:15 Matt Kaufmann
            Abbreviated Output for Input in ACL2

2:15 - 3:00 Matt Kaufmann and J Moore
            New and Desired Features of ACL2

3:00 - 3:30 (Long Break)

Session 4

3:30 - 3:45 Ryan Ralston
            ACL2-Certified AVL Trees

3:45 - 4:00 Fares Fares and Steve Roach
            Proof of Transitive Closure Property of Directed Acyclic Graphs

4:00 - 4:15 John Cowles and Ruben Gamboa
            \triangle = \square

4:15 - 4:30 (Short Break)

Session 5 (Moderator: Pete Manolios)

4:30 - 6:00 Panel: What is the Future of Theorem Proving?

7:30 - 9:00 Workshop Dinner
           Massimino's Restaurant, 207 Endicott Street

Tuesday May 12

8:30 - 9:00 Coffee

Session 6

9:00 - 9:25 Matt Kaufmann, Jacob Kornerup, Mark Reitblatt
           Formal Verification of LabVIEW Programs Using the ACL2 Theorem Prover

9:25 - 9:50 Laurence Pierre, Renauld Clavel, and Regis Leveugle
           ACL2 for the Verification of Fault-Tolerance Properties: First Results

9:50 - 10:15 David Hardin and Samuel Hardin
            Efficient, Formally Verifiable Data Structures using ACL2 Single-Threaded Objects for
High-Assurance Systems

10:15 - 10:30 David Rager
              An Executable Model for Security Protocol JFKr

10:30 - 11:00 (Break)

Session 7

11:00 - 11:55 TBA
             Rump Session

11:55 - 1:25 (Lunch)

Session 8

1:25 - 2:15 Clark Barrett, Invited Keynote Talk
           From SAT to SMT: Successes and Challenges

2:15 - 2:30 (Short Break)

Session 9

2:30 - 2:45 David Greve
            Automated Reasoning With Quantified Formulae

2:45 - 3:10 David Greve
            Assuming Termination

3:10 - 3:25 (Short Break)

Session 10

3:25 - 3:40 Tom van der Broek and Julien Schmaltz
           A Generic Implementation Model for the Formal Verification
of Networks-on-Chips

3:40 - 4:05 Freek Verbeek and Julien Schmaltz
           Formal Validation of Deadlock Prevention in Networks-on-Chips

4:05 - 4:20 (Short Break)

Session 11

4:20 - 4:45 TBA
           Rump Session

4:45 - 5:00 (Short Break)

Session 12

5:00 - 5:30 Matt Kaufmann, J Moore, and All
           Discussion on Possible Future Enhancements to ACL2

5:30 - 6:00 Sandip Ray, David Russinoff, and All
           Business Meeting

==============================================================================

ORGANIZATION

Co-Chairmen:         Sandip Ray,  University of Texas at Austin, USA 
                     David Russinoff, 	Advanced Micro Devices, Inc., USA
Local Arrangements:  Panagiotis Manolios, Northeastern University, USA
Publications:        Ruben Gamboa, University of Wyoming 

Steering Committee:  John Cowles, University of Wyoming, USA 
		     Ruben Gamboa, University of Wyoming, USA 
		     Matt Kaufmann, University of Texas at Austin, USA 
		     Panagiotis Manolios, Northeastern University, USA 
		     J Strother Moore, University of Texas at Austin, USA 
		     Jun Sawada, IBM Austin Research Laboratory, USA
		     Matt Wilding, Rockwell Collins, Inc., USA

==============================================================================
PROGRAM COMMITTEE

  * John Cowles, University of Wyoming, USA 
  * Ruben Gamboa, University of Wyoming, USA 
  * Mike Gordon, Cambridge University, UK 
  * Matt Kaufmann, University of Texas at Austin, USA 
  * Francisco Palomo Lozano, Universidad de Cadiz, Spain 
  * Panagiotis Manolios, Northeastern University, USA 
  * John Matthews, Galois, Inc., USA 
  * J Strother Moore, University of Texas at Austin, USA 
  * Rex Page, University of Oklahoma, USA
  * Jun Sawada, IBM Austin Research Laboratory, USA
  * Julien Schmaltz, Radboud University, Nijmegen, the Netherlands
  * Natarajan Shankar, SRI International, USA 
  * Rob Sumners, Advanced Micro Devices, Inc., USA 
  * Freek Wiedijk, Radboud University, Nijmegen, the Netherlands
  * Matt Wilding, Rockwell Collins, Inc., USA

------------------------------------------------------------------------------
Gabriel Dos Reis | 3 Apr 2009 20:10
Picon
Favicon

PLMMS 2009: Call for Paper


		  The ACM SIGSAM 2009 International
		Workshop on Programming Languages for
		    Mechanized Mathematics Systems
			      PLMMS 2009

		   Munich, Germany; August 21, 2009
		     http://plmms09.cse.tamu.edu/

			   CALL FOR PAPERS

The ACM SIGSAM 2009 International Workshop on Programming Languages
for Mechanized Mathematics Systems will be co-located with TPHOLs 2009. 

General Information

The scope of this workshop is at the intersection of programming
languages (PL) and mechanized mathematics systems (MMS). The latter
category subsumes present-day computer algebra systems (CAS),
interactive proof assistants (PA), and automated theorem provers
(ATP), all heading towards fully integrated mechanized mathematical
assistants. Areas of interest include all aspects of PL and MMS that
meet in the following topics, but not limited to:

  * Dedicated input languages for MMS: covers all aspects of languages
    intended for the user to deploy or extend the system, both
    algorithmic and declarative ones. Typical examples are tactic
    definition languages such as Ltac in Coq, mathematical proof
    languages as in Mizar or Isar, or specialized programming
    languages built into CA systems. 

  * Mathematical modeling languages used for programming: covers the
    relation of logical descriptions vs. algorithmic content. For
    instance the logic of ACL2 extends a version of Lisp, that of Coq
    is close to Haskell, and some portions of HOL are similar to ML
    and Haskell, while Maple tries to do both simultaneously. Such
    mathematical languages offer rich specification capabilities,
    which are rarely available in regular programming languages. How
    can programming benefit from mathematical concepts, without
    limiting mathematics to the computational world view?

  * Programming languages with mathematical specifications: covers
    advanced mathematical concepts in programming languages that
    improve the expressive power of functional specifications, type
    systems, module systems etc. Programming languages with dependent
    types are of particular interest here, as is intentionality vs
    extensionality. 

  * Language elements for program verification: covers specific means
    built into a language to facilitate correctness proofs using
    MMS. For example, logical annotations within programs may be
    turned into verification conditions to be solved in a proof
    assistant eventually. How need MMS and PL to be improved to make
    this work conveniently and in a mathematically appealing way?

These issues have a very colorful history. Many PL innovations first
appeared in either CA or proof systems first, before migrating into
more mainstream programming languages.  This workshop is an
opportunity  to present the latest innovations in MMS design that may 
be relevant to future programming languages, or conversely novel PL 
principles that improve upon implementation and deployment of MMS.  
Why are all the languages of mainstream CA systems untyped?  Why 
are the (strongly typed) proof assistants so much harder to use than 
a typical CAS?  What forms of polymorphism exist in mathematics?  
What forms of dependent types may be used in mathematical modeling?  
How can MMS regain the upper hand on issues of "genericity" and
"modularity"?  What are the biggest barriers to using a more
mainstream language as a host language for a CAS or PA/ATP? 

PLMMS 2007 was held as a satellite event of, and PLMMS 2008 was
a CICM 2008 workshop.

Submission Details

  * Submission deadline: May 11, 2009 (Apia, Samoa time)
  * Author Notification:  June 22, 2009 
  * Final Papers Due: July 10, 2009
  * Workshop: August 21, 2009

   Submitted papers should be in portable document format (PDF),
   formatted using the ACM SIGPLAN style guidelines
   (http://www.acm.org/sigs/sigplan/authorInformation.htm). The length
   is restricted to 10 pages, and the font size 9pt. Each submission
   must adhere to SIGPLAN's republication policy, as explained on the
   web. Violation risks summary rejection of the offending submission.

  Papers are exclusively submitted via EasyChair

          http://www.easychair.org/conferences?conf=plmms09

   We expect that at least one author of each accepted paper attends
   PLMMS 2009 and presents her or his paper.

   Accepted papers will appear in the ACM Digital Library.

Links

  * http://plmms09.cse.tamu.edu/, the PLMMS 2009 workshop web site
  * http://tphols.in.tum.de/, the THOPLs 2009 conference web site

Program Committee

  * Clemens Ballarin, aicas GmbH
  * Gabriel Dos Reis, Texas A&M University (Co-Chair)
  * Jean-Christophe Filliâtre, CNRS Université Paris Sud
  * Predrag Janinic, University of Belgrade
  * Jaakko Järvi, Texas A&M University
  * Florina Piroi, Johannes Kepler University
  * Laurent Théry, INRIA Sophia Antipolis (Co-Chair)
  * Makarius Wenzel, Technische Universität München

------------------------------------------------------------------------------
Peter Vincent Homeier | 3 Apr 2009 22:12
Favicon

Re: Uncaught exception: Chr

It turns out that the instructions Peter Sestoft sent you were
slightly incomplete.

In particular, before the 'make all' in steps 3 and 6, one must
'touch' the new files so that the make recognizes these are new
versions of the files.  Crucially, in step 8, one should use
'./camlrunm' instead of 'camlrunm'; otherwise one would invoke the
installed version and get a bus error, and may mistakenly think that
the build went wrong in some inexplicable way, when it actually
worked.

Finally, when rebuilding HOL, make sure to first go through all of the
subdirectories of tools and do either 'make clean' or 'Holmake clean'
as appropriate, in order to clean out all the old object code produced
by the prior version of mosml, and then do the normal 'mosml <
tools/smart-configure.sml' followed by 'build cleanAll' and 'build'
commands.

May I suggest that these instructions be added to the HOL installation
instructions at http://hol.sourceforge.net/InstallKananaskis.html?

Here is the corrected version:

----------------------------------------------------------------------
  0. Make a backup of your old mosml installation

  1. Before unpacking the attached, make a build of mosml 2.01:

     In mosml/src/ do    make clean world

  2. Unpack the attached:

     In mosml/src/ do    tar xvfz mosml-patch.tgz

  3. Recompile the compiler to generate the new bytecode:

     In mosml/src/compiler do    touch Patch.sml Reloc.sml
                                 make all

  4. Promote the compiler:

     In mosml/src/compiler do    mv mosmllnk mosmlcmp ..

     (I believe mosmllnk is unchanged, but promote for good measure)

  5. Generate new bytecode for libraries, compiler and lexer by
     recompiling:

     In mosml/src/mosmllib do    make clean all
     In mosml/src/compiler do    make clean all
     In mosml/src/lex do         make clean all

  6. Recompile the runtime:

     In mosml/src/runtime do     touch expand.c fix_code.c interp.c
                                 make all

  7. Promote the runtime, compiler and lexer:

     In mosml/src/runtime do     mv camlrunm ..
     In mosml/src/compiler do    mv mosmllnk mosmlcmp ..
     In mosml/src/lex do         mv mosmllex ..

  8. Check that the top-level works:

     In mosml/src do   ./camlrunm compiler/mosmltop -stdlib mosmllib

     and evaluate some expressions.

  9. Rebuild everything to check that the system is stable:

     In mosml/src do   make clean world

     Check that src/mosmlcmp = src/compiler/mosmlcmp
                src/mosmllnk = src/compiler/mosmllnk
                src/mosmllex = src/lex/mosmllex

10. Install

     In mosml/src do   make install

11. Check that HOL builds.
----------------------------------------------------------------------

Cheers, Peter

On Wed, Oct 15, 2008 at 8:19 PM, Michael Norrish
<Michael.Norrish <at> nicta.com.au> wrote:
> Peter Vincent Homeier wrote:
>  > I also see this bug happen when trying to build examples/acl2/ml.
>  >  However, this patch doesn't seem to build right on a Mac running OS X
>  > (10.4) with the following gcc:
>
> Yes, I'm afraid the instructions in my post yesterday were far too
> casual (not to mention wrong!).  I have Peter Sestoft's original here:
>
> ----------------------------------------------------------------------
>  0. Make a backup of your old mosml installation
>
>  1. Before unpacking the attached, make a build of mosml 2.01:
>
>     In mosml/src/ do    make clean world
>
>  2. Unpack the attached:
>
>     In mosml/src/ do    tar xvfz mosml-patch.tgz
>
>  3. Recompile the compiler to generate the new bytecode:
>
>     In mosml/src/compiler do    make all
>
>  4. Promote the compiler:
>
>     In mosml/src/compiler do    mv mosmllnk mosmlcmp ..
>
>     (I believe mosmllnk is unchanged, but promote for good measure)
>
>  5. Generate new bytecode for libraries, compiler and lexer by
>     recompiling:
>
>     In mosml/src/mosmllib do    make clean all
>     In mosml/src/compiler do    make clean all
>     In mosml/src/lex do         make clean all
>
>  6. Recompile the runtime:
>
>     In mosml/src/runtime do     make all
>
>  7. Promote the runtime, compiler and lexer:
>
>     In mosml/src/runtime do     mv camlrunm ..
>     In mosml/src/compiler do    mv mosmllnk mosmlcmp ..
>     In mosml/src/lex do         mv mosmllex ..
>
>  8. Check that the top-level works:
>
>     In mosml/src do   camlrunm compiler/mosmltop -stdlib mosmllib
>
>     and evaluate some expressions.
>
>  9. Rebuild everything to check that the system is stable:
>
>     In mosml/src do   make clean world
>
>     Check that src/mosmlcmp = src/compiler/mosmlcmp
>                src/mosmllnk = src/compiler/mosmllnk
>                src/mosmllex = src/lex/mosmllex
>
> 10. Install
>
>     In mosml/src do   make install
>
> 11. Check that HOL builds.
> ----------------------------------------------------------------------

--

-- 
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)

------------------------------------------------------------------------------
Peter Vincent Homeier | 5 Apr 2009 00:35
Favicon

Re: Uncaught exception: Chr

I tried this on a Macintosh running Mac OS X version 10.5.6 (Leopard),
and the process failed in step 6, when doing "make all" in the runtime
directory:

MinasTirith:runtime palantir$ make all
gcc -c -Dunix -O2 -fno-defer-pop -fomit-frame-pointer -DTHREADED
-I/Users/palantir/sml/mosml/include -o interp.o interp.c
gcc -c -Dunix -O2 -fno-defer-pop -fomit-frame-pointer -DTHREADED
-I/Users/palantir/sml/mosml/include -o expand.o expand.c
gcc -c -Dunix -O2 -fno-defer-pop -fomit-frame-pointer -DTHREADED
-I/Users/palantir/sml/mosml/include -o fix_code.o fix_code.c
sed -n -e '/\/\* ML \*\//s/.* \([a-zA-Z0-9_][a-zA-Z0-9_]*\) *(.*/\1/p' \
                compare.c extern.c externcp.c floats.c gc_ctrl.c
hash.c intern.c interncp.c interp.c ints.c io.c lexing.c meta.c
parsing.c str.c sys.c mosml.c unix.c md5sum.c callback.c dynlib.c >
primitives2
sh -c 'if cmp -s primitives primitives2; \
        then rm primitives2; \
        else mv primitives2 primitives; \
        fi'
gcc -o camlrunm prims.o interp.o expand.o misc.o stacks.o fix_code.o
main.o fail.o signals.o freelist.o major_gc.o minor_gc.o memory.o
alloc.o roots.o compare.o ints.o floats.o str.o io.o extern.o
externcp.o intern.o interncp.o hash.o sys.o meta.o parsing.o lexing.o
gc_ctrl.o mosml.o unix.o runtime.o md5sum.o callback.o dynlib.o -lm
-L/Users/palantir/sml/mosml/lib -ldl
/usr/bin/ld: /usr/lib/gcc/i686-apple-darwin8/4.0.1/../../../libm.dylib
unknown flags (type) of section 6 (__TEXT,__literal16) in load command
0
/usr/bin/ld: /usr/lib/gcc/i686-apple-darwin8/4.0.1/../../../libdl.dylib
unknown flags (type) of section 6 (__TEXT,__literal16) in load command
0
/usr/bin/ld: /usr/lib/gcc/i686-apple-darwin8/4.0.1/../../../libSystem.dylib
unknown flags (type) of section 6 (__TEXT,__literal16) in load command
0
collect2: ld returned 1 exit status
make: *** [camlrunm] Error 1
MinasTirith:runtime palantir$ gcc --version
i686-apple-darwin8-gcc-4.0.1 (GCC) 4.0.1 (Apple Computer, Inc. build 5363)
. . .

Does anyone have an idea that might help?  Do I need a new version of
gcc?  Has anyone else had success performing this upgrade under
Leopard?

Thanks for helping.

Peter

On Fri, Apr 3, 2009 at 4:12 PM, Peter Vincent Homeier
<palantir <at> trustworthytools.com> wrote:
> It turns out that the instructions Peter Sestoft sent you were
> slightly incomplete.
>
> In particular, before the 'make all' in steps 3 and 6, one must
> 'touch' the new files so that the make recognizes these are new
> versions of the files.  Crucially, in step 8, one should use
> './camlrunm' instead of 'camlrunm'; otherwise one would invoke the
> installed version and get a bus error, and may mistakenly think that
> the build went wrong in some inexplicable way, when it actually
> worked.
>
> Finally, when rebuilding HOL, make sure to first go through all of the
> subdirectories of tools and do either 'make clean' or 'Holmake clean'
> as appropriate, in order to clean out all the old object code produced
> by the prior version of mosml, and then do the normal 'mosml <
> tools/smart-configure.sml' followed by 'build cleanAll' and 'build'
> commands.
>
> May I suggest that these instructions be added to the HOL installation
> instructions at http://hol.sourceforge.net/InstallKananaskis.html?
>
> Here is the corrected version:
>
> ----------------------------------------------------------------------
>  0. Make a backup of your old mosml installation
>
>  1. Before unpacking the attached, make a build of mosml 2.01:
>
>     In mosml/src/ do    make clean world
>
>  2. Unpack the attached:
>
>     In mosml/src/ do    tar xvfz mosml-patch.tgz
>
>  3. Recompile the compiler to generate the new bytecode:
>
>     In mosml/src/compiler do    touch Patch.sml Reloc.sml
>                                 make all
>
>  4. Promote the compiler:
>
>     In mosml/src/compiler do    mv mosmllnk mosmlcmp ..
>
>     (I believe mosmllnk is unchanged, but promote for good measure)
>
>  5. Generate new bytecode for libraries, compiler and lexer by
>     recompiling:
>
>     In mosml/src/mosmllib do    make clean all
>     In mosml/src/compiler do    make clean all
>     In mosml/src/lex do         make clean all
>
>  6. Recompile the runtime:
>
>     In mosml/src/runtime do     touch expand.c fix_code.c interp.c
>                                 make all
>
>  7. Promote the runtime, compiler and lexer:
>
>     In mosml/src/runtime do     mv camlrunm ..
>     In mosml/src/compiler do    mv mosmllnk mosmlcmp ..
>     In mosml/src/lex do         mv mosmllex ..
>
>  8. Check that the top-level works:
>
>     In mosml/src do   ./camlrunm compiler/mosmltop -stdlib mosmllib
>
>     and evaluate some expressions.
>
>  9. Rebuild everything to check that the system is stable:
>
>     In mosml/src do   make clean world
>
>     Check that src/mosmlcmp = src/compiler/mosmlcmp
>                src/mosmllnk = src/compiler/mosmllnk
>                src/mosmllex = src/lex/mosmllex
>
> 10. Install
>
>     In mosml/src do   make install
>
> 11. Check that HOL builds.
> ----------------------------------------------------------------------
>
> Cheers, Peter
>
>
> On Wed, Oct 15, 2008 at 8:19 PM, Michael Norrish
> <Michael.Norrish <at> nicta.com.au> wrote:
>> Peter Vincent Homeier wrote:
>>  > I also see this bug happen when trying to build examples/acl2/ml.
>>  >  However, this patch doesn't seem to build right on a Mac running OS X
>>  > (10.4) with the following gcc:
>>
>> Yes, I'm afraid the instructions in my post yesterday were far too
>> casual (not to mention wrong!).  I have Peter Sestoft's original here:
>>
>> ----------------------------------------------------------------------
>>  0. Make a backup of your old mosml installation
>>
>>  1. Before unpacking the attached, make a build of mosml 2.01:
>>
>>     In mosml/src/ do    make clean world
>>
>>  2. Unpack the attached:
>>
>>     In mosml/src/ do    tar xvfz mosml-patch.tgz
>>
>>  3. Recompile the compiler to generate the new bytecode:
>>
>>     In mosml/src/compiler do    make all
>>
>>  4. Promote the compiler:
>>
>>     In mosml/src/compiler do    mv mosmllnk mosmlcmp ..
>>
>>     (I believe mosmllnk is unchanged, but promote for good measure)
>>
>>  5. Generate new bytecode for libraries, compiler and lexer by
>>     recompiling:
>>
>>     In mosml/src/mosmllib do    make clean all
>>     In mosml/src/compiler do    make clean all
>>     In mosml/src/lex do         make clean all
>>
>>  6. Recompile the runtime:
>>
>>     In mosml/src/runtime do     make all
>>
>>  7. Promote the runtime, compiler and lexer:
>>
>>     In mosml/src/runtime do     mv camlrunm ..
>>     In mosml/src/compiler do    mv mosmllnk mosmlcmp ..
>>     In mosml/src/lex do         mv mosmllex ..
>>
>>  8. Check that the top-level works:
>>
>>     In mosml/src do   camlrunm compiler/mosmltop -stdlib mosmllib
>>
>>     and evaluate some expressions.
>>
>>  9. Rebuild everything to check that the system is stable:
>>
>>     In mosml/src do   make clean world
>>
>>     Check that src/mosmlcmp = src/compiler/mosmlcmp
>>                src/mosmllnk = src/compiler/mosmllnk
>>                src/mosmllex = src/lex/mosmllex
>>
>> 10. Install
>>
>>     In mosml/src do   make install
>>
>> 11. Check that HOL builds.
>> ----------------------------------------------------------------------
>
> --
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>

--

-- 
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)

------------------------------------------------------------------------------
Natarajan Shankar | 7 Apr 2009 04:08
Favicon

Automated Formal Methods '09: Second Call For Papers


                        CALL FOR PAPERS
                   Automated Formal Methods (AFM09)
                   June 27, 2009, Grenoble, France
                    http://fm.csl.sri.com/AFM09/

         In association with Computer-Aided Verification 2009
	         http://www-cav2009.imag.fr/

AFM is a one-day workshop centered around the use and integration of formal
verification tools for specification, interactive theorem proving,
satisfiability (SAT) and satisfiability modulo theories (SMT), model
checking, program verification, code generation, and testing, as well as
interfaces, documentation, and education.  This workshop was first initiated
as a users' group meeting for the SRI formal verification tools such as PVS,
SAL, and Yices, but the topics are not restricted to these tools.  The first
workshop was held at FLoC'06, the second workshop with ASE'07, and the third
workshop took place in conjunction with CAV'08.

We welcome position papers on the topics listed above, particularly those
that report on experiments and case studies.  Papers must be fewer than 8
pages long in the ACM SIG Proceedings style
(http://www.acm.org/sigs/publications/proceedings-templates) and should be
submitted to
   http://www.easychair.org/conferences/?conf=afm09
The post-conference proceedings will be published in the ACM Digital
Library.    

PROGRAM CHAIRS: Hassen Saidi, Natarajan Shankar   

PROGRAM COMMITTEE: Myla Archer, Saddek Bensalem, Supratik Chakraborthy,
Rance de Long, Leonardo de Moura, Jean-Christophe Filliatre, Bernd
Finkbeiner, Michael Gordon, John Harrison, Peter Manolios, David
Monniaux, David Naumann, Corina Pasareanu, Lee Pike, Kazuhiro Ogata,
Sanjit Seshia, Ofer Strichman.

KEY DATES:
  Position papers due: April 30, 2009 
  Reviews/decisions: May 20, 2009
  Camera ready versions due: June 10, 2009
  AFM '09 Workshop: June 27, 2009

------------------------------------------------------------------------------
This SF.net email is sponsored by:
High Quality Requirements in a Collaborative Environment.
Download a free trial of Rational Requirements Composer Now!
http://p.sf.net/sfu/www-ibm-com
Martin Leucker | 6 Apr 2009 21:02
Picon
Favicon

Final CfP: ICTAC'09 - Last Chance

Our apology for possible multiple copies.
----------------------------------------------------------------------

LINE + EXTENDED DEADLINE + EXTENDED DEADLINE + EXTENDED DEADLINE + EXT
12 April 2009 + 12 April 2009 + 12 April 2009 + 12 April 2009 + 

----------------------------------------------------------------------
			       ICTAC'09

   6th International Colloquium on Theoretical Aspects of Computing

		     ***   CALL FOR PAPERS   ***

		   Equatorial Hotel Bangi, Malaysia
		 University Kebangsaan Malaysia (UKM)

		       August 16th - 20th 2009

		    http://www.ictac.net/ictac09/
----------------------------------------------------------------------

The 6th International Colloquium  on Theoretical Aspects  of Computing
is taking place from  the 16th till the  20th of August 2009  in Kuala
Lumpur, Malaysia. ICTAC'09  is     organized by Abdullah   Mohd   Zin,
Universiti Kebangsaan  Malaysia   and  Jeff Sanders,    United  Nation
University, Institute  of   Software Technology,  Macao.  The   PC  is
chaired by Martin Leucker (TU Munich) and Carroll Morgan (UNSW).

Visit http://www.ictac.net/ictac09 for a preliminary web page.

About ICTAC 2009
----------------

ICTAC 2009 is the 6th  International Colloquium on Theoretical Aspects
of  Computing, the latest  in  a series  founded by the  International
Institute for  Software  Technology of  the  United Nations University
(UNU-IIST).  The    main purpose  of  ICTAC   is    to bring  together
practitioners and researchers  from academia,  industry and government
to present research and  to  exchange ideas and  experience addressing
challenges  in  both theoretical  aspects  of   computing and in   the
exploitation   of   theory  through  methods   and  tools   for system
development. The previous four   ICTAC  events were held  in  Guiyang,
China (2004), Hanoi,   Vietnam (2005),  Tunis, Tunisia (2006),   Macau
(2007) and Istanbul (2008).

Workshops
---------

The main  conference  is   surrounded  by  workshops  and  a    summer
school. See the web page for more details.

Invited Speakers
----------------
Zuohua Ding	 Zhejiang Sci-Tech University
Leslie Lamport   Microsoft
Annabelle McIver Macquarie University
Sriram Rajamani  Microsoft

Scope 
-----

Topics include, but are not limited to:

  * software specification, refinement, verification and testing
  * model checking and theorem proving
  * software architectures
  * coordination and feature interaction
  * integration of theories, formal and engineering methods and tools
  * models of concurrency, security, and mobility
  * parallel, distributed, and internet-based (grid) computing
  * real-time, embedded and hybrid systems
  * automata theory and formal languages
  * principles and semantics of languages
  * logics and their applications
  * type and category theory in computer science
  * case studies, theories, tools and experiments of verified systems  
  * service-oriented architectures: models and development methods
  * domain modelling and domain-specific technology: examples,
    frameworks and experience 

Paper Submissions
-----------------

ICTAC 2009  calls for two types  of contributions: RESEARCH PAPERS and
TOOL DEMONSTRATION PAPERS. Both types  of contributions will appear in
the  LNCS   proceedings    and have    oral     presentations at   the
conference. Papers should be written in English in LNCS format.

RESEARCH PAPERS:

Research   papers  should  contain  original  research, and sufficient
detail to   assess  the merits  and  relevance  of  the  contribution. 
Submissions  reporting on  industrial  case  studies are welcome,  and
should  describe both  strengths and  weaknesses  in sufficient depth. 
Research papers should be no more than 15 pages.

TOOL DEMONSTRATION PAPERS:

Tool demonstration    papers present  tools   based on  aforementioned
theories or fall into the above  application areas. Tool demonstration
papers allow researchers to  stress the technical and practical  side,
illustrating how one    can   apply the  theoretic  contributions   in
practice. Tool demonstration papers should be no more than 6 pages.

As  usual, submissions to the conference  must not have been published
or    be  concurrently   considered  for  publication   elsewhere. All
submissions will  be judged on  the basis of originality, contribution
to the field, technical and presentation quality, and relevance to the
conference.  Submission constitutes a commitment to attend and present
a paper, if accepted.

Proceedings  of ICTAC 2009 will be  published by Springer  in the LNCS
series.

Important Dates
---------------

Submission of Papers:       12 April 2009 (extended by 2 days)
Notification of acceptance: 25 May   2009
Final copy for proceedings:  1 June  2009
ICTAC 2009:                 16 - 20 August 2009

 
Committees
----------

General Chair
-------------
Abdullah Mohd Zin  Universiti Kebangsaan Malaysia
Jeff Sanders       United Nation University, Institute of Software
                   Technology, Macao 

Program Chairs
--------------
Martin Leucker     Technische Universität München, Germany
Carroll Morgan     University of New South Wales

Local Organizing Committee
--------------------------
Zarina Shukur, Universiti Kebangsaan Malaysia (Chairperson)
Nazlia Omar
Syahanim Mohd Salleh

Program Committee
-----------------

Parosh Abdulla      Uppsala University, Schweden
Keijiro Araki       Kyushu University, Japan
Farhad Arbab        Leids University, The Netherlands
Christel Baier	    Technical University of Dresden, Germany
Mario Bravetti	    Universita di Bologna, Italian
Ana Cavalcanti	    University of York, England
Van Hung Dang       United Nations University, Macao
David Deharbe	    Federal University of Rio Grande do Norte, Brazil
Wei Dong	    National University of Defense Technology, China
Deepak D'Souza	    Indian Institute of Science, India
John Fitzgerald	    Newcastle Uiversity, England
Wan Fokkink	    Vrije University Amsterdam, The Netherlands
Marcelo Frias	    University of Buenos Aires,  Argentina
Kokichi Futatsugi   JAIST, Japan
Paul Gastin	    LSV/ENS Cachan, France
Susanne Graf	    VERIMAG, France
Lindsay Groves	    Victoria University of Wellington, New Zealand
Anne Haxthausen	    Technical University of Denmark, Denmark
Moonzoo Kim	    KAIST, South Korea
Kim G. Larsen	    Aalborg University, Denmark
Insup Lee	    University of Pennsylvania, USA
Martin Leucker	    TU Munich, Germany
Kamal Lodaya	    Institute of Mathematical Sciences, India
Larissa Meinicke    Abo Akademi, Finland
Ugo Montanari	    University of Pisa, Italian
Carroll Morgan	    University of New South Wales, Australia
Ahmed Patel	    Universiti Kebangsaan Malaysia, Malaysia
Pekka Pihlajasaari  Data Abstraction (Pty) Ltd, South Africa
Abhik Roychoudhury  National University of Singapore, Singapore
Hassen Saidi	    SRI International, USA
Augusto Sampaio	    Universidade Federal de Pernambuco, Brazil
Cesar Sanchez	    IMDEA, Spain
Marjan Sirjani	    University of Tehran, Iran
Sofiene Tahar	    Concordia University, Canada
Serdar Tasiran	    Koc University, Turkey
Helmut Veith	    Technical University Darmstadt, Germany
Mahesh Viswanathan  University of Illinois at Urbana, USA
Tomas Vojnar	    Brno University of Technology, Czech Republic
Ji Wang		    Zhejiang University, China
Jim Woodcock	    University of York, England
Husnu Yenigun	    Sabanci University, Turkey
Naijun Zhan	    Chinese Academy of Sciences, China
Huibiao Zhu	    East China Normal University, China

Steering Committee
------------------

John Fitzgerald     University of Newcastle upon Tyne, UK
Martin Leucker 	    Technische Universität München, Germany
Zhiming Liu (Chair) UNU-IIST, Macao
Tobias Nipkow       Technische Universität München, Germany
Augusto Sampaio     Universidade Federal de Pernambuco, Brazil
Natarajan Shankar   SRI, USA
Jim Woodcock        University of York, UK

------------------------------------------------------------------------------
This SF.net email is sponsored by:
High Quality Requirements in a Collaborative Environment.
Download a free trial of Rational Requirements Composer Now!
http://p.sf.net/sfu/www-ibm-com
Bernardo Cuenca Grau | 7 Apr 2009 18:25
Picon
Picon

2nd CfP: 22nd International Workshop on Description Logics (DL 2009)

Apologies for cross posting

---------------------------------------------------------------------

     22st International Workshop on Description Logics (DL 2009)
                           CALL FOR PAPERS
                     Oxford, United Kingdom
                           27-30 July 2009

                      http://dl.kr.org/dl2009/

The DL workshop is the major annual event of the description logic
research community. The workshop is thought as a gathering forum to
meet, discuss and exchange experiences among all those, both in the
academia and industry, who are interested in description logics and
their applications.

----------------------------------------------------------------------

IMPORTANT DATES

Paper submission deadline:  20    April 2009 (strict!)
Notification of acceptance: 01    June  2009
Camera ready papers due:    22    June  2009
DL'07 Workshop:             27-30 July  2008 (3 1/2 days)

----------------------------------------------------------------------

WORKSHOP SCOPE

We invite contributions on all aspects of description logics,
such as

* foundations of description logics, including expressive power,
  decidability and complexity of reasoning, novel inference problems,
  and reasoning techniques for solving these problems;

* extensions of description logics, including, but not limited to,
  closed-world and nonmonotonic reasoning, defaults, epistemic
  reasoning, temporal and spatial reasoning, procedural knowledge, and
  query languages;

* integration of description logics with other formalisms, such as
  object-oriented representation languages, database query languages,
  constraint-based programming, logic programming, and rule-based
  systems;

* use of description logics in applications or areas such as ontology
  engineering, ontology languages, databases, semi-structured data,
  document management, natural language, learning, planning, semantic
  web, and grid computing;

* building systems based on description logics, with special emphasis
  on optimization and implementation techniques; and

* tools that exploit description logic reasoning, such as ontology
  editors, database schema design, query optimization, and data
  integration tools.

----------------------------------------------------------------------

SUBMISSION DETAILS

We invite submissions of papers in Springer LNCS style, see

    http://www.springer.com/comp/lncs/Authors.html

to arrive no later than April 20, 2009.

The length of submissions is limited to 11 pages, including title and
abstract (can be omitted if necessary), but excluding references
(i.e., the length of the paper without the references must be at most
11 pages). Papers must be submitted in PDF format via EasyChair; see

    http://www.easychair.org/conferences/?conf=dl2009

The workshop proceedings will be made available electronically in the
CEUR Workshop Proceedings series; see

    http://www.CEUR-ws.org/

Accepted submissions will be selected for either oral or poster
presentation; however, no distinction will be made in the workshop
proceedings: all accepted papers can be 11 pages long.

----------------------------------------------------------------------

INVITED SPEAKERS

* Leonid Libkin, University of Edinburgh, UK

* Kavitha Srinivas, IBM Research, USA

* Rajeev Gore, The Australian National University, Australia

----------------------------------------------------------------------

WORKSHOP CHAIRS

* Ian Horrocks, Oxford, UK (Workshop chair)
* Bernardo Cuenca Grau, Oxford, UK (PC Chair)
* Boris Motik, Oxford, UK (PC Chair)

----------------------------------------------------------------------

PROGRAM COMMITTEE

* Achille Fokoue, IBM Research, USA
* Aditya Kalyanpur, IBM Research, USA
* Alex Borgida, Rutgers University, USA
* Anni-Yasmin Turhan, TU Dresden, Germany
* Bijan Parsia, University of Manchester, UK
* Birte Glimm, University of Oxford, UK
* Carlos Areces, LORIA, France
* Carsten Lutz, University of Bremen, Germany
* Diego Calvanese, Free University of Bozen-Bolzano, Italy
* Dirk Walther, University of Liverpool, UK
* Evren Sirin, IBM Research, USA
* Frank Wolter, University of Liverpool, UK
* Giorgos Stamou, National Technical University of Athens, Greece
* Grant Weddell, University of Waterloo, Canada
* Jeff Z. Pan, University of Aberdeen, UK
* Jos de Bruijn, Free University of Bolzano, Italy
* Luciano Serafini, ITC-IRST, Italy
* Magdalena Ortiz, TU Vienna, Austia
* Maja Milicic, TU Dresden, Germany
* Markus Krötzsch, University of Karlsruhe, Germany
* Meghyn Bienvenu, University of Bremen, Germany
* Oliver Kutz, University of Bremen, Germany
* Pascal Hitzler, University of Karlsruhe, Germany
* Peter Patel-Schneider, Bell Labs Research, USA
* Rajeev Gore, Australian National University, Australia
* Ralf Möller, Hamburg University of Technology, germanz
* Riccardo Rosati, Sapienza Universita di Roma, Italy
* Robert Stevens, University of Manchester, UK
* Roman Kontchakov, Birkbeck College, UK
* Sebastian Rudolph, University of Karlsruhe, Germany
* Stefan Schlobach, Vrije Universiteit Amsterdam, The Netherlands
* Stijn Heymans, TU Vienna, Austia
* Thomas Meyer, Meraka Institute, South Africa
* Thomas Schneider, University of Manchester, UK
* Umberto Straccia, ISTI-CNR, Italy
* Viorica Sofronie-Stokkermans, Max-Planck-Institute, Germany
* Volker Haarslev, Concordia University, Canada
* Yevgeny Kazakov, University of Oxford, UK

----------------------------------------------------------------------

RESOURCES

* Information about registration, travel information, accommodation,
  and so on will be made available on the DL 2009 homepage:

        http://dl.kr.org/dl2009/

* Enquiries about the DL 2009 workshop can be made by contacting
  the organizing committee:

        dl2009 <at> easychair.org

* The official Description Logic home page is at

        http://dl.kr.org/

----------------------------------------------------------------------

------------------------------------------------------------------------------
This SF.net email is sponsored by:
High Quality Requirements in a Collaborative Environment.
Download a free trial of Rational Requirements Composer Now!
http://p.sf.net/sfu/www-ibm-com

Gmane