M.Z.Kwiatkowska | 3 Oct 12:57 1994

Chair in Computer Science


Dear Colleague,

Please find enclosed an advertisement for a Chair in Theoretical
Computer Science or Software Engineering at the University of 
Birmingham.  I would appreciate it if you could distribute it
to those who might be interested.  The deadline is 14th October 1994.  

With regards,

Marta Kwiatkowska
_________________

\documentstyle[10pt]{article}
% \pagestyle{empty}
\setlength{\oddsidemargin}{-0.5cm}
\setlength{\evensidemargin}{-0.5cm}
\setlength{\textwidth}{6.75in}
\setlength{\topmargin}{-0.5cm}
\setlength{\headheight}{0cm}
\setlength{\headsep}{0cm}
\setlength{\textheight}{9.9in}
\def\sp{\\[0.1cm]}
\def\Sp{\\[0.2cm]}
\def\SP{\\[0.45cm]}
\def\ps{\vspace{-0.2 cm}}
\def\Ps{\vspace{-0.4 cm}}
\def\PS{\vspace{-0.6 cm}}
\def\hs{\newline\hspace*{2.0cm}}
% indent next line
(Continue reading)

Uffe Engberg | 3 Oct 14:32 1994
Picon
Picon

BRICS positions


			Postdoctoral positions at BRICS

There are to be several postdoctoral positions at BRICS for a period
of one to two years starting in 1995.  Applications by researchers are
welcome in the areas of logic, semantics and algorithmics.
Applications for positions should preferably be sent by e-mail and
include curriculum vitae and two or three names of referees for
recommendations as well as the referees' regular mail addresses and,
if possible, e-mail addresses.

BRICS, a Centre for Basic Research in Computer Science, is funded by
the Danish National Research Foundation for the period 1994-1999.  Its
aim is to establish in Denmark important areas of basic research in
the mathematical foundations of Computer Science, notably Algorithmics
and Mathematical Logic.  The Centre is to develop these areas as a
joint effort between the theoretical-computer-science groups at Aarhus
University and Aalborg University.  The research plan is based on a
committment to develop Algorithmics and Logic integrated with existing
strong activities in Semantics of Computation, using a combination of
long-term efforts and a number of short-term, intensive programmes,
within carefully chosen scientific themes.  Organizationally, BRICS is
an autonomous centre with its own management, and yet with its
activities strongly integrated in the existing infrastructure and
student environments at the two universities.

The scientific planning is the responsibility of the following committee:

Glynn Winskel, Professor (Aarhus), Director
Mogens Nielsen, Associate Professor (Aarhus), Codirector
(Continue reading)

Computer Science Theorynet | 7 Oct 13:58 1994
Picon

Request for Subscription to types list

Attachment: application/octet-stream, 299 bytes
Peter Wegner | 24 Oct 15:40 1994

Please publicize this in the types list

 To: Potential Contributors to Computing Surveys
 Subject: Invitation to discuss the article "On Computational Complexity and the Nature of Computer
Science", by Juris Hartmanis
 From: Peter Wegner, Incoming Editor in Chief, Computing Surveys
 Reply to: kha@...

You are invited to submit a discussion piece to Computing Surveys on topics arising from the recent Turing
Award article by Juris Hartmanis in the October CACM. The overall topic of his article, "On Computational
Complexity and the Nature of Computer Science," lends itself to both technical discussion of questions
in theoretical computer science and broader discussion of policy issues relating to "Computing the
Future". I hope you will be able to participate so that we can start a meaningful discussion on the research
directions and goals of computer science in the pages of Computing Surveys. Juris has agreed to comment on
accepted discussion items. Potential topics for discussion, all of them related to questions raised in
the paper, are listed below:

 1. What is the role of theory, and especially of complexity theory, in computer science? How does
complexity relate to other theoretical areas of computer science like semantics?
 2. What are the critical research questions for the next decade? How is the change from algorithmic to
network and distributed computing technology affecting the paradigm of computer science research? 
 3. What distinguishes CS from the other sciences? Is it the wide range of scales, its concrete and
general-purpose conceptual models, or something else.
 4. What is the status of automata theory and what are its current challenges?
 5. What is the status of complexity theory and what are its current challenges?
 6. What is the status of the P = NP problem and what is its relevance to
broader issues?
 7. What is the role of nondeterminism in algorithms research, are there connections to concurrency
research? 
 8. What is the role of randomness, information theory, and Kolmogoroff complexity in theoretical research?
 9. What is the role of algorithms in scalability and programming in the large?
 10. What is the relation of theoretical and experimental computer science? Is the role of experiments
changing as the field matures?
 11. What is the role of theory in software engineering?
 12. What is the relation of computer science to the physical sciences and to
engineering? Is computer science primarily an engineering discipline, an experimental disciline, a
mathematical discipline, or a new discipline that borrows from other fields but has unique goals and
perspectives? 
 13. What are the challenges in the area of metrics and experimentation?
 14. What is the role of demonstration as an alternative to examination?
 15. Is "demo or die" a real alternative to "publish or perish" in academic institutions?
 16. What is the role of engineering and mathematical principles in computer science?
 17. What is the role of aesthetics and taste in a world that is increasingly emphasizing the short-term
relevance of research?
 18. How central is algorithmic abstraction to practical computer science? Is it the primary abstraction
or is it just one among many "levels of abstraction" for practical problem solving and system design?
 19. Does a "natural computer scientist", say a software engineer, necessarily
think algorithmically?
 20. What is the role of proofs and of interactive proofs? What are the limitations of proof techniques for
programming in the large?

Your discussion should be between 500 and 1000 words, and should be received no later than Dec 15th for
inclusion in the March 1995 issue of Computing Surveys.  Please send a message to my secretary
"kha@..." with a copy to me "pw <at> cs.brown.edu" to let me know if
you can participate in this "Computing Surveys Symposium". 
	
	Yours

	Peter Wegner
	Editor in Chief Computing Surveys (starting January 1995)

lphuang | 10 Oct 10:57 1994
Picon

Programs for Proof-nets


The following programs:

 mll.c      a program for testing whether a
            proof-structure in multiplicative
            fragment of linear logic is logically sound, i.e.
            is a proof-net

fmll.c     a program for testing whether a  proof
           structure with units (1s and \bots) is
           logically sound, i.e. represent (at least)
           one proof of sequent calculus

are now available by ftp.

Both programs are   highly portable,
they are written in ANSI C, and can be compiled
in ANY computer where ANY C compiler is installed.
Please read the file mll.fmll.read.me  first.

FTP instructions:

    ftp gloxinia.cs.cuhk.hk
    login: lphuang
    password: hlplhy
    cd itnt
    get mll.c
    get fmll.c
    get  mll.fmll.read.me
    bye

If you are interested in the theoretical topics behind the programs,
please find following files in the same directory

 criteria.dvi
 appen. dvi

Sincerely,

Lin Peng Huang Ph.D.
Department of Computer Science and Engineering
Shanghai Jiao Tong University
Shanghai 200030, P.R.China

Harold Schellinx | 11 Oct 17:50 1994
Picon

Paper announcement


  The following paper is obtainable by anonymous ftp from 

               boole.logique.jussieu.fr

  It can be found in the directory pub/scratch/DJS, under the name

               decostringopolaro.ps.Z

  (download, uncompress, print)

  The directory DJS contains several related papers (read the
  README file).

     ---------------------------------------------------
    |      V. Danos, J.-B. Joinet & H. Schellinx        |
    |                                                   | 
    |    "A NEW DECONSTRUCTIVE LOGIC: LINEAR LOGIC"     |
     ---------------------------------------------------

    Abstract:

    There has been much ado about constructivizing classical connectives
    and quantifiers during the last four, five years.
    Our approach to the problem is to understand this first of all as the
    quest for a classical second order calculus equipped with a strong
    (and, as much as possible, confluent) normalization, and a 
    denotational semantics.

    Considering that there are many, seemingly unrelated, solutions, we 
    would rather classify these, than throw one more solution on the heap 
    (new solutions are going to show up as a result of the classification, 
    anyway).

    As the title suggests, to design such a classification we use linear
    logic, to be specific three different ways to embed Gentzen's LK into LL:
    pletho, stringo and polaro. Each one of these `therapies' gives rise to 
    a sound computational interpretation of classical logic obtained by
    `pulling back' the normalization of LL as well as its denotational 
    semantics in coherent spaces. As a by-product we recover Parigot's 
    'free deduction' (FD) and `lambda-mu', as well as Girard's LC as
    particular cases of, respectively, the pletho, stringo and polaro
    `therapies'.

Andre Scedrov | 11 Oct 23:02 1994

Lambda Definability in Categorical Models


               A Characterization of Lambda Definability 
             in Categorical Models of Implicit Polymorphism  

                            Moez Alimohamed 

                      University of Pennsylvania   

This paper contains the work of Moez Alimohamed, a mathematics graduate 
student at the University of Pennsylvania who died tragically on August 29th.
Lambda definability is characterized in categorical models of simply typed 
lambda calculus with type variables.  A category-theoretic framework known 
as glueing or sconing is used to extend the Jung-Tiuryn characterization of 
lambda definability in Henkin models for the simply typed lambda calculus 
first to ccc models, and then to categorical models of the calculus with 
type variables.  

WWW access is http://www.cis.upenn.edu/~andre/moez.html. The paper is also 
available by anonymous ftp from the host ftp.cis.upenn.edu as the file 
pub/papers/scedrov/def.ps.Z.  

Jean-Yves GIRARD | 12 Oct 14:09 1994
Picon

LLL


An extended abstract of a forthcoming paper
LIGHT LINEAR LOGIC
is available by anonymous ftp
lmd.univ-mrs.fr
dir : pub/girard
name : LLLo.ps.Z

Abstract : The abuse of structural rules can have damaging complexity  
effects.

---

Jean-Yves GIRARD
Directeur de Recherche

CNRS, Laboratoire de Mathematiques Discretes
163 Avenue de Luminy, case 930
13288 Marseille cedex 9

<girard@...>
(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)

Sergei Artemov | 13 Oct 19:40 1994
Picon
Picon

LLW is decidable


The paper by A.Kopylov 

\title{Decidability of Linear Affine Logic}
\author{Alexei P. Kopylov \\
Department of Mathematics and Mechanics \\
Moscow State University \\
119899, Moscow, Russia}
\date{September, 1994} 

\begin{abstract}
The propositional Linear Logic is known to be undecidable.
In the current paper we prove that the full propositional Linear Affine
Logic containing all the multiplicatives, additives, exponentials,
and constants is decidable. The proof is based on a
reduction of the Linear Affine Logic to sequents of
specific ``normal forms'', and
on vector games interpretation adapted to these ``normal forms''.
\end{abstract}

is now issued as the preprint

 CNRS, Laboratoire de Math\'{e}matiques Discr\`{e}tes,
 Pr\'{e}tirage n$^\circ$ 94-32, ~1994, 30~p.\\
 Available by anonymous ftp from host lmd.univ-mrs.fr
 and the file pub/kopylov/fin.dvi

Best regards, 
Sergei Artemov  

Andre Scedrov | 17 Oct 20:59 1994

DIMACS Special Year on Logic and Complexity


>From vardi@... Mon Oct 17 14:14 EDT 1994
>From: vardi@... (Moshe Vardi)

       DIMACS 1995-96 Special Year on Logic and Algorithms
     Call for Visitor & PostDoctoral Fellowship Applications

   The DIMACS Center for Discrete Mathematics and Theoretical Computer
Science announces its 1995-6 Special Year on Logic and Algorithms.

   DIMACS is a Science and Technology Center funded by the NSF,
whose participating institutions are Rutgers University, Princeton 
University, AT&T Bell Laboratories, and Bellcore.  Research and 
education activities at DIMACS focus on such areas as analysis of 
algorithms, combinatorics, complexity, computational algebra, discrete 
and computational geometry, discrete optimization and graph theory.  
A primary activity of the Center is to sponsor year-long research 
programs on specific topics of current interest, and one such program
is this Special Year on Logic and Algorithms.

   A dichotomy in theoretical computer science is best demonstrated by
looking at the 1994 Handbook of Theoretical Computer Science.  Volume A
discusses algorithms and complexity, while Volume B treats formal models
and semantics.  Theoretical computer science in the United States is
largely "Vol. A"-ish, while European theoretical computer science is
largely "Vol. B"-ish.  The goal of this Special Year is to bridge the gap
between the two branches, focusing on three bridge areas: Computer-Aided
Verification, Finite-Model Theory, and Proof Complexity.  All three are
emerging research areas that fit naturally between Vol. A and Vol. B.

   Below is a brief description of each topic, and a tentative list of
workshops associated with that topic.  We also plan a series of week-long
tutorials, one in each topic, intended to introduce students, recent
graduates, and professionals from other areas to the topic.

   We invite applications for visiting and postdoctoral positions at
DIMACS in connection with the Special Year.  We encourage people to
apply to NSF or other granting agencies for support to be used at
DIMACS, as well as applying to DIMACS itself.  Many funding deadlines
fall between mid-October and mid-November, which calls for speedy
action by those who are interested in visiting DIMACS.  For more
information on these positions, likely granting agencies, or anything
else, contact DIMACS as described at the end of this announcement.
DIMACS will announce other postdoc and visitor application deadlines
in November, 1994.

                     Computer-Aided Verification

   Computer-Aided Verification studies algorithms and structures for
verifying properties of programs.  It draws upon techniques from graph
theory, combinatorics, automata theory, complexity theory, Boolean
functions and algebras, logic, Ramsey theory and linear programming.  
Since the DIMACS CAV workshop in 1990, worldwide interest in CAV has
grown enormously, not only in academia but in companies like Intel, DEC,
Sun and AT&T.  This creates an unusual and rewarding opportunity to see
theory put directly into practice.
   We plan workshops in "Timing verification and hybrid systems" and in
"Computational and complexity issues in automated verification".

                           Finite-Model Theory

   Model theory is the study of mathematical structures which satisfy
sets of axioms.  Recent work on the FINITE models of a set of axioms has
yielded elegant connections with theoretical computer science, including
model-theoretic characterizations of complexity classes.  Further, when a
class of finite mathematical structures (e.g. graphs) is equipped with
probability measures, one can often develop powerful meta-theorems called
zero-one laws, which give conditions under which probabilities must
approach zero or one as the structure size goes to infinity.
   We plan workshops in "Finite models and descriptive complexity" and in
"Logic and random structures".

                           Proof Complexity

   Two related notions of "proof complexity" currently motivate research
at the interface between computer science and logic.  One notion centers
on the length of a proof, and the other on the complexity of the inference
steps within the proof.
   It is well known that NP=co-NP iff all propositional tautologies have
short proofs.  But the connection between proof length and complexity
theory goes much deeper.  Lower bounds on circuits are closely tied to
those on proof length in restricted systems, and advances on one front
often lead quickly to progress on the other.
   By restricting the complexity of inference steps within a proof, one
obtains a fragment of Peano Arithmetic called Bounded Arithmetic, which
defines exactly the predicates in the polynomial hierarchy.  Exciting 
recent work has shown that if certain theories of bounded arithmetic can
prove lower bounds in complexity theory, then corresponding cryptographic
systems cannot be secure.
   We plan a single, four-day workshop on "Feasible arithmetic and
lengths of proofs".

                          Other Interactions

   As usual, this DIMACS Special Year aims to be inclusive, not exclusive.
Many other areas, beyond the organizers' ken, would mesh with these themes.
This fourth, "catch-all" topic is intended to encourage all scientists
who might benefit from interaction with logicians, combinatorialists and
computer scientists, and with the topics we HAVE listed.

                      Federated Logic Conference

   As part of this Special year, DIMACS will host a Federated Logic
Conference (FLC).  FLC will be modeled after the successful Federated
Computer Research Conference (FCRC).  The goal is to battle fragmentation
of the technical community by bringing together synergetic conferences 
that apply logic to computer science.  The following conferences will
participate in FLC: CADE (Conference on Automated Deduction), CAV
(Conference on Computer-Aided Verification), LICS (IEEE Symp. on Logic in
Computer Science), and RTA (Conference on Rewriting Techniques and
Applications). The four conferences will span eight days, with only
two-way parallelism at any given time.  We will make special efforts to
bring about interaction between the various conferences.  The meeting will
take place in late June, 1996, on one of the Rutgers campuses.

                      For Further Information

   You can use several methods to contact the DIMACS center.
     By email: center@...
     (For information on visiting, fellows@...)
     By telephone: 908-445-5928
     By FAX: 908-445-5932
     By mosaic/www/lynx: http://dimacs.rutgers.edu/
     By gopher: gopher dimacs.rutgers.edu
     By TELNET: telnet dimacs.rutgers.edu and login as "info"
     By post: DIMACS Center
              Rutgers University
              P.O. Box 1179
              Piscataway, NJ 08855-1179
You can also contact the following people:

     For prompt discussion of applying for visiting faculty fellowships,
postdoctoral fellowships, etc. contact
     Eric Allender, <allender@...>
     Moshe Vardi, <vardi@...>
Available information includes a list of NSF programs and contacts,
information on DIMACS matching opportunities for postdoctoral fellowships,
etc.

DIMACS Associate Director for Research:
     Steve Mahaney <mahaney@...>

DIMACS Center Administrator:
     Maryann Holtsclaw <holts@...>

Special Year Organizing Committee:
     Eric Allender, Rutgers U. <allender@...>
     Bob Kurshan, AT&T Bell Labs <k@...>
     Moshe Vardi, Rice U. <vardi@...>

Special Year Publicity Chair:
     Stephen Bloch, Adelphi U. <sbloch@...>

Special Year Steering Committee:
     Paul Beame, U. Washington <beame@...>
     Sam Buss, U. California, San Diego <sbuss@...>
     Gregory Cherlin, Rutgers U. <cherlin@...>
     Ed Clarke, Carnegie Mellon U. <Edmund_Clarke@...>
     Steve Cook, U. Toronto <sacook@...>
     Allen Emerson, U. Texas <emerson@...>
     Joan Feigenbaum, AT&T Bell Labs <jf@...>
     Orna Grumberg, Technion <orna@...>
     Phokion Kolaitis, U. California, Santa Cruz <kolaitis@...>
     Daniel Leivant, Indiana U. <leivant@...>
     Richard Lipton, Princeton U. <rjl@...>
     Amir Pnueli, Weizmann Institute <amir@...>
     Peter Winkler, AT&T Bell Labs <pw@...>


Gmane