headers
Mark Lillibridge | 1 Aug 1995 18:38
Picon

The relationship between exceptions and call/cc


The following Tech Report is now available by anonymous ftp:

    "Exceptions are Strictly More Powerful Than Call/CC"
     by: Mark Lillibridge, Carnegie Mellon University

URL:	    ftp://reports.adm.cs.cmu.edu/usr/anon/1995/CMU-CS-95-178.ps
ftp-server: reports.adm.cs.cmu.edu
directory:  /usr/anon/1995
file:	    CMU-CS-95-178.ps

Abstract:

	We demonstrate that in the context of statically typed pure
functional lambda calculi, exceptions are strictly more powerful than
call/cc.  More precisely, we prove that the simply typed lambda calculus
extended with exceptions is strictly more powerful than Girard's F-omega
(a superset of the simply typed lambda calculus) extended with call/cc
and abort.

	This result is established by showing that the first language is
Turing equivalent while the second language permits only a subset of the
recursive functions to be written.  We show that the simply typed lambda
calculus extended with exceptions is Turing equivalent by reducing the
untyped lambda calculus to it by means of a novel method for simulating
recursive types using exception-returning functions.  The result
concerning F-omega extended with call/cc is from a previous paper of the
author and Robert Harper's.
(Continue reading)

Permalink | Reply | 0 comments |
headers
David Aspinall | 6 Aug 1995 15:55
Picon
Picon

paper: Subtyping Dependent Types


Hello all,

I'd like to announce the availability of a draft paper:

                       SUBTYPING DEPENDENT TYPES

                 David Aspinall and Adriana Compagnoni

  		      David.Aspinall@...
	            Adriana.Compagnoni@...

  Abstract:

  We describe a subtyping extension of the Pure Type System lambdaP
  (an abstract version of LF).  This system is the simplest corner of
  the lambda-cube with type-dependency, yet forms the core of applied
  type-theories for which subtyping is a desirable extension, for
  example to give better economy of encodings in LF or to allow
  automatic adaptation of proofs in \lambdaPRED (the predicate
  calculus fragment of the Calculus of Constructions).

  We establish some meta-theoretic results about the system, including
  subject reduction, minimal types and decidability.  

  The combination of subtyping and type-dependency is quite tricky to
  analyse, mainly because the typing and subtyping relations are
  mutually defined, which means that tested techniques of examining
  subtyping in isolation no longer apply.  We prove our results using
  an algorithmic reformulation which breaks some circularity of the
(Continue reading)

Permalink | Reply | 0 comments |
headers
Dirk Dussart | 11 Aug 1995 15:01
Picon
Picon

Curry-Howard Isomorphism


Can anyone refer me to material in which the CH-isomorphism for logics
with subtyping is studied? 

Your help is appreciated!

-- Dirk

[All, Please send your replies to Dirk.
 Dirk, Please summarise your replies to the Types Forum.
  -- Philip Wadler, moderator, Types Forum.]
Permalink | Reply | 0 comments |
headers
Carolyn Talcott | 17 Aug 1995 02:14
Picon

types


I have finally made a web page for my database of automated 
reasoning systems and tools (and added many new entries).
The url for the page is

   http://www-formal.stanford.edu/clt/ARS/ars-db.html

If you find errors or missing links please let me know.  I am 
still gathering data and making new entries 
(a never ending process it seems.)

Enjoy

Carolyn Talcott
http://www-formal.stanford.edu/clt/home.html
Permalink | Reply | 0 comments |
headers
Giovanni Sambin | 18 Aug 1995 12:32
Picon

announcement of a congress


Dear Colleague,

A meeting on type theory will take place on October 19-21
this year in Venice. The main subject of the meeting is
the intuitionistic type theory that Per Martin-Lof
started developing in 1970. This is reflected in the
festive title of the meeting

     "Twenty-Five Years of Constructive Type Theory",

but we also want some related developments to be taken
into account at the meeting. The program will display the
various points of view from which type theory has been
approached, including logic and foundations of mathematics,
computing science, philosophy and linguistics.

There will be two and a half days of talks, followed by
a round table discussion on the background and possible
future lines of development of type theory.
A list of speakers and discussants is appended to
this letter.

 A limited number of places is still available for
registration, and a still smaller number for accomodation
in Venice at a reasonable price. More detailed information
on this and on other practical arrangements will be sent
on request

  Giovanni Sambin       Jan von Plato
(Continue reading)

Permalink | Reply | 0 comments |
headers
Daniel Mahler | 22 Aug 1995 10:31
Picon
Picon

universe elimination rules


Could someone tell me what are universe elimination rules in type theories.

Do they have something to do with quantifying or abstracting over universes?
Are there type systems which actually do this?

	thanks
	Daniel Mahler

[All, Please send your replies to Daniel Mahler.
 Daniel Mahler, Please summarise your replies to the Types Forum.
  -- Philip Wadler, moderator, Types Forum.]
Permalink | Reply | 0 comments |
headers
Geoff Sutcliffe | 31 Aug 1995 01:27
Picon
Picon

CADE-13 Call for Papers


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

     The Thirteenth International Conference on Automated Deduction
     --------------------------------------------------------------

                         Rutgers University
                   New Brunswick, New Jersey, USA

                      30 July - 3 August, 1996

                   CADE-13:  First Call for Papers

The CADE conferences are the major forum for the presentation of new
research in all aspects of automated deduction. Original research
papers, descriptions of working reasoning systems, and problem sets
that provide innovative, challenging tests for automated reasoning
systems, are solicited.

CADE conferences cover all aspects of automated deduction:

    First vs. Higher Order Logics            Classical vs. Non-Classical Logics
    Special vs. General Purpose Inference    Interactive vs. Automatic Systems

Specific topics of interest include (but are not limited to):

    Resolution        Sequent Calculus       Decision Procedures
    Unification       Rewrite Rules          Mathematical Induction
(Continue reading)

Permalink | Reply | 0 comments |
headers
Geoff Sutcliffe | 31 Aug 1995 09:23
Picon
Picon

TPTP-v1.2.0 release


*Email us if you want to register as a TPTP user or be removed from this alias.

                   The TPTP Problem Library, Release v1.2.0
                   ----------------------------------------

                                Geoff Sutcliffe
          Dep't of Computer Science, James Cook University, Australia.
                              geoff@...

                               Christian Suttner
                 Institut fuer Informatik, TU Muenchen, Germany
                       suttner@...

The  TPTP (Thousands  of Problems  for Theorem  Provers)  Problem Library  is a
library of test problems for automated theorem proving (ATP) systems, using the
clause  normal form  of 1st order logic.  The TPTP  supplies the ATP  community
with:
+ A comprehensive library of the ATP test problems that are available today, in
  order to provide an overview and a simple, unambiguous reference mechanism.
+ A comprehensive list of references and other interesting information for each
  problem.
+ New  generalized variants  of problems  whose original  presentation is hand-
  tailored towards a particular automated proof.
+ Arbitary size instances of generic problems (e.g., the pigeon-holes problem).
+ A utility  to convert the  problems to  existing ATP formats.  Currently  the
  KIF, leanTAP, 3TAP, METEOR, MGTP, OTTER, PTTP, SETHEO,  and SPRFN formats are
  supported,  and the  utility can  easily be  extended to  produce any  format
  required.
+ General guidelines outlining the requirements for ATP system evaluation.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alexey P. Kopylov | 21 Aug 1995 20:47
Picon

MLLW2 is undecidable


              Second order  Linear Affine Logic is Undecidable.
                               Alexei Kopylov

 In referring to linear logic fragments,
   N stands for non-commutative versions
     (with -o and o- being left and right implications, respectively,
     and "*" being non-commutative product),
   M for multiplicative fragment,
   A for additive fragment,
   2 for second order quantifiers, and
   I for "intuitionistic" version of linear logic fragments,
   W for Linear Logic with the weakening rule (called Linear Affine Logic).

 Lincoln, Scedrov, and Shankar showed the undecidability of IMLL2 and IMALL2
 by embedding of LJ2 (announced in this forum, LICS '95).
 Lafont has proved the undecidability of MALL2 (announced in this forum, to
 appear in the Journal of Symbolic Logic).
 Recently, Lafont and Scedrov proved that MLL2 is undecidable (announced in
 this forum).
 Emms shows embedding of LJ2 into N-IMLL2 as well.
 Kanovich demonstrated the undecidability of N-MLL2 and second order
 Lambek Calculus (LC2). (Announced in this forum).

 Here we prove that MLLW2 is also undecidable. The main ideas of the proof is
 similar to ideas in Lafont and Scedrov's paper. Namely, we encode two counter
 machines (Minsky machines) in LLW2. In order to obtain the faithfulness of
 the encoding we use the phase semantic. But here we need the phase semantic
 for linear affine logic. So, we introduce such semantic.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane