headers
ian a. mason | 1 May 2001 03:25
Picon
Picon
Favicon

Mechanical Verification of a Context Lemma

People,

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 
http://mcs.une.edu.au/~iam/Data/Papers/91fp.ps

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

Permalink | Reply | 0 comments |
headers
David Benson | 2 May 2001 01:14

Foundational Methods in Computer Science Workshop (FMCS'01)


                         ANNOUNCEMENT

                          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]

 WORKSHOP HOTEL:
        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)

Permalink | Reply | 0 comments |
headers
John Hughes | 2 May 2001 13:29
Picon
Picon

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).

Scope

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)

Permalink | Reply | 0 comments |
headers
Joseph Vanderwaart | 3 May 2001 19:33
Picon

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
	http://www.cs.cmu.edu/~joev/work.html

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
states.

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.
Permalink | Reply | 0 comments |
headers
Roy L. Crole | 4 May 2001 18:49
Picon
Picon
Favicon

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)

Permalink | Reply | 0 comments |
headers
Derek R. Dreyer | 4 May 2001 20:41
Picon
Favicon

paper on recursive modules

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

http://reports-archive.adm.cs.cmu.edu/anon/2001/abstracts/01-112.html

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
CMU-CS-01-112

Abstract:

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)

Permalink | Reply | 0 comments |
headers
Bernhard Gramlich | 7 May 2001 19:55
Picon
Favicon

STRATEGIES 2001 (call for participation, prelim. program)

*********************************************************************
          CALL FOR PARTICIPATION AND PRELIMINARY 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 

BACKGROUND, AIMS AND TOPICS

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)

Permalink | Reply | 0 comments |
headers
Brian Postow | 7 May 2001 23:34
Picon
Favicon

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 ]
Permalink | Reply | 0 comments |
headers
Ralf Treinen | 9 May 2001 11:15
Picon

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)

Permalink | Reply | 0 comments |
headers
Alan Wood | 15 May 2001 12:29
Picon

CFP - Coordination 2002


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

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

                         Fifth International Conference
                                      on

                       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:

     http://www-users.cs.york.ac.uk/~wood/Coord02/Coordination2002.html

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)

Permalink | Reply | 0 comments |

Gmane