Wolfgang Ahrendt | 2 May 13:30 2005


[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]


CADE-20 Workshop on

Non-Theorems, Non-Validity, Non-Provability

Tallinn, Estonia
Friday, July 22, 2005

Call for Papers


for a web version of this CFP, see:



Automated Reasoning (AR) traditionally has focused on proving
theorems. Because of this, AR methods and tools in the past were
mostly applied to formulae which were already known to be true. If on
the other hand a formula is not a theorem, then most traditional AR
methods and tools cannot handle this properly (i.e. they will fail,
run out of resources, or simply not terminate).
(Continue reading)

AVoCS 2005 | 3 May 02:25 2005

AVoCS '05 [First CALL for PAPERS]

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]


AVoCS '05
Fifth International Workshop on
Automated Verification of Critical Systems

University of Warwick, UK, 12-13 September 2005


The aim of this workshop is to encourage interaction and exchange of
ideas among members of the international research community.
Particularly, we hope to achieve integration and transfer of knowledge
between academia and industry.

The workshop subject is to be interpreted broadly and inclusively.
It covers all aspects of automated verification (model checking, theorem
proving, specification, etc) pertaining to various types of critical
systems, be it safety-critical, business-critical, or

The technical programme will consist of invited talks, regular papers,
and short presentations.  The workshop will be relatively informal,
with an emphasis on discussion.

Previous AVoCS workshops were held at the University of Oxford (2001),
the University of Birmingham (2002), the University of Southampton
(Continue reading)

ICLP 2005 | 3 May 17:44 2005

ICLP 2005: Extended Deadlines

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

                           Call for Papers

    Twenty first International Conference on Logic Programming

                          2-5 October, 2005
                      Sitges (Barcelona) Spain

          Co-located with the International Conference on
     Principles and Practice of Constraint Programming (CP'05)


         New abstract submission deadline:  May  8th, 2005 
         New paper submission deadline:     May 11th, 2005

  [* Please note that ICLP'05 has a doctoral consortium for the first
     time as well as a special industrial paper session (details
   * Note that ICLP05's dates intersect with a solar eclipse visible
     in Barcelona ].

The Conference

The 21st  International Conference on  Logic Programming will  be held
(Continue reading)

Fabio Martinelli | 2 May 15:50 2005

FAST2005: Extended deadline for the 3rd International Workshop on Formal Aspects in Security and Trust

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

                        [apologies for multiple copies]

        !!!!NEWS:  EXTENDED DEADLINE and updated submission instructions!!!!

3rd International Workshop on Formal Aspects in Security & Trust (FAST2005)

Newcastle, UK, 18-19 July 2005.

FAST 2005 is affiliated with 13th Formal Methods Symposium (FM05: http://www.csr.ncl.ac.uk/fm05/) 
and under the auspices of IFIP WG 1.7 "Theoretical Foundations of Security Analysis and Design"

            -last call for papers -


The third international Workshop on Formal Aspects in Security and Trust (FAST2005) 
aims at continuing the successful efforts of the first two FAST workshops for 
fostering the cooperation among researchers in the areas of security and trust. 
The new challenges offered by the so-called ambient intelligence space as a future 
paradigm in the information society demand for a coherent framework of concepts, 
tools and methodologies to enable user's trust and confidence on the underlying 
computing infrastructure. These need to address issues relating to both guaranteeing 
security of the infrastructure and the perception of the infrastructure being secure. 
In addition, user confidence on what is happening must be enhanced by developing trust 
(Continue reading)

Alexander Gelbukh (MICAI | 3 May 02:19 2005

CFP: MICAI-2005 Artificial Intelligence, Springer LNAI: submission reminder and CFP-2

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Dear members of TYPES list,

I think the following CFP is relevant for the Types list since type theory
and logical reasoning has direct connection with Artificial Intelligence. So
I invite the member of the list to publish their papers in the Proceedings
of this conference.

Alexander Gelbukh

        MICAI 2005

        4th Mexican International Conference on 

        November 14-18, 2005
        Monterrey, Mexico


        Proceedings: Springer LNAI.
        Submission: May 29 (abstract May 22).
        Keynote speakers: see website.


*** WHAT'S NEW ***

(Continue reading)

Bernhard Gramlich | 3 May 18:45 2005

FroCoS 2005: Final cfp - extended submission deadline: May 16, 2005

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

                     [Apologies for multiple copies]


                   FroCoS 2005: FINAL CALL FOR PAPERS

          *** SUBMISSION DEADLINE (EXTENDED): May 16, 2005 ***


 5th International Workshop on Frontiers of Combining Systems (FroCoS 2005)

                 Vienna, Austria, September 19-21, 2005 




In various areas of computer science, such as logic, computation,
program development and verification, artificial intelligence, 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
(Continue reading)

Bengt Nordström | 4 May 10:37 2005

Announcement: TYPES Summer School, August 15 - 26

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Important deadlines: May 20: Grant application, June 3: registration

It is now possible to register for the course!

                    TYPES Summer School 2005

        Proofs of Programs and Formalisation of Mathematics

              August 15-26 2005, Goteborg, Sweden


During the last ten years major achievements have been made in using
computers for interactive proof developments to produce secure
software and to show interesting mathematical results. Recent major
results are, for instance, the complete formalisation of a proof of
the four colour theorem, and a formalisation of the prime number
theorem. See the following articles in The Economist and Science:


The summer school is a two weeks' course for postgraduate students, 
researchers and industrials who want to learn about interactive proof 
development. The present school follows the format of previous TYPES 
summer school (in Baastad 1993, Giens 1999, Giens 2002).  There will be 
introductory and advanced lectures on lambda calculus, type theory, 
logical frameworks, program extraction, and other topics with relevant
(Continue reading)

Carlos Areces | 6 May 15:18 2005

ESSLLI 2006 - Call for Course and Workshop Proposals

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]


  18th European Summer School in Logic, Language and Information
                           ESSLLI 2006
            31 July - 11 August, 2006, Malaga, Spain 



The European Summer School in Logic, Language and Information (ESSLLI)
is organized every year by the Association for Logic, Language and
Information (FoLLI, http://www.folli.org) in different sites around

The main focus of ESSLLI is on the interface between linguistics,
logic and computation.  ESSLLI offers foundational, introductory and
advanced courses, as well as workshops, covering a wide variety of
topics within the three areas of interest: Language and Computation,
Language and Logic, and Logic and Computation.

Previous summer schools have been highly successful, attracting up to
500 students from Europe and elsewhere.  The school has developed into
an important meeting place and forum for discussion for students and
researchers interested in the interdisciplinary study of Logic,
Language and Information. 
(Continue reading)

m.fayad | 8 May 08:23 2005

ECOOP 2005 First Workshop on Building a System Using Patterns -- Deadline extended

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Syprus List..

Sorry for multiple copies..

New deadline:  May 30, 2005.  Looking forward to your submissions.. Thank

Building Systems Using Patterns: Examine the Illustrious Claim ? Call for 
Preliminary Call for Papers
ECOOP 2005 First Workshop on
Building A System Using Patterns: Examine the Illustrious Claim
Call for Papers
ECOOP 2005 Full day workshop
The 19th European Conference on Object-Oriented Programming 
July 25-29, 2005, Glasgow, Scotland

As software increases in size and becomes more complex and costly, the 
need for techniques to ease software development is likewise increasing. 
Over the years, pattern community has evolved and received more attention 
from both academia and industry. Developing software using patterns can 
reduce cost and condense development life-cycles, while simultaneously 
maintaining the quality of the developed systems.  However, the potential 
of using patterns in developing software systems is not fully realized. 
(Continue reading)

Michael Kohlhase | 7 May 07:13 2005

MKM 2005 Final CfP

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

[Please post - apologies for multiple copies.]

                         MKM 2005

             Fourth International Conference on


          15. - 16. July 2005 (Workshops: 14. July)
                    Bremen --- Germany
           (organized by International University Bremen)

                   FINAL CALL FOR PAPERS

Mathematical Knowledge Management is a new field in the intersection
of mathematics and computer science.

We need new techniques for managing the enormous volume of
mathematical knowledge available in current mathematical sources and
making it available through the new developments in information
technology. A list of topics (to be understood as specialized to the
realm of mathematical information) comprises but is not restricted to:

Knowledge representation     Repositories of formalized mathematics
Metadata                     Deduction systems
(Continue reading)