2 Dec 1996 13:35

Hilbert systems vs. Gentzen systems

[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]

Healfdene Goguen writes:

> I am interested in opinions on the tradeoffs between two styles of
> presenting logic:
> 	* systems where the deduction theorem is a theorem, hereafter
> Hilbert systems, and
> 	* systems where the deduction theorem is internalized as a
> rule of inference, hereafter Gentzen systems.
>
> This distinction is lifted to type theory, with first class proof
> objects, through Curry's abstraction algorithm in the Hilbert systems
> and through Church's typed lambda calculus in the Gentzen systems.

...

> I would be interested in any opinions on these tradeoffs, further
> differences between the systems, or recent or historical references
> that discuss this question.

One important difference between combinatory logic (i.e. Hilbert
systems) and lambda calculus (here Gentzen systems) is that the first
is "algebraic", whereas the second is not. In particular the models of
combinatory logic are closed under submodels which is not the case for
lambda calculus. E.g. the closed terms of combinatory logic (the
"interior") form a combinatory algebra which is not the case for
lambda calculus (the closed terms are just a combinatory algebra).

This is discussed in Hindley's & Seldin's "Introduction to Combinators


3 Dec 1996 02:08

Re: Hilbert systems vs. Gentzen systems

[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]

> From Healfdene Goguen:
>	* Meta-properties, such as the deduction theorem, are commonly
> brought into the object language.  This is more serious since Curry's
> abstraction doesn't satisfy the xi rule which allows equality
> underneath abstraction.

> From Thorsten Altenkirch:
>
> One important difference between combinatory logic (i.e. Hilbert
> systems) and lambda calculus (here Gentzen systems) is that the first
> is "algebraic", whereas the second is not. In particular the models of
> combinatory logic are closed under submodels which is not the case for
> lambda calculus. E.g. the closed terms of combinatory logic (the
> "interior") form a combinatory algebra which is not the case for
> lambda calculus (the closed terms are just a combinatory algebra).
>
> This is discussed in Hindley's & Seldin's "Introduction to Combinators
> and lambda calculus", pp. 107 for the untyped case but it is easy to
> see that it applies to typed calculi as well.

There is a point to be considered here that is often overlooked. In a
certain, strong, sense, the lambda calculus actually *is* algebraic.
The failure of the above properties (Curry's abstraction does not
satisfy the xi-rule; lambda calculus models are not closed under
submodels) comes from the notion of model considered, and not from the
lambda calculus itself.  It is my impression that this has been known to
a few people for a long time, but since this point is missing from some
standard texts (including Hindley and Seldin's book and also


4 Dec 1996 23:55

CFP: Types in Compilation Workshop

	   --- ACM SIGPLAN Workshop Announcement ---

Types in Compilation (TIC97)

Held in conjunction with ICFP97
Amsterdam, The Netherlands
June 8, 1997

[The following workshop announcement is available on the web at:

http://www.cs.bc.edu/~muller/TIC97/
]

Workshop Description

Recent advances in type theory have led to a number of new
applications of types during the compilation process. Type
information has been found to be useful for compiler verification,
for program analysis and transformation, for optimizing dynamic
method dispatch in object-oriented languages, for code generation,
for debugging of the compiler and a number of other applications.
Several state-of-the-art compilers maintain an explicitly-typed
representation of the source program through the later stages of
compilation. Some compilers emit type information into the object
file to facilitate later verification of the object code.

The workshop on Types in Compilation is a one day meeting that will
cover both theoretical aspects and practical applications of type
systems in compilation.



5 Dec 1996 18:43

invitation

The laboratory of mathematics of the university of Chambery will have the
opportunity to invite during the 1997 year (winter, spring or fall) a
researcher in logic (from a foreign country) for some weeks (probably
between 2 and 4).
This researcher can be either a person with a permanent position or a
student (having, or almost having a Ph D). He (or she) can "come from"
mathematics or computer science.
The logic group in Chambery works on  lambda calculus : combinatorial
problems, proof and programs with the use of classical logic, parallelism
(pi calculus), ...
Chambery is close to Lyon (There is also a group there at the Ecole
normale) and Grenoble.

R.DAVID
Laboratoire de Maths
Campus Scientifique
73376 Le Bourget du Lac (France)
tel (33) (0)4 79 75 87 17    fax (33) (0)4 79 75 87 42
email david@...


6 Dec 1996 18:29

Paper: 2nd-order unification and type inference for Church-style polymorphism


Hi,

I am pleased to inform you that my paper

Second-order unification and type inference for Church-style
polymorphism

is available via anonymous ftp from zls.mimuw.edu.pl (file
pub/alx/simple.dvi.gz).

Here is a brief abstract

We present a proof of the undecidability of type inference for the
Church-style system ${\cal F}$. For this, we consider the
second-order unification problem. The natural reduction from
unification to type inference leads to certain, quite strong,
restriction on instances --- arguments of variables cannot contain
variables.  This requires another proof of the undecidability of the
second-order unification since known results use variables in
arguments of other variables.  We give such a proof in the present
paper. Moreover, our proof uses elementary techniques, which is
important from the methodological point of view, because the
Goldfarb's proof highly relies on the undecidability of the tenth
Hilbert's problem.

Sincerely yours,
Aleksy Schubert


9 Dec 1996 07:42

ICALP'97 -- final call for papers

[A postscript version of the call for papers is available via the ICALP
web page at http://www.cs.unibo.it/icalp97.]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                   %
%                      ICALP '97                    %
%                      =========                    %
%     24th International Colloquium on Automata,    %
%            Languages, and Programming             %
%                                                   %
%      Bologna, Italy, July 7th -- 11th, 1997       %
%                                                   %
%                 FINAL CALL FOR PAPERS             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The 24th annual meeting of the European Association for Theoretical Computer
Science will take place in Bologna, Italy, July 7-11 1997. ICALP '97 comes
in conjunction with the 25th anniversary of the foundation of EATCS.
To celebrate the SILVER JUBILEE, this edition of ICALP includes several new
events:

- Celebration of EATCS and of its founders (keynote speaker M. Nivat - Paris)

- Invited Lectures on major advances in theoretical computer science since
EATCS has been established:
R. Milner (Cambridge)           M.O. Rabin (Jerusalem and Harvard)
C. Papadimitriou (Berkeley)     D.S. Scott (Pittsburgh)

- Invited Lectures on the state of the art and new promising trends:


2 Dec 1996 16:07

Inhabitation in F (Loeb's thm.)

The following paper is available from my Web page:

http://zls.mimuw.edu.pl/~urzy/ftp.html

or by anonymous ftp from
machine:    ftp.mimuw.edu.pl
directory:    /pub/users/urzy
files:    loeb.{dvi,ps}.Z

Title:  Inhabitation in typed lambda-calculi (a syntactic approach).
Author:  Pawel Urzyczyn

Abstract

A type is inhabited (non-empty) in a typed calculus iff there is a closed
term of this type. The inhabitation (emptiness) problem is to determine
if a given type is inhabited. This paper provides direct, purely syntactic
proofs of the following results: the inhabitation problem is PSPACE-complete
for simply typed lambda-calculus and undecidable for the polymorphic second-
order and higher-order lambda calculi (systems F and F-omega).

By Curry-Howard isomorphism, these lambda calculi correspond to propositional
intuitionistic logics. Thus, two of the above three results are immediate
consequences of Statman's and Loeb's results about zero-order and second-order
propositional intuitionistic logics.  However, the present proofs (esp. that
of Loeb's theorem) are much simpler than the existing ones. In addition, the
proof of Loeb's theorem, being entirely syntactic, does not rely on any
completeness result.

The motivation for this work was to provide a way to explain these results


11 Dec 1996 11:30

NEW PhD PROGRAM AT MUNICH

NEW PhD PROGRAM AT MUNICH (LMU AND TU)
http://www.mathematik.uni-muenchen.de/~schwicht/LI/general.html
* Program.  The Department of Mathematics of the Ludwig-Maximilians-
Universitaet Muenchen and the Department of Computer Science of the
Technischen Universitaet Muenchen (Germany) will establish a new
postgraduate program ("Graduiertenkolleg") entitled "Logic in Computer
Science" starting on April 1st, 1997.  The aim is to extend the
applicability of logical methods for design, specification, verification
and optimization of programs, program systems and hardware.
* Topics.  Logical foundations: Lambda calculus, equational logic, temporal
logic, model checking (Buchholz, Buettner, Clote, Kroeger,  Nipkow,
Schulz, Schwichtenberg).  Theorem provers: integration of (higher order)
equational logic, combination of theorem provers and special methods
(Buchholz, Buettner, Clote, Kroeger, Nipkow, Schulz, Schwichtenberg).
Modeling of distributed systems (Broy, Buettner, Kroeger, Wirsing).
Specification and verification (Antreich, Broy, Clote, Kroeger, Nipkow,
Schwichtenberg, Wirsing).  Foundations of software technology (Antreich,
Broy, Wirsing).
* Grants.  We offers 6 PhD grants for a period of maximally three years.
* Applications.  Applicants with very high qualification in one of the
mentioned or related research topics are invited to send their
applications with the usual documents (curriculum vitae, certifications,
copies of master's thesis and publications, description of intended
project, two letters of recommendation) not later than February 15th, 1997
to the chairman of the postgraduate program: Prof. Helmut Schwichtenberg,
Mathematisches Institut der LMU, Theresienstr. 39, D-80333 Muenchen,
Tel. +49 89 2394 4413/4, Fax +49 89 280 5248,
E-mail: schwicht@...



12 Dec 1996 04:32

Embedding CLL in ILL

  The embedding of classical logic in intuitionistic logic is well-known (for
example, Goedel et al.'s using triple-negation, or Girard's translation using
polarities).  Is there a similar embedding of classical linear logic into
intuitionistic linear logic?  Could someone give me a reference for this?

I am also interested in knowing if anyone has presented a "reverse" embedding
of classical linear logic into classical logic.  Maybe this sounds useless, but
it would give rise to the embedding above by composition:

<-?-
CL ---> CLL
|
v
IL ---> ILL

---
Frank Christoph                 Next Solution Co.      Tel: 0424-98-1811
christo@...                             Fax: 0424-98-1500


12 Dec 1996 04:48


We would like to announce that the following draft
paper is available as

We completely revised the type system in our previous paper:
"A Partially-Deadlock-free Typed Process Calculus (I)."
Any comments are welcome.

--
A Partially Deadlock-free Typed Process Calculus (II)
by
Naoki Kobayashi
Univeristy of Tokyo

Abstract

We propose a novel static type system for a process calculus, which
ensures both partial deadlock-freedom and partial confluence.  The key
ideas are (1) introduction of order of channel use as type
information, and (2)classification of communication channels into
reliable and unreliable channels based on their usage, with a grantee
of the usage by the type system. We can ensure that communications on
reliable channels never cause deadlock, and also that certain reliable
channels never introduce non-determinism.  With the type system, for
example, both call-by-value and call-by-name simply typed
$$\lambda$$-calculus can be encoded into the deadlock-free and
confluent fragment of our process calculus; thus, we can recover
behavior of the typed $$\lambda$$-calculus in the level of process