headers
blute | 2 Apr 2002 14:39
Picon
Favicon

Re: CTCS-Final CFP and deadline extension

We have received a number of requests for a further extension of
our deadline, so we have pushed it back to April 19th. Sorry for
generating so much email.

cheers,
Rick Blute
Program Committee Chair

+++++++++++++++++++++++++++++++++++

            CATEGORY THEORY AND COMPUTER SCIENCE (CTCS'02)
                          AUGUST 15-17, 2002

                    GRADUATE STUDENT PRECONFERENCE
                          AUGUST 12-14, 2002

                         University of Ottawa
                       Ottawa, Ontario, Canada

                        FINAL CALL FOR PAPERS

CTCS '02 is the 9th Conference on Category Theory and Computer
Science. The purpose of the conference series is the advancement of
the foundations of computing using the tools of category theory.  The
emphasis is upon applications of category theory, but it is recognized
that the area is highly interdisciplinary.

Typical topics of interest include, but are not limited to,
category-theoretic aspects of the following:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Delia Kesner | 3 Apr 2002 11:26
Picon

workshop on higher-order rewriting 2002 call for abstracts

     The First International Workshop on Higher-Order Rewriting

                July 21st, 2002, Copenhagen, Denmark 

                   Held in conjunction with FLOC'02

                    http://www.lri.fr/~kesner/hor/

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

Purpose: 

The aim of HOR is to provide an informal setting to discuss recent work and
work in progress concerning higher-order rewriting.

Scope:

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

* Applications

  proof checking, 
  theorem proving, 
  declarative programming, 
  program transformation.

* Foundations

  pattern matching,
  unification,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Dr. Gopal Gupta | 5 Apr 2002 03:27

CALL FOR PROPOSALS FOR ORGANIZING ICLP'03


          CALL FOR PROPOSALS FOR ORGANIZING ICLP'03

The Association for Logic Programming (ALP) invites proposals for
organizing the 19th International Conference on Logic Programming
(ICLP) in the year 2003.

The ICLP is ALP's and the logic programming communities' flagship
conference where most recent advancements in logic programming are
presented. The conference is attended by researchers interested in
logic programming, constraint programming, programming languages, AI
and other affiliated fields. The last few ICLPs were held in:
Copenhagen (2002), Paphos/Cyprus (2001), London (2000), Las Cruces/NM
(1999).

If you are interested in organizing ICLP'03, please get in touch with
me asap.  More details of what is entailed in proposing to organize an
ICLP can be found in ALP's website:

              http://www.cwi.nl/projects/alp/ 

(click on "ALP policy" button at the bottom of the index bar).

Gopal Gupta (gupta@...)
ALP Conference Coordinator
Permalink | Reply | 0 comments |
headers
Rafael Morales | 5 Apr 2002 11:55
Picon

Schedule of ICALP 2002

The URL of the ICALP2002 schedule in static version is:

  http://sirius.lcc.uma.es/ICALP2002/PreliminarySchedule.html

and the dynamic version in:

  http://www.lcc.uma.es/ICALP2002, and then "Schedule" button.

Best regards,
--
Rafael Morales

Visit the Web pages of:
    ICALP'2002 conference http://www.lcc.uma.es/ICALP2002
    and AH'2002 conference http://www.lcc.uma.es/AH2002
Permalink | Reply | 0 comments |
headers
Workshop on Types in Programming | 5 Apr 2002 16:06
Picon
Favicon

CFP: TIP'02 Workshop on Types in Programming

[ NEWS: ENTCS issue planned for proceedings ]

			Final Call for Papers
	      Workshop on Types in Programming (TIP'02)
		   Dagstuhl, Germany, July 9, 2002
			Colocated with MPC'02
	http://www.informatik.uni-freiburg.de/~thiemann/tip02/

Modern programming languages rely on type systems with static type
checking to detect common errors at compile time. While the benefits
of statically checked type systems have long been recognized, there
are some areas where the type systems of modern programming languages
are not expressive enough. Some interesting programs will always be
rejected, despite their semantical soundness.

There are several remedies to this situation, ranging from dependent
types (where types may contain values) through intersection types to
types with modalities. These systems are well-investigated from a
theoretical point of view by logicians and type theorists. However,
the impact of these developments on practical programming has been
small, partly because they are trading simplicity against
expressivity.

The objective of the workshop is to make researchers in programming
languages aware of new developments and research directions on the
theory side while at the same time pointing out problems arising in
practical uses to theorists.  Technical topics include, but are not
limited to:

* Type systems in all variants: polymorphic, dependent, intersection,
(Continue reading)

Permalink | Reply | 0 comments |
headers
nipkow | 8 Apr 2002 10:44
Picon
Favicon

New book: Isabelle/HOL Tutorial

- YOU ALWAYS WANTED TO TRY AN INTERACTIVE THEOREM PROVER,
  but they looked so complicated.

- YOU ARE ALREADY USING ONE,
  but the documentation ...

LOOK NO FURTHER!

We are pleased to announce the publication of the Isabelle/HOL tutorial

  Isabelle/HOL: A Proof Assistant for Higher-Order Logic
  by Tobias Nipkow, Lawrence C. Paulson and Markus Wenzel
  Springer LNCS 2283

This book is a self-contained introduction to interactive proof in
higher-order logic (HOL), using the proof assistant Isabelle2002. It is a
tutorial for potential users rather than a monograph for researchers.

For more information (and online access!), please visit

    http://www.in.tum.de/~nipkow/LNCS2283/

Enjoy,

Tobias Nipkow
Larry Paulson
Markus Wenzel
Permalink | Reply | 0 comments |
headers
Clemens Szyperski | 8 Apr 2002 23:06
Picon
Favicon

RE: Component Pascal type system is unsound

Late update on this one: the hole was closed almost
immediately after Fergus discovered it - by requiring
invariance on OUT parameters.

This is one of the humbling experiences where you are
reminded that soundness proofs are actually useful ;-)

- Clemens

> -----Original Message-----
> From: Fergus Henderson [mailto:fjh@...] 
> Sent: Thursday, December 27, 2001 7:49 AM
> To: Types List
> Subject: Component Pascal type system is unsound
> 
> 
> [----- The Types Forum, 
> http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> While we're on the topic of languages with unsound type 
> systems, let me mention another one: Component Pascal. 
> <http://www.oberon.ch/docu/language_report.html>.
> 
> According to www.oberon.ch, Component Pascal is a refined 
> version of Pascal, Modula-2, and Oberon, and moreover it is 
> advertised as being "type-safe".
> 
> However, in July this year, in response to some mail from 
> John Gough, I constructed an example which demonstrates a 
> hole in Component Pascal's type checking.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Ian Miguel | 9 Apr 2002 17:15
Picon

Doctoral Programme of CP-2002: Call for Applications

    Doctoral Programme  of the Eighth International Conference on
     Principles and Practice of Constraint Programming (CP-2002)

            www.math.unipd.it/~frossi/cp2002-doctoral.html

                         September 7-13, 2002
                          Cornell University
                           Ithaca, NY, USA

  ==================================================================
                        CALL FOR APPLICATIONS
  ==================================================================

CP-2002 invites students to  apply for the CP-2002 Doctoral Programme,
which will  provide an opportunity for  a group of  Ph.D.  students to
discuss  and explore  their research  interests and  career objectives
with a panel of established researchers in Constraint Programming.

The   CP-2002 doctoral  programme  has  the  following objectives:  to
provide  a  setting  for  mutual  feedback  on  participants'  current
research  and guidance  on future  research directions;  to  develop a
supportive  community  of  scholars  and  a  spirit  of  collaborative
research; to support a  new generation of researchers with information
and  advice  on academic,  research,  industrial, and  non-traditional
career  paths;   to  contribute   to  the  conference   goals  through
interaction  with other  researchers and  participation  in conference
events.

Program:  The program  will  consists of  students' presentations  and
tutorials given by senior researchers of the field.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Summer School on Foundations of Internet Security | 10 Apr 2002 17:18
Picon
Picon

Summer School on Foundations of Internet Security


                       CALL FOR PARTICIPATION

                 ACM  State-of-the-Art Summer School 
                 on Foundations of Internet Security
                          June 14-23, 2002
                       Duszniki Zdroj, Poland
                  http://www.ii.uni.wroc.pl/school/

Organized by
  Institute of Computer Science, University of Wroclaw, Poland
with support of 
  Association for Computing Machinery, 
  Office of Naval Research International Field Office and 
  Microsoft Research
  AXIT Poland

			  BASIC INFORMATION

The goal of the meeting is to bring state-of-the art knowledge on the
theory and tools that can be applied to enhance the security of the
Internet.

The programme of the school includes cryptography, design of secure
(cryptographic) network protocols, crypto protocol verification,
intrusion detection, security of distributed computing, and security
of mobile code, including proof carrying code and byte-code
verification. The focus of the school is intentionally broad so that
students can acquire, not only information about particular topics
they may be interested in working on, but awareness of security in all
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jud Wolfskill | 11 Apr 2002 20:12
Picon
Favicon

book announcement--Bruce

Readers of the Types Forum might be interested in this book.  For more
information, please visit  http://mitpress.mit.edu/026202523X/

Foundations of Object-Oriented Languages
Types and Semantics
Kim B. Bruce

In recent years, object-oriented programming has emerged as the dominant 
computer programming style, and object-oriented languages such as C++ and 
Java enjoy wide use in academia and industry. This text explores the formal 
underpinnings of object-oriented languages to help the reader understand the 
fundamental concepts of these languages and the design decisions behind them.

The text begins by analyzing existing object-oriented languages, paying 
special attention to their type systems and impediments to expressiveness. It 
then examines two key features: subtypes and subclasses. After a brief 
introduction to the lambda calculus, it presents a prototypical 
object-oriented language, SOOL, with a simple type system similar to those of 
class-based object-oriented languages in common use. The text offers proof 
that the type system is sound by showing that the semantics preserves typing 
information. It concludes with a discussion of desirable features, such as 
parametric polymorphism and a MyType construct, that are not yet included in 
most statically typed object-oriented languages.

Kim B. Bruce is Frederick Latimer Wells Professor of Computer Science at 
Williams College.

8 x 9, 376 pp., 100 illus, cloth, ISBN 0-262-02523-X

______________________
(Continue reading)

Permalink | Reply | 0 comments |

Gmane