headers
Thorsten Altenkirch | 2 Dec 1996 13:35
Picon

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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Peter Selinger | 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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Robert Harper | 4 Dec 1996 23:55
Picon
Favicon

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.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Rene David | 5 Dec 1996 18:43
Picon
Favicon

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.
If you are interested please contact R David.

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@...
Permalink | Reply | 0 comments |
headers
Aleksy Schubert | 6 Dec 1996 18:29
Picon
Picon

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

Comments are welcome.

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Roberto Gorrieri | 9 Dec 1996 07:42
Picon

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:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Pawel Urzyczyn | 2 Dec 1996 16:07
Picon
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Helmut Schwichtenberg | 11 Dec 1996 11:30
Picon

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@...
(Continue reading)

Permalink | Reply | 0 comments |
headers
Frank Christoph | 12 Dec 1996 04:32
Picon

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
Permalink | Reply | 1 comment |
headers
KOBAYASHI Naoki | 12 Dec 1996 04:48
Picon

deadlock-free process calculus


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

   ftp://camille.is.s.u-tokyo.ac.jp/pub/papers/deadlock.dvi.Z

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
(Continue reading)

Permalink | Reply | 0 comments |

Gmane