6 Sep 23:08 1990

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


10 Sep 17:31 1990

### 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?


21 Sep 19:09 1990

### 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.
there some obvious observations one can make based
on what is known about the untyped lambda calculus?

carl gunter


21 Sep 19:17 1990

### 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


22 Sep 16:53 1990

### Re: PER's and operational semantics

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

<9009211709.AA07500 <at> stork>
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,

John


23 Sep 04:11 1990

### 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


27 Sep 20:46 1990

### 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
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


1 Oct 20:56 1990

### Fixed Points in Synthetic Domain Theory

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

Fixed Points in Synthetic Domain Theory

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: