headers
Cosimo Laneve | 7 Nov 2002 12:49
Picon

ICTCS'03


                   EIGHT ITALIAN CONFERENCE ON
              THEORETICAL COMPUTER SCIENCE (ICTCS'03)

               University Center, Bertinoro, Italy 
		    October, 13 -- 15, 2003

              Sponsored by the European Association
             of Theoretical Computer Science (EATCS)

The Eight Italian Conference on Theoretical Computer Science will
take place in Bologna. Papers presenting original contributions 
in any area of theoretical computer science are being sought.  

Topics include (but are not limited to):

	analysis of algorithms, automata, computability,
        computational complexity, cryptography, data types and structures,
        design of algorithms, formal languages, foundations of functional
        programming, foundations of logic programming, new computing
        paradigms, parallel and distributed computation,
        program specification, program verification, term rewriting,
        theory of concurrency, theory of data bases, theory of logical
        design and layout, theory of robotics, theory of knowledge bases,
        type theory, semantics of programming languages, security,
        symbolic and algebraic computation.

GENERAL CHAIR 
        Roberto Gorrieri, Bologna
(Continue reading)

Permalink | Reply | 0 comments |
headers
Matthew Hennessy | 11 Nov 2002 15:40
Picon
Picon

New technical report on types for mobile agents


The use of types to control the mobility of distributed agents, 
and the effect of these types on agent equivalence, should make the
following technical report of interest to subscribers to the theory
mailing list.

Available from http://www.cogs.susx.ac.uk/reports/

Title:      Towards a behavioural theory of access and mobility control
            in distributed systems
Author(s):  Matthew Hennessy, Massimo Merro, Julian Rathke
Report:     Computer Science Report 2002:01
Issued:     University of Sussex, Brighton BN1 9QH, October 2002
Abstract:   We define a typed bisimulation equivalence for the language
            Dpi, a distributed version of the pi-calculus in which
            processes may migrate between dynamically created locations.
            It takes into account resource access policies, which can be
            implemented in Dpi using a novel form of dynamic capability
            types. The equivalence, based on typed actions between
            configurations, is justified by showing that it is
            fully-abstract with respect to a natural distributed version
            of a contextual equivalence. In the second part of the paper
            we study the effect of controlling the migration of
            processes. This affects the ability to perform observations
            at specific locations, as the observer may be denied access.
            We show how the typed actions can be modified to take this
            into account, and generalise the full-abstraction result to
            this more delicate scenario.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Peter Selinger | 14 Nov 2002 03:35
Picon

paper: towards a quantum programming language

Dear Type Theorists,

my new paper, "Towards a Quantum Programming Language", is available
from my web site. In it, I describe a programming language for quantum
computation. Unlike other such languages appearing in the literature,
this one has a static type system which guarantees the absense of
run-time errors. It can handle recursive types, but not higher-order
types (yet).

The paper is self-contained and does not presuppose any knowledge of
quantum physics. As usual, comments are welcome.

-- Peter Selinger

http://quasar.mathstat.uottawa.ca/~selinger/papers.html

Abstract: The field of quantum computation suffers from a lack of
syntax. In the absence of a convenient programming language,
algorithms are frequently expressed in terms of hardware circuits or
Turing machines. Neither approach particularly encourages structured
programming or abstractions such as data types. In this paper, we
describe the syntax and semantics of a simple quantum programming
language. This language provides high-level features such as loops,
recursive procedures, and structured data types. It is statically
typed, and it has an interesting denotational semantics in terms of
complete partial orders of superoperators.
Permalink | Reply | 0 comments |
headers
Matthias Felleisen | 15 Nov 2002 04:50
Favicon

Re: semantics for F_{sub,rec} ??


Thomas, you wrote: 

"if it turns out as built on sand (in the sense that it lacks a good
semantics for the target language used in these translational
interpretations)."

Would you mind illustrating this "building on sand" portion of your
letter with, oh say, one or two practical examples? 
 - How would programmers suffer from a lack of a classical semantics?
 - How would programming language researchers suffer? 
 - What can go wrong? 

Thanks -- Matthias
Permalink | Reply | 0 comments |
headers
Martin Hofmann | 15 Nov 2002 11:39
Picon

TLCA 2003 Last call for papers

                    Sixth International Conference on

            Typed Lambda Calculi and Applications (TLCA '03)

                    Valencia, Spain, 10-12 June 2003

                   Second and Final Call for Papers
	          SUBMISSION DEADLINE 2 December 2002

TLCA is getting into shape: we now have three excellent confirmed INVITED
SPEAKERS: David McAllester, Georges Gonthier, and Ralph Loader, whose
presentations promise to make TLCA an exciting event next summer. You can
make it even more exciting by submitting a COOL PAPER on ...

... original research results that are broadly relevant to the theory and
applications of typed calculi. The following list of topics is
non-exhaustive:

    * Proof-theory: Natural deduction and sequent calculi, cut
      elimination and normalisation, linear logic and proof nets,
      type-theoretic aspects of computational complexity
    * Semantics: Denotational semantics, game semantics, realisability,
      categorical models
    * Implementation: Abstract machines, parallel execution, optimal
      reduction, type systems for program optimisation
    * Types: Subtypes, dependent types, type inference, polymorphism,
      types in theorem proving
    * Programming: Foundational aspects of functional and
      object-oriented programming, proof search and logic programming,
      connections between and combinations of functional and logic
(Continue reading)

Permalink | Reply | 0 comments |
headers
Thomas Streicher | 15 Nov 2002 15:36
Picon
Favicon

Re: semantics for F_{sub,rec} ??

> "if it turns out as built on sand (in the sense that it lacks a good
> semantics for the target language used in these translational
> interpretations)."
> 
> Would you mind illustrating this "building on sand" portion of your
> letter with, oh say, one or two practical examples? 
>  - How would programmers suffer from a lack of a classical semantics?
>  - How would programming language researchers suffer? 
>  - What can go wrong? 

what I meant was that it POTENTIALLY builds on sand as the target language
of the translation hasn't a much clearer semantics then the source language;
in particular, the FOOL book uses as target language a higher order 
polymorphic lambda calculus with subtyping, recursion and STATE; this latter
aspect hasn't been investigated at all; what comes to my mind is the vague
possibility of using computational monads (in this case the state monad) but
it isn't evident that one can build models of this calulus using the Kleisli
category on PERs for the state monad

another problem I have with the target language is that the recursive types
are not initial/terminal algebras for some functor; such a desire is not
pure categorical fetishism because being an initial/terminal solution gives
rise to reasoning principles as in Paulson's book, namely that the least 
endomorphism of the solution is identity; this gives rise to Pitts' Theorem
from 1996 which Bernhard Reus and I have used for proving unique existence of
Object Specifications `a la Abadi and Leino 
(http://www.cogs.susx.ac.uk/users/bernhard/lics02.ps).

I mean in a sense that situation w.r.t. this translational semantics is a bit
like denotational semantics of Strachey before Scott interfered and provided
(Continue reading)

Permalink | Reply | 1 comment |
headers
dalzilio | 15 Nov 2002 16:58
Picon

Paper announcement: on tree automata for XML Schema validation


Dear all, 

We would like to announce the following research report:

"XML Schema, Tree Logic and Sheaves Automata."
By Silvano Dal-Zilio and Denis Lugiez.

Some recent works have studied statically typed languages for XML
processing based on Document Type Definition (DTD), a simple standard
for defining documents validity. In this context, several algorithms are
based on regular tree automata. 

This paper is concerned with an extension of tree automata tailored to
the manipulation of XML Schema, a more advanced standard. The paper is
available from: http://www.cmi.univ-mrs.fr/~dalzilio/RR-4631.ps

Regards,

Silvano Dal-Zilio
Denis Lugiez

---------

Abstract:

We describe a new class of tree automata and a related logic on trees,
with applications to the processing of XML documents and XML schemas.

XML documents, and other forms of semi-structured data, may be roughly
(Continue reading)

Permalink | Reply | 0 comments |
headers
Matthias Felleisen | 15 Nov 2002 17:19
Favicon

the point of (any) semantics, was Re: semantics for F_{sub,rec} ??


Everyone -- I should clarify my reaction and my response to Thomas. 

1. I have done my share of semantics. 
2. I am doing my share of systems building. 
3. And I really wish that I could say 1 and 2 are related. 
   Naturally I understand that my students all share the 
   "cultural heritage" of my 'semantics phase.' But clearly 
   there should be more and if there is more, we can hopefully 
   bring semantics closer to others. 

So, I am calling on people to collect a bunch of examples with the
following characteristics: 

  - people make a claim about a language 
  - people later find that this is not true 
  - by adjusting the implementation to the language, we help programmers 
    develop, debug, and maintain their programs more easily and indeed, 
    prevent latent explosions. 

Example: I volunteer one of my own publications as an example. Some of 
you may be aware of my paper with Andrew Wright, which uses my 'evaluation
context semantics' to prove type soundness/safety for a series of ML-ish
languages. 

The last of the languages is the polymorphic ML core with call/cc. At the
time, plain polymorphic callcc had been added to SML/1e and people thought
'it worked.' Naturally our proof showed that it worked. We turned it into
a tech report and submitted it to Info and Control.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Dan Grossman | 16 Nov 2002 19:33
Picon
Favicon

Re: the point of (any) semantics, was Re: semantics for F_{sub,rec} ??


For some reason I've begun collecting interactions between type 
variables and effects that have the characteristics listed below.  (Is 
this really any stranger than a stamp collection? :-))  Granted, this is 
a very narrow response to Matthias' call -- surely semantics is useful 
for more than "assignment statements and alphas".

A brief introduction to my collection:
* ML + call/cc (Wright/Felleisen/Lillibridge/Harper)
* Polymorphic fields in OCaml 3.05 (Leroy/Prevost, July 2002)
    -- see OCaml mailing list
* Existential types in Cyclone (April 2002)
   [Yes, I am 'guilty' too.  I just was lucky enough to discover my 
mistake before somebody else did.]
    -- see ESOP2002
* Generic Java type inference (Jeffrey, December 2001)
    -- see Types List
* Breaking parametricity in ML (Pierce/Sangiorgi, 1997)
   [Not an unsoundness, but a surprising result nonetheless]
    -- see JACM2000

This collection makes it possible to make provocative rants.  For example:
(1) Language designers not familiar with this collection will continue 
to make false claims about polymorphic languages.
(2) Alas, language designers familiar with this collection will continue 
to make false claims about polymorphic languages.

--Dan

Matthias Felleisen wrote:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Chet Murthy | 17 Nov 2002 06:34
Picon
Favicon

Re: the point of (any) semantics, was Re: semantics for F_{sub,rec} ??


I thought I'd add a few things to the "provocative rant" category.

(0) I'm a reformed type theorist, and I believed all the gospel, just
like everybody else on this list.  Since that time, I've moved into
the industrial application of programming language technology, in a
sense that can only be summarized as "as real as it gets".

And yet, I've found that languages like Perl are critical tools, and
for good reasons that people on this list would appreciate.  It isn't
all dross over in the land of programming language research and
semantics.

[Bluntly put, it took Larry Wall (a SYSTEMS ADMINSTRATOR) to convince
the world of the value of CommonLisp.  Think about it.  Think hard
about it.  'cos it is true, and a really disappointing statement about
the entire programming-language community.]

I've even found uses for ML -- real uses for ML, where I can make
money, and we're talking enterprise transaction-processing money, not
NSF grant money.

(1) Examples of problems arising in languages like ML, or in cute
theoretical ideas like "Generic Java" are uninteresting and
unconvincing to the Great Unwashed.

(2) When arguing that some example is a proof of the value of a
particular brand of semantics, it is IMPORTANT to validate that the
example could not be done more easily in some OTHER brand of
semantics.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane