headers
H}kan Millroth | 2 Dec 1994 14:22
Picon
Picon

CS position in Uppsala


[* I apologise if you receive this more than once. *]

Applications are invited for a permanent position as senior lecturer
at the department of Computing Science, Uppsala University, Sweden.
The department has two chairs in computer science, one in computing
science and one in applied computing science.  The senior lectureship
is with the computing science group.

Virtually all research being conducted in the group is related to
computational logic and other declarative programming paradigms.
However, many different aspects are studied, ranging from topics such
as efficient execution on sequential and parallel computers to
AI-oriented questions, for example, about automated reasoning.

Requirements: PhD in computer science. Applicants should have strong
research and teaching records.

APPLICATIONS CLOSE: January 9, 1995.

GENERAL INFORMATION: For information on the application procedure, call
Christina Lindberg, telephone +46-18-181867, fax +46--18-181999.

For information about the computing science research group contact:

	Jonas Barklund			Hakan Millroth
	email: jonas@...		email: hakanm <at> csd.uu.se
	tel. +46-18-181050		tel +46-18-181056
	fax  +46-18-511530		fax +46-18-511925
(Continue reading)

Permalink | Reply | 0 comments |
headers
PLILP'95 Conference | 3 Dec 1994 17:50
Picon

Call for Papers PLILP'95


[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

\documentstyle{article}

                       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
                       %%        Call for papers      %%
                       %%      PLILP'95 conference    %%
                       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\head{
{\bf                             CALL FOR PAPERS                        
}\\[2mm]
{\Large\bf                          PLILP'95                               
}\\[3mm]
                      Seventh International Symposium on
\\                           Programming Languages,
\\                   Implementations, Logics and Programs
\\{\bf                    Utrecht  (the Netherlands)
}\\                          September 20-22, 1995
}

\def\body{
            Following the six previous \PLILP\ meetings in Orleans (1988), 
            Link\"{o}ping (1990), Passau (1991), Leuven (1992), Tallinn (1993) 
            and Madrid (1994),  the Seventh International Symposium on 
{\em        Programming Languages, Implementations, Logics and Programs
}           will be held in Utrecht (the Netherlands).
            The meeting will run in parallel with \LoPSTr'95, the
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jean Gallier | 12 Dec 1994 16:52

Two papers on reducibility


The following two papers are available by ftp (see below).
Both are are revised versions of earlier papers.
The first one is to appear in TCS (June-July 95?), and the second
one is more of a tutorial in nature.
Together with my earlier

             ``On the Correspondence Between
                  Proofs and lambda-Terms''

to appear any day in the ``Cahiers du Centre de Logique de Louvain'',
(edited by Philippe de Groote), these papers constitute
a fairly unified view of the reducibility method and its
applications. If not already fluent with the method,
I would suggest starting with the above paper,
or the second of the two listed below.

Happy Holidays
(and don't forget about geometric intuitions!)

-- Kurt W.A.J.H.Y. Reillag
   Hospices de Beaune

================================================================= 
             Proving Properties of Typed lambda-Terms
             Using Realizability, Covers, and Sheaves

The main purpose of this paper is to take apart the reducibility
method in order to understand how its pieces fit together, and in
particular, to recast the conditions on candidates of reducibility as
(Continue reading)

Permalink | Reply | 0 comments |
headers
ldpl95 | 13 Dec 1994 13:46
Picon

workshop announcement


[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

[Now that we established the publication of proceedings I would like to
submit a more detailed workshop announcement.  --Michael Huth.]

                         Announcement of the

         Workshop on LOGIC, DOMAINS, AND PROGRAMMING LANGUAGES

                           May 24-27, 1995

      Organizers: K.H. Hofmann, M. Huth, A. Jung, and K. Keimel

                       Fachbereich Mathematik
                   Technische Hochschule Darmstadt
                      64289 Darmstadt, Germany
               E-mail: ldpl95@...

The Workshop on Logic, Domains, and Programming Languages is aimed at
computer scientists and mathematicians alike, who share an active
interest in the mathematical foundations of computer science. The
scope of the workshop encompasses all aspects of Programming Language
Semantics ranging from purely theoretical topics to concrete
applications and implementations of semantic methods. Possible
workshop topics are, for example, Lambda Calculi and Functional
Programming, Domain Theory, Denotational and Algebraic Semantics, Type
Theories, Linear Logic, Process Algebras, and Concurrency.
(Continue reading)

Permalink | Reply | 0 comments |
headers
ohearn | 14 Dec 1994 02:13
Picon

SIPL Advance Program


[Since it is clearly relevant, I am distributing this workshop
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

			SIPL '95  Advance Program

		       2nd ACM SIGPLAN Workshop on 
		     STATE in Programming Languages

			     San Francisco
	 		     Jan 21, 1995

	         (held in conjunction with POPL '95;
	         registration information may be found at
	         ftp://wuarchive.wustl.edu/pub/popl95)

8:30 - 10:00

Tutorial -
  State in Progrmming Languages: 
  Issues in languages, 	semantics and reasoning.
     P. W. O'Hearn (Syracuse University) and 
     U. S. Reddy (University of Illinois)

Formalizing Hoare Logic
     J. E. Caplan (University of Illinois)

10:30 - 12:00

An Imperative Object Calculus
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jean-Yves GIRARD | 15 Dec 1994 10:38
Picon

paper availbale by ftp


PROOF-NETS : THE PARALLEL SYNTAX FOR PROOF-THEORY

One year ago I announced essential progresses on additives, both on  
proof-nets and on geometry of interaction. The paper on GOI was  
quickly written, but the paper on proof-nets was postponed, since I  
found a bug when I wrote the details. Recently I discovered the two  
systems with constant cut-elimination complexity, ELL and LLL. I  
tried to make a proof with old fashioned methods, i.e. sequent  
calculus. This was extremely painful (difficult to avoid the nonsense  
of double layer sequents, difficult to provide a natural size for  
proofs etc.) In fact -assuming that I had the patience to cope with  
these minor technicalities, the reader would have got a symmetric  
problem, i.e. to find out what is the central idea in this  
bureaucratic mess. The use of sequents here was nothing but a  
childish game of encryption/decryption.
This is why I decided to do it with proof-nets. The problem is that  
additives play an important role in LLL (not that much in ELL), and  
that I was never satisfied with the extant notion of proof-net. But  
it turns out that the extant notion (equipped with a lazy  
cut-elimination) normalizes in linear time, and that's enough for  
what I wanted to do. This is the reason why I decided to write a  
survey paper concerning proof-nets. Its aim is to provide an  
alternative syntax, in case one wants to do elegant proof-theory or  
achieve subtle aims, or simply protect forests...
The paper mainly deals with additive proof-nets, for which the best  
known solution is presented, and their lazy normalization. The  
discussion about possible improvements and the description of the  
full procedure are postponed to an appendix. The paper proceeds with  
the unproblematic extension to quantifiers (which look like
(Continue reading)

Permalink | Reply | 0 comments |
headers
Zena Matilde Ariola | 16 Dec 1994 18:10

job announcement


UNIVERSITY OF OREGON: FACULTY POSITION

The Department of Computer and Information Science invites applications for
at least one tenure track faculty position.   Candidates from all areas of
Computer Science will be considered; however, we are particularly
interested in the areas of programming languages, computational science,
and software systems. Candidates should have a Ph.D. in computer science
and a strong commitment to both research and teaching. We offer an
excellent research environment.  The department has major research
strengths and funding in the areas of human/machine interfaces, parallel
programming languages and environments, software engineering, computational
science, distributed operating  systems, electronic media, graphics,
declarative languages, and the theory of computation. The department is
associated with the NSF-funded Software Engineering Research Center (SERC)
and the Computational Intelligence Research Laboratory (CIRL).
Instructional laboratories consist of UNIX-based workstations and computer
servers.  Research facilities include special equipment for user-interface
design, graphics, and parallel processing. A new computational science
laboratory will house multiple parallel computers with high-performance
graphics hardware.

The University of Oregon is located in Eugene, a community rated among the
most livable in the nation. Qualified candidates should send their
curriculum vitae and the names of at least four references to: Faculty
Search Committee, Computer and Information Science, University of Oregon,
Eugene, OR, 97403-1202; or send email: faculty.search@...  For
full consideration, applications should be received by 3/1/95,  but we will
continue to accept applications until the position is filled. The
University of Oregon is an Equal Opportunity/ Affirmative Action
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jean Gallier | 16 Dec 1994 21:17

paper available by ftp


The following paper, a revised version of an older paper, is
available by ftp (see below):

          Kripke models and the  (in)equational logic of
            the second-order lambda-calculus

We define a new class of Kripke structures for the second-order
lambda-calculus, and investigate the soundness and completeness of
some proof systems for proving inequalities (rewrite rules) as well as
equations.  The Kripke structures under consideration are equipped
with preorders that correspond to an abstract form of reduction, and
they are not necessarily extensional. A novelty of our approach is
that we define these structures directly as functors A: worlds ->
Preor equipped with certain natural transformations corresponding to
application and abstraction (where worlds is a preorder, the set of
worlds, and Preor is the category of preorders).  We make use of an
explicit construction of the exponential of functors in the
Cartesian-closed category Preor^{worlds}, and we also define a kind of
exponential to take care of type abstraction.  However, we strive for
simplicity, and we only use very elementary categorical
concepts. Consequently, we believe that the models described in this
paper are more palatable than abstract categorical models which
require much more sophisticated machinery (and are not models of
rewrite rules anyway).  We obtain soundness and completeness theorems
that generalize some results of Mitchell and Moggi to the second-order
lambda-calculus, and to sets of inequalities (rewrite rules).

Available by anonymous ftp as
kripke1.dvi.Z
(Continue reading)

Permalink | Reply | 0 comments |
headers
berline | 19 Dec 1994 12:34
Picon
Favicon

announcement: consistence of Map Theory

    	A simple semantic consistency proof for Map Theory based on
                   $\xi$-denotational semantics

                     Ch. Berline and K. Grue
			     

Map theory, which is a foundation of mathematics based on
lambda-calculus instead of logic and sets, has been introduced in 
[Grue, TCS 102(1), 1992].

Map theory is an equational theory which embodies predicate calculus;
from the metamathematical point of view its strength lies somewhere
between ZFC and ZFC+SI , where SI asserts the existence of an
inaccessible cardinal.

The first result is proved in [G] by means of a syntactical
translation of ZFC (including classical predicate calculus) within map
theory, and the second by building a model of map theory within
ZFC+SI.  This latter construction is however highly technical, though
the starting intuitions are quite natural.

We present here a semantic proof of the consistency of map theory within
 ZFC+SI , which is in the spirit of denotational semantics and relies
on mathematical tools which reflect faithfully, and in a transparent
way, the intuitions behind map theory.

This paper (submitted) is now available by anonymous ftp or by WWW.

ftp host: boole.logique.jussieu.fr
dir:  pub/distrib/berline-grue
(Continue reading)

Permalink | Reply | 0 comments |
headers
Joe Wells | 20 Dec 1994 01:30
Favicon

paper available: New Proof Method for SN for Typed Lambda Calculi


This note is the announcement of the availability of a paper entitled:

  New Notions of Reduction and Non-Semantic Proofs of Beta Strong
  Normalization in Typed Lambda Calculi

by myself and A. J. Kfoury.  Here is the abstract:

  Two new notions of reduction for terms of the lambda calculus are
  introduced and the question of whether a lambda term is beta strongly
  normalizing is reduced to the question of whether a lambda term is
  merely normalizing under one of the new notions of reduction.  This
  leads to a new way to prove beta strong normalization for typed lambda
  calculi.  Instead of the usual semantic proof style based on Girard's
  ``candidats de r\'eductibilit\'e'', termination can be proved using a
  decreasing metric over a well-founded ordering in a style more common in
  the field of term rewriting.  This new proof method is applied to the
  simply-typed lambda calculus and the system of intersection types.

It is Boston Univ. Comp. Sci. Dept. Tech. Rep. 94-014 and it is available
via anonymous FTP from the host CS-FTP.BU.EDU in the directory
"techreports" as the file "94-014-strong-normalization.ps.gz" (93K).  The
URL is:

  ftp://cs-ftp.bu.edu/techreports/94-014-strong-normalization.ps.gz

(Files ending with the ".gz" suffix are compressed with the "gzip"
program, which is available via anonymous FTP from the host
PREP.AI.MIT.EDU in the directory "pub/gnu" with filenames
"gzip-1.2.4.msdos.exe", "gzip-1.2.4.shar", "gzip-1.2.4.tar", and
(Continue reading)

Permalink | Reply | 0 comments |

Gmane