headers
Kim Bruce | 1 Apr 1996 20:35
Picon

FOOL Workshop paper submission problem


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

We had a fairly catastrophic failure of e-mail this morning and may have
lost some submisions for FOOL 3, The Third International Workshop on
Foundations of Object-Oriented Languages.

If you submitted a paper and have not received an acknowledgement from me,
please resubmit your paper to fool-submit@... with a note to 
the effect that it is a resubmission.  For added safety send a separate note
to fool-info as we have also been experiencing some difficulty with some
mail host machines choking on long postscript files.

I apologize for the inconvenience.

	Kim Bruce, FOOL(ish) program chair

P.S.  This all comes from having a paper deadline on April Fool's day (U.S.
- and perhaps world - holiday in which people play tricks on each other).
I guess computers can get involved too!
Permalink | Reply | 0 comments |
headers
Robert Harper | 4 Apr 1996 18:32
Picon

reminder: ICFP '96, FCRC '96


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

%!PS-Adobe-2.0
%%Creator: dvipsk 5.58f Copyright 1986, 1994 Radical Eye Software
%%Title: ICFP.dvi
%%Pages: 1
%%PageOrder: Ascend
%%BoundingBox: 0 0 612 792
%%EndComments
%DVIPSCommandLine: dvips -f ICFP
%DVIPSParameters: dpi=300, compressed, comments removed
%DVIPSSource:  TeX output 1996.02.10:1458
%%BeginProcSet: texc.pro
/TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N
/X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72
mul N /landplus90{false}def / <at> rigin{isls{[0 landplus90{1 -1}{-1 1}
ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale
isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div
hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul
TR matrix currentmatrix dup dup 4 get round 4 exch put dup dup 5 get
round 5 exch put setmatrix}N / <at> landscape{/isls true N}B / <at> manualfeed{
statusdict /manualfeed true put}B / <at> copies{/#copies X}B /FMat[1 0 0 -1 0
0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{/nn 8 dict N nn
begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X
array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo
setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{/sf 1 N /fntrx
FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0]N df-tail}B /E{
pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}
B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{128 ch-data dup
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alessandra Carbone | 4 Apr 1996 11:18
Picon

Two logic papers


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

Both papers can be requested by writing to ale@...

TITLE: Interpolants, Cut Elimination and Flow Graphs for the
Propositional Calculus

AUTHOR: A. Carbone -- ale@...

To appear in Annals of Pure and Applied Logic.

ABSTRACT: We analyse the structure of propositional proofs in the
sequent calculus focusing on the well-known procedures of
Interpolation and Cut Elimination.  We are motivated in part by the
desire to understand why a tautology might be `hard to prove'.  Given
a proof we associate to it a logical graph tracing the flow of
formulas in it (Buss, 1991) (The idea of using the flow of occurrences
to study the structure of proofs is fundamental in the work of
Jean-Yves Girard (Girard, 1987)).  We show some general facts about
logical graphs such as acyclicity of cut-free proofs and acyclicity of
contraction-free proofs (possibly containing cuts), and we give a
proof of a strengthened version of the Craig Interpolation Theorem
based on flows of formulas.  We show that tautologies having minimal
interpolants of {\it non-linear} size (i.e. number of symbols) must
have proofs with certain precise structural properties. We then
analyse the transformation of logical flow graphs during the procedure
of cut elimination and show that given a proof $\Pi$ and a cut-free
form $\Pi '$ associated to it (obtained by a particular cut
elimination procedure), certain subgraphs of $\Pi '$ which are logical
(Continue reading)

Permalink | Reply | 0 comments |
headers
Roy L. Crole | 12 Apr 1996 18:44
Picon
Picon
Favicon

Finite Model Theory Tutorial


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

                        FINITE MODEL THEORY

                 Problems, Methods and Applications
                          - A Tutorial -

                       Second Announcement.

            University of Wales Swansea, 7--9 July, 1996.

Finite model theory has emerged in recent years as a very active
area of research, on the frontier of logic, combinatorics and computer
science.  The two-day tutorial to be held in Swansea will present
an in-depth introduction to the field aimed at postgraduate students
and postdoctoral researchers (though open to all).

Topics covered will include the central problems and methods of finite
model theory, as well as applications in complexity theory, databases
and computer aided verification.

The detailed programme and a registration form are attached.

The cost of registration is 380 GBP.  A limited number of subsidised
places are available for postgraduate students at 340 GBP.  These will
be awarded on a first come first served basis, so early registration
is recommended.

Registration includes:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Joxan Jaffar | 12 Apr 1996 18:28
Picon

ASIAN'96 CALL FOR PAPERS


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

                        CALL FOR PAPERS --- ASIAN'96

                     ASIAN COMPUTING SCIENCE CONFERENCE

                       Singapore, December 2-5, 1996

                                 BACKGROUND
                                 ----------

The  first  conference  ASIAN'95 (also called ACSC'95 last year) was held
in Bangkok, Thailand, in December 1995, organized by the Asian Institute
of Technology in partnership with INRIA, France, and the UNU/IIST, Macau.
Its main purpose was to provide a local forum for Asian researchers in
Computer Science.  Its scope was a  broad coverage of CS, though there was
a focus on the more conceptual areas of algorithms, concurrency and
knowledge.  Its proceedings appeared as  Springer-Verlag's LNCS 1023.

                                   SCOPE
                                   -----

The  1996  conference will continue to emphasize the conceptual areas of CS,
though papers in all areas will be considered.  The following themes
represent the areas of focus for this year.

* Programming (semantics, languages, systems, paradigms, types, ...)
* Concurrency & Parallelism (algorithms, formalisms, systems, ...)
* Networking & Security (algorithms, protocols, formalisms, systems, ...)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Sutcliffe Geoff | 16 Apr 1996 16:06
Picon
Favicon

CADE-13 ATP System Competition


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

         Thirteenth International Conference on Automated Deduction
                   Rutgers University, New Brunswick, USA
                          30 July - 3 August, 1996

                       CADE-13 ATP System Competition
                       ------------------------------

                        FINAL CALL FOR PARTICIPATION

The CADE conferences are the major forum for the presentation of new
research in all aspects of automated deduction.  An ATP (Automated
Theorem Proving) system competition will be held in conjunction with
CADE-13.  The competition will be held on Thursday, 1 August, 1996.

The CADE-13 ATP system competition will evaluate the performance of
fully automated sound ATP systems, on 1st order CNF theorems chosen
from the TPTP Problem Library.  The evaluation will be in terms of the
number of theorems proved, and the time taken; in the context of a
specified time limit for each proof attempt, and a bounded number of
TPTP theorems.  Issues regarding competition categories, problem
selection, time limits, system execution, and performance evaluation
are explained in the competition WWW page:
    http://wwwjessen.informatik.tu-muenchen.de/~suttner/Competition.html
Please note the following changes since the original competition
announcement:
+ Propositional problems have been excluded
+ The pure equality category will contain only unit equality problems,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Milan Daniel | 19 Apr 1996 16:24
Picon

GOEDEL'96 - Conference Programme


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

   Conference Announcement,  Programme  and  Registration Form
   ***********************************************************

On the occasion of the ninetieth anniversary of the birth of Kurt Goedel,
an international conference entitled

   LOGICAL FOUNDATIONS OF MATHEMATICS, COMPUTER SCIENCE AND PHYSICS
             -- Kurt Goedel's Legacy (GOEDEL'96)

will take place on August 25-29, 1996, in Brno, Czech Republic
(the birthplace of Kurt Goedel).

Aims and topics:

 The aim of the conference is to pay tribute to Kurt Goedel
 by arranging a scientific event presenting a forum for papers
 relevant to foundational aspects of Logic in Mathematics, Computer
 Science, Philosophy and Physics -- areas influenced by Kurt Goedel's
 work.
   A session is planned to honour Professor Hao Wang, one of Goedel's
 closest collaborators, who died on May 13, 1995. The
 proceedings volume will be published by Springer-Verlag in
 the series Lecture Notes in Logic and distributed at the
 conference. (The deadline for contributions has already expired.)

Organizers:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Allan Cheng | 19 Apr 1996 17:13
Picon
Favicon

BRICS Autumn School in Verification


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

*************************************************************
 This message is being forwarded on several mailing lists.
 Please excuse receipt of multiple copies and please 
 forward to any colleagues whom it might interest.
*************************************************************

                Preliminary Announcement

                 BRICS Autumn School in 
                    Verification 

            October 28 -- November 2, 1996
                   Aarhus, Denmark

Description
===========

BRICS, centre for  Basic  Research In Computer  Science, was
founded in 1994 by  the Danish National  Research Foundation
at University   of  Aarhus and  University  of  Aalborg; the
director  is  Professor Glynn   Winskel.   Each year,  BRICS
focusses  on a selected theme in  the area of Algorithms and
Complexity Theory, Logic, and Semantics.

This year's BRICS theme is Verification. The activities will
cover verification  of computing  systems in a  broad sense.
More specifically,  we  intend to investigate  specification
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carl Gunter | 19 Apr 1996 20:19

new job


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

[As can be seen from the following, the Penn introductory course has
an unusually `typish' flavour, a development to be applauded.
-- Philip Wadler, moderator, Types Forum.]

		    ------------------------------
		      University of Pennsylvania
		    Instructor in Computer Science
		    ------------------------------

Applications are invited for an instructor position in Computer
Science, beginning July 1996.  Candidates from all areas of computer
science will be considered, although the principal selection criterion
will be demonstrated teaching and laboratory design ability rather
than research. The appointment is initially for one year, renewable
for up to three years.

The instructor will be primarily responsible for the laboratory
section of Programming Languages and Techniques, our introductory
undergraduate programming course for computer science majors.  This
course is a two semester sequence that teaches programming using three
programming languages: Scheme, SML, and C++ (with possibly some Java).
The goal is to teach language principles like semantics, types,
abstraction, and modular design while applying these principles in
laboratory exercises.  We are especially interested in applicants with
a knowledge and interest in the languages and topics of the course,
ability and enthusiasm for teaching programming, creativeness in
designing laboratory exercises, and good organizational skills.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Robert Harper | 19 Apr 1996 21:58
Picon
Favicon

reminder: fcrc registration deadline looms


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

The deadline for hotel rooms for the Federated Computing Research
Conferences (including ICFP, PLDI, and the Workshop on Functional
Languages in Introductory Computing) has been extended until April
24th.  Please register soon to ensure that you will be able to get a
room at the conference hotel!

For more information, see the FCRC home page at
http://www.acm.org/conferences/fcrc.

Robert Harper
Permalink | Reply | 0 comments |

Gmane