ian a. mason | 1 May 03:25 2001

Mechanical Verification of a Context Lemma


We are very pleased to announce the completion of a mechanically
verified proof of recent result in operational semantics, using SRI's
PVS system.  The result is a context lemma for a general class of
programming languages, and goes by the name of the "CIU lemma".  The
proof uses the "annotated holes" technique developed in [1] to prove
the original version of the CIU lemma. The actual version of the lemma
we prove is much more general than [1], and follows the development of
[2]. An paper describing the result, and the proof development, can be
found at [3], and the actual machine proof at [4], in the form of a
PVS dump file. The development of the proof uncovered several small
gaps in the presentation given in [2].

The actual proof of CIU in PVS involves the proving over one thousand
distinct facts.  It takes PVS 9248 seconds (154 minutes) of
CPU time running on a Linux machine configured with 2GBytes of main
memory and 4 550 MHz Xeon PIII processors.  The dump file containing
all the PVS definitions, facts, and proofs is 17 MBytes and is
available from [4]

[1] Mason, I. A. and Talcott, C. L.,
Equivalence in Functional Languages with Effects,
Journal of Functional Programming, Vol 1, pp 287-327, 1991.
Available as postscript from 

[2] Talcott, C.,
Reasoning about Functions with Effects,
in "Higher Order Operational Techniques in Semantics",
(Continue reading)

David Benson | 2 May 01:14 2001

Foundational Methods in Computer Science Workshop (FMCS'01)


                          Workshop on
              Foundational Methods in Computer Science
               --  a series of informal workshops on
              categories and logic in computer science

                FMCS'01 : May 31 -- June 3, 2001
                      Spokane, Washington

                with sponsorship from the
                School of Electrical Engineering and Computer Science
                Washington State University

                May 31: Arrival day
                        -- Reception in the evening, 7-10pm PDT
                June 1: Tutorial Talks
                June 2: Research Talks
                        Conference Banquet
                June 3: Research Talks in the morning
                        Noon -- end of workshop
                [includes talks by John MacDonald, Robin Cockett, Ernie Manes, Paul Gilmore,
                 and tutorials by Ernie Manes and Phil Mulry]

        WestCoast River Inn  (509) 326-5577
                             (800) 325-4000
        State you are with the FMCS conference
        to obtain the lower conference rate of $US73 per night.
(Continue reading)

John Hughes | 2 May 13:29 2001

Erlang workshop

(apologies if you receive more than one copy of this).

Call for abstracts to the

Erlang Workshop

Firenze, September 2, 2001, in connection with PLI2001 
(Principles, Logics, and Implementations of high-level 
programming languages).


Contributions are invited on experience with and 
applications of Erlang, critiques and proposals for 
extensions, design methods and structuring principles 
for large functional systems, implementation techniques, 
programming tools, verification methods, etc.

Submitted abstracts should be 2-12 pages, and will be 
judged on the potential for an interesting presentation.
Abstracts should in text, postscript or PDF format and
sent to workshop@... by May 15, 2001. 
Authors will be notified of acceptance by June 15, 2001.

Authors of accepted abstracts are welcome to submit 
full papers or additional accompanying materials for 
inclusion in the informal proceedings by August 15, 2001.

Home page of the Erlang workshop

(Continue reading)

Joseph Vanderwaart | 3 May 19:33 2001

Paper Announcement: An Expressive, Scalable Type Theory for Certified Code

We would like to announce the availability of the following paper at:
	http://www.cs.cmu.edu/~crary/papers/  or

Comments or suggestions are always welcome.

-- Karl Crary and Joseph Vanderwaart

An Expressive, Scalable Type Theory for Certified Code
Karl Crary and Joseph C. Vanderwaart

We present the type theory LTT, intended to form a basis for typed
target languages, providing an internal notion of logical proposition
and proof.  The inclusion of explicit proofs allows the type system to
guarantee properties that would otherwise be incompatible with
decidable type checking.  LTT also provides linear facilities for
tracking ephemeral properties that hold only for certain program

Our type theory allows for re-use of typechecking software by casting
a variety of type systems within a single language.  We provide
additional re-use with a framework for modular development of
operational semantics.  This framework allows independent type systems
and their operational semantics to be joined together, automatically
inheriting the type safety properties of those individual systems.

Roy L. Crole | 4 May 18:49 2001

MERLIN Call for Participation

                       CALL FOR PARTICIPATION

                             Workshop on

     MEchanized Reasoning about Languages with variable bINding

                            (MERLIN 2001)  

    Siena, Italy, June 18-19, 2001 in connection with IJCAR 2001

                  * http://www.mcs.le.ac.uk/merlin *
              **** Early registration: May 15, 2001 ****

Currently, there is considerable interest in the use of computers to
encode (operational) semantic descriptions of programming
languages. Such encodings are often done within the metalanguage of a
theorem prover or related system. The encodings may require the use of
variable binding constructs, inductive definitions, coinductive
definitions, and associated schemes of (co)recursion.

The aim of this workshop is to provide researchers with a forum to
review state of the art results and techniques, and to present recent
and new progress in the areas of:

  + The automation of the metatheory of programming languages,
particularly work which involves variable binding.
(Continue reading)

Derek R. Dreyer | 4 May 20:41 2001

paper on recursive modules

We would like to (belatedly) announce the availability of the following TR at


Comments and suggestions would be greatly appreciated.

-- Derek R. Dreyer, Robert Harper, and Karl Crary

Toward a Practical Type Theory for Recursive Modules

Derek R. Dreyer, Robert Harper, and Karl Crary

March 2001


Module systems for languages with complex type systems, such as
Standard ML, often lack the ability to express mutually recursive type
and function dependencies across module boundaries.  Previous work by
Crary, Harper and Puri set out a type-theoretic foundation for
recursive modules in the context of a phase-distinction calculus for
higher-order modules.  Two constructs were introduced for encoding
recursive modules: a fixed-point module and a recursively dependent
signature.  Unfortunately, the implementations of both constructs
involve the use of equi-recursive type constructors at higher-order
kinds, the equivalence of which is not known to be decidable.

In this paper, we show that the practicality of recursive modules is
(Continue reading)

Bernhard Gramlich | 7 May 19:55 2001

STRATEGIES 2001 (call for participation, prelim. program)


  4th International Workshop on Strategies in Automated Deduction
                         (STRATEGIES 2001)

                www: http://www.logic.at/strategies01/

      Siena, Italy, June 18, 2001, in connection with IJCAR 2001 


Strategies are almost ubiquitous in automated deduction and reasoning  
systems, yet only recently have they been studied in their own
right. The workshop aims at making progress towards a deeper
understanding of the nature of strategies and search plans, their
description, properties, and usage, especially, but not exclusively,
in theorem proving and model building. It provides a common forum for
researchers working on all aspects of strategies, under different
terminologies and in various domains.

Topics of interest for the workshop include all aspects related to
strategies in automated deduction. The emphasis of this year's 
workshop will be on 

- theory and analysis of strategies (e.g., formal approaches for
  abstract representation and comparison of theorem proving strategies
  and their behavior, terminological foundations),
- strategies in (existing) theorem proving systems (e.g.,
(Continue reading)

Brian Postow | 7 May 23:34 2001

Survey of object oriented models of computation

I'm not sure if this is the right place to ask this question, if it
is'nt, I'm sure someone here will tell me what is. I'm looking for a
comprehensive survey of object oriented models of computation, along
the lines of Bruce/Cardelli/Pierce's "Comparing Object Encodings", but
more complete, or perhaps just more recent. I need to write a brief
introduction, and I want to make sure that I don't leave out any
important papers.

Thank you all

Brian Postow

[ I don't know of any comprehensive survey.  A couple of other
references that come to mind besides the ones in the BCP paper are
Castagna/Ghelli/Longo's lambda-& calculus and any number of
"core-Java" calculi, e.g. Featherweight Java.  If you're also
interested in concurrent object models, then there are a whole bunch
more systems to add to the list.  --BCP ]

Ralf Treinen | 9 May 11:15 2001

UNIF 2001: Call for Participation

                     1st Call for Participation
                              UNIF 2001
               15th International Workshop on Unification
                           June 18-19, 2001
                            Siena,  Italy
                          Part of IJCAR 2001

UNIF is the main international meeting on unification. Unification is
concerned with the problem of identifying given terms, either
syntactically or modulo a given logical theory. Syntactic unification
is the basic operation of most automated reasoning systems, and
unification modulo theories can be used, for instance, to build in
special equational theories into theorem provers.

The main purpose of UNIF is to bring together people interested in
unification, present recent (even unfinished) work, and discuss new
ideas and trends in unification and related fields. In particular, it
is intended to offer a good opportunity for young researchers and
researchers working in related areas to get an overview of the current
state of the art in unification theory and get in contact with the
experts in the field.

The meeting will include short (15 minute) and long (30 minute) talks,
invited talks, and social time to discuss current topics of interest,
which include (but are not limited to):

   o  General E-unification and Calculi 
   o  Special Unification Algorithms
   o  Matching 
(Continue reading)

Alan Wood | 15 May 12:29 2001

CFP - Coordination 2002

                       C O O R D I N A T I O N   2 0 0 2
                               8-11 April 2002


                         Fifth International Conference

                       Coordination Models and Languages

                         C a l l   f o r   P a p e r s

We invite your paper submissions to the fifth in the series of Coordination
conferences, which  will be held in York (UK) on the 8-11 April 2002.

Full details are available at:


or by email from: wood@...

Important dates:
               Full Paper Submissions:       9 Nov. 2001
               Notification of acceptances: 14 Jan. 2002
               Camera-ready version:         1 Feb. 2002
(Continue reading)