1 Jan 2003 07:05

### Re: Classifying the cardinalities of types

```Hi David,

Here are the practical reasons:

1. Since my programming language is aimed at practical applications, I
require that all complete programs be deterministic -- in other words, any
non-determinism (multivaluedness or zerovaluedness) is limited to internal
computations, and not the observable results of running the program.  This
requires verifying that the program's type is of cardinality 1.

2. Like Ontic, I use nondeterminism to express the idea that a term has more
than one potential value.  Thus lambda(x 1|2|3|4).x+7 is a function whose
domain is the range of integers from 1-4.  This particular expression can't
reduce any further: we can't evaluate "x+7" because we don't know what value
x will take on.  However, we can reduce the function lambda(x 3).x+7 to
lambda(x 3).10, because we know that "x" can only take on the value 3.  In
general, whenever reading a function parameter, or a "recursive self-value",
I need to examine the cardinality in order to determine whether a reference
(formally, a de Bruijn index) can be released or whether it needs to remain
there in the normal-form.  This is why the potential cardinality set {0,1,m}
works well for my application: all the language rules intimiately care about
is whether a term is uninhabited, single-valued, or multivalued.  There is
no compiler logic special-cased, for example, for cardinality-2 elements.

By "recursive self-value", I mean an expression like {x 3|5|7,y x+3}.  I
represent such things as arrays with a special kind of de Bruijn index
referring back to the enclosing function, rather than its parameter.  This
turns out to be a very expressive notation, allowing object-oriented data
structures a la James Hickey's "Very Dependent Types" -- a type can not only
depend on function parameters, but also on recursive values that aren't
```
(Continue reading)

6 Jan 2003 03:09

### Call for Papers: 10th Static Analysis Symposium

```----------------------------------------------------------------------
Call for Papers

SAS '03
10th Annual International Static Analysis Symposium
June 11-13, 2003  :  San Diego, California
http://www.lix.polytechnique.fr/~radhia/sas03/index.html

Federated Computing Research Conference FCRC 2003
http://www.acm.org/sigs/conferences/fcrc/
----------------------------------------------------------------------

Static Analysis is increasingly recognized as a fundamental tool
for high performance implementations and verification systems of
programming languages.  The series of Static Analysis Symposia has served
as the primary venue for presentation of theoretical, practical, and
application advances in the area.

The 10th International Static Analysis Symposium SAS'03 will be
held at the Town and Country Resort & Conference Center in San Diego (USA)
as part of the Federated Computing Research Conference FCRC 2003.  Previous
symposia were held in Madrid, Paris, Santa Barbara, Venice, Pisa, Paris,
Aachen, Glasgow and Namur.

The technical program for SAS'03 will consist of invited lectures,
tutorials, panels, presentations of refereed papers, and software
demonstrations.  Contributions are welcome on all aspects of Static
Analysis, including, but not limited to:

abstract interpretation,   data flow analysis,
```
(Continue reading)

6 Jan 2003 16:42

### BRICS PhD grants and Marie Curie fellowships

```[Please accept our apologies if you receive this more than once]

BRICS - Basic Research in Computer Science

at the Universities of  Aarhus  and Aalborg, Denmark

This is a call for applications for:

PhD admission and PhD grants, and
Marie Curie Training Site Fellowships.

BRICS, Basic  Research in  Computer Science, is  funded by  the Danish
National  Research  Foundation.   It  comprises an  International  PhD
School with an associated Research Laboratory.

BRICS  is  based  on  a  commitment to  develop  theoretical  computer
science, covering core areas such as:

- Semantics of Computation,
- Logic,
- Algorithms and Data Structures,
- Complexity Theory,
- Data Security and Cryptology, and
- Verification,

as well as a number of spin-off activities including

- Web Technology,
- Quantum Informatics,
- Bio Informatics, and
```
(Continue reading)

7 Jan 2003 21:11

### Field's Institute Summer School in Logic & Theoretical CS (fwd)

```Dear Colleagues:

June will be theoretical computer science month at U. Ottawa! The
Field's Institute will sponsor a summer school in Logic and
Foundations of Computation at the University of Ottawa this
summer, June 2-20, 2003.  This program will be hosted by the logic
group in the Department of Mathematics and Statistics at the
University of Ottawa  (consisting of Philip Scott, Richard Blute,
and Peter Selinger).

The program will consist of 2 weeks of courses for graduate
students, then a week of workshops in several areas of
theoretical computer science.   This program is particularly aimed
at graduate students in mathematics, logic, theoretical computer
science, mathematical linguistics and related areas. The program
culminates in the 18th annual IEEE Logic in Computer Science
(LICS2003) meeting on campus at U. Ottawa.  For the latter,
see  http://www.dcs.ed.ac.uk/home/als/lics/

The details (and finances) of the Field's program are still being worked
out, but we wanted to alert our colleagues to the following themes:

Weeks 1,2:  Each week will consist of two courses (one in the
morning, the other in the afternoon), taught by experts in the
area.  We are planning topics that include:

Week 1: (a) Categorical Logic and type theory and  (b) Linear Logic.
Week 2:  (a) Game Semantics   and (b) Concurrency.
Week 3:  Workshops.  These include, among other topics,

```
(Continue reading)

8 Jan 2003 01:14

### CFP: FOAL 2003--Foundations Of Aspect-oriented Languages

```
CALL FOR PAPERS

Foundations of Aspect-Oriented Languages (FOAL)

March 17, 2003
Boston, Massachusetts
http://www.cs.iastate.edu/~leavens/FOAL/cfp-2003.html

A one-day workshop to be held in conjunction with the
Second International Conference on
Aspect-Oriented Software Development (AOSD 2003),
March 17-21, 2003, Boston, Massachusetts, USA
http://aosd.net/conference

THEMES AND GOALS

FOAL is a forum for research in foundations of aspect-oriented
programming languages. Areas of interest include but are not limited
to:

* Semantics of aspect-oriented languages
* Specification and verification for such languages
* Type systems
* Static analysis
* Theory of testing
* Theory of aspect composition
* Theory of aspect translation (compilation) and rewriting
* Applications of such theories in practice (such as language
design studies)
```
(Continue reading)

8 Jan 2003 18:43

### PLI'03 Call for Workshop Proposals

```				  PLI '03
Call for Workshop Proposals

Uppsala, Sweden
August 25-29, 2003

The 2003 colloquia on Principles, Logics, and Implementations of High-Level
Programming Languages (PLI 2003) will be held in Uppsala, Sweden, on August
25-29, 2003. PLI 2003 is a federation of colloquia that includes ICFP 2003
(the ACM SIGPLAN International Conference on Functional Programming) and
PPDP 2003 (the ACM SIGPLAN International Conference on Principles and
Practice of Declarative Programming).

Proposals for workshops are invited for consideration ofACM SIGPLAN
sponsorship and affiliation with PLI 2003. Affiliated workshops will be
held in parallel with the ICFP and PPDP colloquia. The purpose of these
workshops is to provide a platform for presenting novel ideas in a less
formal and possibly more focused way than the conferences themselves. As
such, they also offer a good opportunity for young researchers to present
their work and to obtain feedback from an interested community. The format
of each workshop is to be determined by the organizers, but it is expected
that they contain ample time for general discussion. The preference is for
one-day workshops, but other schedules will also be considered.

Researchers and practitioners are invited to submit workshop proposals to
the PLI 2003 Workshop Chair, Peter Lee (petel@...), NO LATER THAN
FEBRUARY 14, 2003. Submission may be made by e-mail (Postscript, PDF, or
ASCII) with "PLI03 Workshop Submission" in the subject header. Following
ACM SIGPLAN's sponsorship procedures, proposals must include:

```
(Continue reading)

9 Jan 2003 10:04

### Intuitionistic logic on real line

```Note: I am sending this message to the Foundations of Mathematics
list and also to the Types list, hoping that it may be interesting
to the subscribers of both.

Intuitionistic predicate logic is not complete for real topology.
----------------------------------------------------------------

It is well known that a propositional formula is an intutionistic
tautology if and only if it is true in the Heyting algebra of all
open sets of the real line (or plane). See for instance [1] or [2].
Whether the same holds for first-order logic is mentioned in [2] as
an open question. The answer to this question turns out to be negative,
as can be seen from the following simple example. To my surprise,
this fact seems to be not known, at least nobody I asked until now
was aware of the incompleteness.

Here is the example. Write (x) and (Ex), respectively, for the universal
and existential quantifiers. The formula

(*)     (x)[P(x)\/ [not P(x)]] -> (Ex)P(x) \/ (x)[not P(x)]

is true on the real line, but it is not an intuitionistic theorem.

Proof:
Denote by ~B the pseudocomplement of an open set B, and by Int(B) its
interior. Let /\ and \/ denote both finite and infinite intersections
and sums.

Lemma: Let K be an open connected set contained in the union of B and ~B.
Then K is either contained in B or in ~B.
```
(Continue reading)

13 Jan 2003 11:43

### First APPSEM-II Workshop

```+---------------------------------------------------------------------+

FIRST ANNOUNCEMENT AND CALL FOR PARTICIPATION

First APPSEM-II Workshop
26th - 28th March 2003
Nottingham, United Kingdom

The first annual workshop of  the IST working group APPSEM-II (Applied
Semantics II) will be held  at the University of Nottingham from 26-28
March 2003.  All  members of the working group  are invited to attend,
but participation of non-members  from both academia and industry with
interests  in application-oriented  programming language  semantics is
actively encouraged.   The purpose of  the workshop is to  present new
results and plan future work in each of the nine themes of the group:

A - Program structuring: OO programming, modules (Didier Remy);
B - Proof assistants, functional programming,
and dependent types (Thierry Coquand);
C - Program analysis, generation, and configuration (Neil Jones);
D - Specification and verification methods (Uday Reddy);
E - Types and type inference in programming (Fritz Henglein);
F - Games, sequentiality, and abstract machines (Pierre-Louis Curien);
G - Semantic methods for distributed computing (Glynn Winskel);
H - Resource models and web data (Peter O'Hearn, Philippa Gardner);
I - Continuous phenomena in Computer Science (Achim Jung).

For each theme there will  be a session of presentations, organised by
the theme leader (in parentheses  above).  There will also be a number
of invited presentations, an industrial panel session, a brainstorming
```
(Continue reading)

14 Jan 2003 16:41

### ETAPS 2003 - call for participation

```       **********************************************************
***                                                    ***
***                     ETAPS 2003                     ***
***         Warsaw, Poland, April, 5-13, 2003          ***
***                                                    ***
***              CALL FOR PARTICIPATION                ***
***                                                    ***
***               !!!! REGISTER NOW !!!!               ***
***                                                    ***
***           http://www.mimuw.edu.pl/etaps03/         ***
***                                                    ***
**********************************************************

**********************************************************
***                                                    ***
***                  Important Dates                   ***
***                                                    ***
***     January 31 - Grant Application Deadline        ***
***     February 5 - Discount Registration Deadline    ***
***        March 3 - Early Registration Deadline       ***
***       March 31 - End of Online Registration        ***
***                                                    ***
***               April 5-13  - ETAPS 03               ***
***                                                    ***
**********************************************************

-----------------------------------------------------------------------
5 Conferences - 15 Workshops - 7 Tutorials
-----------------------------------------------------------------------
```
(Continue reading)

17 Jan 2003 15:12

### ACM-IEEE MEMOCODE'2003 - Call for Papers

```Dear colleagues,

I would like to bring the following CFP to the attention of this mailing-list,
as topics such as behavioral   and system types or high-level system design
languages might be of interest to some readers.
Best regards,
Jean-Pierre.

______________________________________________________________________________

CONFERENCE ANNOUNCEMENT AND CALL FOR PAPERS

ACM & IEEE MEMOCODE 2003

First ACM-IEEE International Conference on Methods and Models for Codesign

Programming models, formal analysis methods and
verification  techniques  for high-level system
design:  towards  convergence of formal methods
and industrial trends.

June 24th-26th, 2003 - Mont Saint-Michel, France
______________________

CO-SPONSORS      ACM Special Interest Group on Digital Automation
IEEE Circuits and System Society
IEEE Computer Society, Digital Automation TC

in cooperation with INRIA, IRISA, Université de Rennes I

```
(Continue reading)

Gmane