3 Mar 2000 09:34

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

ANNOUNCEMENT AND CALL FOR PAPERS

The Haskell Workshop forms part of the PLI 2000 colloquium on
Principles, Logics, and Implementations of high-level programming
languages, which comprises the ICFP and PPDP conferences, together
with associated workshops.  Previous Haskell Workshops have been
held in La Jolla (1995), Amsterdam (1997), and Paris (1999).

www.cs.nott.ac.uk/~gmh/hw00.{html,ps,txt}

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

SCOPE

The purpose of the Haskell Workshop is to discuss experience with Haskell,
and possible future developments for the language.  The scope of the
workshop includes all aspects of the design, semantics, theory, application,
implementation, and teaching of Haskell.  Submissions that discuss
limitations of Haskell at present and/or propose new ideas for future
versions of Haskell are particularly encouraged.

SUBMISSION DETAILS

Deadline for submission:      1st June 2000


3 Mar 2000 12:47

### Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover

Dear all,

I would like to draw your attention to the following preprint
available from http://www.dcs.ed.ac.uk/home/fhlt/Research/

Comments and suggestions are very welcome!

Yours faithfully,

Francis.

Implementing a Program Logic of Objects in a Higher-Order Logic Theorem
Prover

by Martin Hofmann and Francis Tang

We present an implementation of a program logic of objects, extending that
of Abadi and Leino. In particular, the implementation uses higher-order
abstract syntax (HOAS) and---unlike previous approaches using HOAS---at
the same time uses the built-in higher-order logic of the theorem prover
to formulate specifications. We give examples of verifications that have
been attempted with the implementation. Due to the mixing of HOAS and
built-in logic the soundness of the encoding is nontrivial and is
established by way of a semantic interpretation based on ideas from
category theory. The details of this interpretation will be given
elsewhere.

--
Francis Tang                       Email: francis.tang@...
LFCS, Division of Informatics,     Url: http://www.dcs.ed.ac.uk/~fhlt/


3 Mar 2000 16:26

### 7th WoLLIC'2000

                         Call for Contributions

7th Workshop on Logic, Language, Information and Computation
(WoLLIC'2000)
August 15-18, 2000

!  TUTORIALS   >>     (Tutorial Day: August 15th)       <<   TUTORIALS !

Natal, Brazil

The "7th Workshop on Logic, Language, Information and Computation"
(WoLLIC'2000), the seventh version of a series of workshops which started
in 1994 with the aim of fostering interdisciplinary research in pure and
applied logic, will be held in Natal, Brazil, from August 15th to 18th 2000.
Contributions are invited in the form of short papers (10 A4 10pt pages) in
all areas related to logic, language, information and computation, including:
pure logical systems, proof theory, model theory, algebraic logic, type theory,
category theory, constructive mathematics, lambda and combinatorial calculi,
program logic and program semantics, logics and models of concurrency,
logic and complexity theory, nonclassical logics, nonmonotonic logic,
logic and language, discourse representation, logic and artificial
intelligence, automated deduction, foundations of logic programming,
logic and computation, and logic engineering.

The 7th WoLLIC'2000 has the scientific sponsorship of the Association
for Symbolic Logic (ASL), the Interest Group in Pure and Applied Logics
(IGPL), the European Association for Logic, Language and Information (FoLLI),
de Logica (SBL).



3 Mar 2000 23:58

### Paper Announcement: Secure Information Flow as Typed Process Behaviour

We are pleased to announce the following paper:

Secure Information Flow as Typed Process Behaviour

by
Kohei Honda    Vasco Vasconcelos   Nobuko Yoshida

* Long version: - Queen Mary and Westfield College, CS Technical Paper 767
- University of Leicester, MCS Technical Paper, 1/2000
* Short version: a revised version will appear in ESOP 2000, LNCS, Springer

are available from:

http://www.dcs.qmw.ac.uk/~kohei              (Queen Mary and Westfield College)
http://www.di.fc.ul.pt/~vv/publications.html (Lisbon University)
http://www.mcs.le.ac.uk/~nyoshida/paper.html (Leicester University)

Kohei Honda:       Queen Mary and Westfield College,  kohei@...
Vasco Vasconcelos: University of Lisbon,              vv@...
Nobuko Yoshida:    University of Leicester,           ny11@...

----------------------------- ABSTRACT ------------------------------
We propose a new type discipline for the $\pi$-calculus in which
secure information flow is guaranteed by static type checking.
Secrecy levels are assigned to channels and are controlled by
subtyping.  A behavioural notion of types capturing causality of
actions plays an essential role for ensuring safe information flow in
diverse interactive behaviours, making the calculus powerful enough to


6 Mar 2000 18:41

### ETAPS 2000 - 2nd Call for Participation

(Sorry, if you receive multiple copies of this Call.
Doris Faehndrich)
------------------------------------------------------------------
ETAPS 2000 - EUROPEAN JOINT CONFERENCES ON
THEORY AND PRACTICE OF SOFTWARE

Technical University of Berlin, March 25 - April 2, 2000

-------- CALL FOR PARTICIPATION ----- REMINDER -------------------

Welcome to Berlin, welcome to ETAPS, the European Joint Conferences on
Theory and Practice of Software, the European forum for academic and
industrial researchers working on these topics!

For 9 days you will be able to choose between
5 conferences -TACAS 2000, FOSSACS 2000, FASE 2000, ESOP 2000,
CC 2000 - with more than 120 regular papers and tool
demonstrations  covering a wide range of topics from theory
and practice,
7 invited lectures by Abbas Edalat, David Harel, Martin Odersky,
Richard M. Soley, Wlayslaw M. Turski, Reinhard Wilhelm, Pierre
Wolper,
5 satellite events - GRATRA 2000, CMCS 2000, CBS 2000, INT 2000,
CoFi 2000 -,
10 tutorials - XML for Software Engineers, A tutorial on Maude,
Rigorous Requirements for Safety-Critical Systems: Fundamentals
and Applications of the SCR Method, Multi-Paradigm Programming,
Query-based Automated Debugging, The Unified Modelling Language,
Swinging Types, Tables and computation, SDL 2000, Software
Metrology Basis -


6 Mar 2000 19:52

### MetaML release Version 1.0

The Pacific Software Research Center at the Oregon Graduate Institute
is proud to announce the first public release of MetaML. For more
http://www.cse.ogi.edu/PacSoft/projects/metaml/index.html

MetaML is a meta-programming system designed to make the
construction of meta-programs such as program generators safe and
easy. In a meta-programming system meta-programs manipulate
object-programs. Meta-programs may construct object-programs,
combine object-program fragments into larger object-programs,
observe the structure and other properties of object-programs, and
execute object-programs to obtain their values.

In addition to these operational properties, a meta-programming
system should also have a good human-system interface. MetaML
provides the following benefits:

1) It is easy to construct code using pattern-based object-code
templates. Templates  look like the object language they represent.

2) Program fragments are easy to combine into larger program
fragments, this is accomplished by a parameterizable splicing
mechanism analogous to a "template-with-holes".

3) Object-code has a parametric type, i.e., there is code with type
Int, code with type Float, etc. Type correctness of the
meta-program, guarantees type correctness of the object-programs it
constructs.



8 Mar 2000 10:56

### International Summer School on Computational Logic

       F I R S T   C A L L   F O R    P A R T I C I P A T I O N

~~~~~~~~~~~~~~~~~~~~~~

International Summer School on Computational Logic
ISCL 2000

Maratea (Italy), September 3-8
http://www.cs.unimaas.nl/~etalle/school2000/index.html

AIM

The school is addressed to young researchers and PhD students, as well
as to university and industry researchers. Its main goal is to give
the participants an insight of some relevant research lines in
Computational Logic.

PROGRAMME

The school consists of six lectures on different topics, including
theoretical foundations and practical perspectives. Each lecture
covers one topic from basic notions to more advanced issues.  PhD
students may ask to have a proficiency final exam at the end of the
school.  The lecturers and the topics are the following:

- Moreno Falaschi (University of Udine, Italy). Optimization of
declarative languages.

- Thom Fruehwirth (LMU Munich, Germany). Constraint Programming.



9 Mar 2000 01:55

### CP2000: Final Call for Papers [NEW SUBMISSION DATES]


[ Benjamin C. Pierce asked me to write a short prolog underlining the ]
[ relevance of CP2000 for TYPES readers. Although not being an expert ]
[ in this area, here my 10 cents.                                     ]
[                                                                     ]
[       Martin Henz                                                   ]
[       Publicity Chair, CP2000                                       ]

Constraint-based formalisms have been proved useful for several kinds
of type inference and type checking methods. Examples include the
use of constraints for simpler reformulations of classical type inference
methods such as Hindley-Milner-style polymorphic type inference, mode
analysis for concurrent logic programming, binding time analysis in logic
programming etc. The conference CP2000 invites submissions on typing that
use constraint-based or constraint-related methods.

[It is my standard policy to request such prologs for announcements of
events that are not self-evidently relevant to Types.  This turns out
to have two good effects: the posters of most announcements never
respond to my request, and the ones that do always add useful
information.  Thanks, Martin!  -- BCP]

Sixth International Conference on
Principles and Practice of Constraint Programming

September 18-22, 2000, Singapore

http://www.comp.nus.edu.sg/~cp2000

CALL FOR PAPERS


9 Mar 2000 13:19

### MFCS 2000 - Submission Deadline Approaching

      Please note that the submission deadline is MARCH 24, 2000.

**************************************************************************
MFCS 2000

25th International Symposium on
Mathematical Foundations of Computer Science

August 28 - September 1, 2000
Bratislava, Slovak Republic, Europe

http://www.mfcs.sk/

**************************************************************************
CALL FOR PAPERS
**************************************************************************

The series of MFCS symposia, organized alternately in the Czech Republic,
Poland and Slovakia since 1972, has a long and well-established tradition.
The MFCS symposia encourage high-quality research in all branches of
theoretical computer science. Their broad scope provides an opportunity to
bring together specialists who do not usually meet at specialized
conferences. Papers presenting original research on theoretical aspects of
computer science are solicited.

Principal topics of interest include (but are not limited to): design and
analysis of algorithms (sequential, parallel, distributed, approximation,
computational biology, computational geometry, graph, network, on-line,
optimisation) and data structures, algorithmic learning theory, automata,
grammars and formal languages, structural and computational complexity,


9 Mar 2000 15:22

### Postdoctoral Research Associate


POSTDOCTORAL RESEARCH ASSOCIATE

Department of Computer Science
Carnegie Mellon University

The Fox project on Advanced Language Technology for Extensible Systems
under the direction of Robert Harper, Peter Lee, and Frank Pfenning is
looking for a postdoctoral researcher.  Applicants should have
background and interests in one or more of the following areas:

- design and implementation of ML and related languages
- advanced type systems, proof-carrying code and certifying compilation
- embedded systems, network software and safety infrastructure

The ideal candidate will have credentials in system building and a
lively interest in language theory.  Participation in teaching
activities is also encouraged.  The appointment is initially for one
year with a potential renewal for a second year.  Salary is negotiable
and commensurate with experience.

The Fox project is working to demonstrate the viability and benefits of
advanced languages for programming real-world systems, with an emphasis
on networking, mobile code, and related safety and efficiency problems.