headers
lcp | 6 Sep 1990 23:08
Picon

ISABELLE USERS EMAIL FORUM

To: logic@..., types <at> theory.lcs.mit.edu,
        proof-sci@...

Date: Thu, 23 Aug 90 12:05:54 +0100

ISABELLE USERS EMAIL FORUM   isabelle-users@...

A new electronic mailing list is available for users of the theorem prover
Isabelle. The list is open to everybody who is interested in Isabelle.

The mailing list can be used for the following purposes (among others):

* to exchange information about proofs conducted using Isabelle

* to exchange formalizations of logics, tactics, and other pieces of code
(of reasonable size!)

* to give information about how, using FTP, to obtain pieces of code
of unreasonable size

* to report faults and limitations of Isabelle

* to volunteer to correct such faults and limitations

* to discuss wider issues such as foundations, logical frameworks, ...

* by Isabelle's implementors, to ask your opinion of proposed changes and
to announce new releases

The forum will NOT be moderated.
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 10 Sep 1990 17:31
Picon

SIGACT news

Date: Fri, 07 Sep 90 15:19:27 -0700

SIGACT news has columns on
	Database Theory
	Cryptology
	Computational Geometry
	Complexity Theory
but no
	Logic and Programming Theory

Any volunteers?
Permalink | Reply | 0 comments |
headers
gunter | 21 Sep 1990 19:09

PER's and operational semantics

Date: Thu, 20 Sep 90 14:10:54 EDT

There is been quite a bit of interest in the use
of Partial Equivalence Relations to model types
in programming languages.  However, I cannot think
of even one paper on PER's which discusses the
relationship between these models and the execution
of the programs they are intended to interpret.
What is currently known about this subject?  Are
there some obvious observations one can make based
on what is known about the untyped lambda calculus?

carl gunter
Permalink | Reply | 0 comments |
headers
theory | 21 Sep 1990 19:17
Picon

Lecture by Harry Mairson: Complexity of Type Inference

Date: Tue, 18 Sep 90 17:45:29 EDT
To: theory-seminars

                Massachusetts Institute of Technology
                   Laboratory for Computer Science
                    Theory of Computation Seminar

                  Date: Thursday, September 27, 1990
                     Time: Refreshments at 4:00pm
                            Talk at 4:15pm
                           Place: NE43-512A

                   The Complexity of Type Inference
                for Higher-order Typed Lambda Calculi

                           Harry G. Mairson
                         Brandeis University
                        Waltham, Massachusetts

We analyze the computational complexity of type inference for untyped
lambda-terms in the second-order polymorphic typed lambda-calculus
(F_2) invented by Girard and Reynolds, as well as higher-order
extensions F_3, F_4,..., F_omega proposed by Girard.  We prove that
recognizing the F_{2}-typable terms requires exponential time, and for
F_omega the problem is nonelementary.  We show as well a sequence of
lower bounds on recognizing the F_{k}-typable terms, where the bound
for F_{k+1} is exponentially larger than that for F_k.

The lower bounds are based on generic simulation of Turing Machines,
where computation is simulated at the expression and type level
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 22 Sep 1990 16:53
Picon

Re: PER's and operational semantics

To: gunter@...
Cc: types@...

In-Reply-To: Your message of Fri, 21 Sep 90 13:09:39 -0400.
             <9009211709.AA07500 <at> stork> 
Reply-To: John C. Mitchell <jcm@...>
Date: Fri, 21 Sep 90 11:46:56 -0700
Sender: jcm@...

This is a reasonable question. There are several situations you might
take a look at. The simplest, which might not turn out to be very
interesting, is traditional HEO as a model of typed lambda calculus,
perhaps with primitive recursion operators at all types. Since all of
the recursive functions in this model are total, some of the issues
ordinarily involved in establishing computational adequacy might not arise.

A more interesting question, to my mind, is what happens with models that
do contain a fixed-point operator, and the relationship between the
domain structure and recursion theory. The papers in Session 11 of last
LICS might be a good place to start here (Freyd  Mulry Rosolini Scott;
Abadi Plotkin; Phoa). Perhaps this is what you were suggesting, Carl,
when you asked about the untyped rather than typed calculus?

John
Permalink | Reply | 0 comments |
headers
gunter | 23 Sep 1990 04:11

PER's and operational semantics

Date: Sat, 22 Sep 90 14:57:07 EDT
To: jcm@...
Cc: types@...

"A more interesting question, to my mind, is what happens with models that
do contain a fixed-point operator, and the relationship between the
domain structure and recursion theory."     --- John Mitchell

This is really what I had in mind.  The interpretation would need to
use CPER's (as in Amadio's LICS 88 paper), the PER's in the
Abadi/Plotkin paper, or something else which is able to interpret
recursion.  Does an adequacy or full abstraction result hold for the
semantics of a reasonable calculus in any of these models?

                --- carl gunter
Permalink | Reply | 1 comment |
headers
Jonathan P. Seldin | 27 Sep 1990 20:46
Picon
Picon

Extensions to Theory of Constructions (734 lines)

Date:     Wed, 27 Sep 89 11:22:41 EDT

 EXCLUDED MIDDLE WITHOUT DEFINITE DESCRIPTIONS IN THE THEORY OF CONSTRUCTIONS

                              Jonathan P. Seldin
                          Department of Mathematics
                             Concordia University
                         7141 Sherbrooke Street West
                          Montreal, Quebec, H4B 1R6
                                    Canada
                         seldin@...

     Acknowledgement of Sponsorship:  The research which produced the 
     information contained in this document was sponsored in part by the 
     U.S. Air Force Systems Command, Rome Air Development Center, Grif-
     fiss AFB, New York 13441-5700 under Contract No. F30602-85-C-0098, 
     in part by grant EQ41840 from the program Fonds pour la Formation de 
     Chercheurs et l'aide a la Recherche (F.C.A.R.) of the Quebec 
     Ministry of Education, and in part by grant OGP0023391 from the 
     Natural Sciences and Engineering Research Council of Canada.

1.  Introduction

     In his posting to the TYPES network [1989], Pottinger shows that if 
excluded middle and definite descriptions are added to Coquand's calculus of 
constructions, then any two terms in a small type (i.e., a type in Prop) are 
equal (in the sense of Leibniz equality).  This conclusion is called "proof 
degeneracy".  Although in general proof degeneracy does not imply inconsisten-
cy, it is still undesirable because it means that all terms in small types are 
identified by the logic, and hence there is no representation of a data type
(Continue reading)

Permalink | Reply | 0 comments |
headers
Paul Taylor | 1 Oct 1990 20:56
Picon

Fixed Points in Synthetic Domain Theory

Date: Mon, 1 Oct 90 19:12:57 BST

                Fixed Points in Synthetic Domain Theory

Carl Gunter's comments about the relationship between PERs and traditional
semantics of programming languages has prompted me to make the announcement
I meant to make a fortnight ago.  I strongly differ from the Pennsylvanian
point of view, though, in not considering PERs but an axiomatic approach,
of which there are many different models.

% TeX definitions
\def\E{{\cal E}}\def\imp{\Rightarrow}
\input mssymb % for the next two symbols only:
\def\natno{{\Bbb N}}\def\sigleq{\sqsubseteq}

My axiomatisation is as follows: $\E$ denotes an elementary topos with a
natural numbers object $\natno$; by a "set" I mean an object of $\E$.
If you don't like the word ``topos'', you can understand this as intuitionistic
set theory.  $\Sigma$ is a class of predicates (ie a subobject of $\Omega$)
including true and false and closed under binary conjunction and countable
(ie $\natno$-indexed) existential quantification (disjunction). This is
required to satisfy the following two axioms:
$$      \forall\sigma\in\Sigma.\lnot\lnot\Sigma\imp\Sigma        $$
(Markov's principle) and 
$$      \forall\Phi:\Sigma^\natno\to\Sigma.\Phi(\lambda n.\top)\imp
	\exists n\in\natno.\Phi(\lambda m.m\leq n)		$$
(finitary principle). The first will be assumed throughout, the second only
when stated.

Definitions:
(Continue reading)

Permalink | Reply | 0 comments |

Gmane