headers
Lawrence C Paulson | 7 Jul 1993 12:57
Picon

Co-induction by ftp


The following paper, about co-induction in Isabelle HOL, is available by
anonymous ftp from the University of Cambridge.  Instructions:

* Connect to host ftp.cl.cam.ac.uk 
* Use login id "ftp" with your internet address as password
* put ftp in BINARY MODE ("binary") 
* go to directory ml (by typing "cd ml")
* "get" the files coind.dvi.Z and coind-fig.ps.Z from that directory.  

Comments welcome!  Also please let me know if you encounter difficulties.

								Larry Paulson

	Co-induction and Co-recursion in Higher-order Logic
			Lawrence C Paulson

			     Abstract

A theory of recursive and corecursive definitions has been developed in
higher-order logic (HOL) and mechanised using Isabelle.  Least fixedpoints
express inductive data types such as strict lists; greatest fixedpoints
express co-inductive data types, such as lazy lists.  Well-founded
recursion expresses recursive functions over inductive data types;
co-recursion expresses functions that yield elements of co-inductive data
types.  The theory rests on a traditional formalization of infinite trees.

The theory is intended for use in specification and verification.  It
supports reasoning about a wide range of computable functions, but it does
not formalize their operational semantics and can express noncomputable
(Continue reading)

Permalink | Reply | 0 comments |
headers
Kim Bruce | 6 Jul 1993 10:19
Picon

OOL paper available by anonymous ftp


I would like to announce the availability via ftp of an extended abstract,
"TOIL:  Imperative object-oriented languages can be type-safe, too"
by Kim Bruce and Robert van Gent, Williams College.

This paper discusses the design of a statically-typed imperative 
object-oriented programming language which is based on a carefully-designed
formal semantics.  The natural (operational) semantics and type-checking
rules for the language are given.  A subject-reduction theorem is proved,
one consequence of which is the provable safety of the type-checking rules.
The design of this language is based on the same principles as TOOPLE,
Bruce's functional object-oriented language, which has been the subject
of several earlier papers (see for instance the POPL '93 proceedings).
In particular, the new language (TOIL - for Typed Object-oriented Imperative
Language) supports classes, objects, methods, hidden instance variables,
subclasses and subtypes.

It can be obtained via anonymous ftp at:
	angus.cs.williams.edu
Change to directory, pub/kim
Type: binary
then: get TOILPOPL.dvi

For a description of other papers available in the same directory,
get the README file.

	Kim Bruce

P.S.  I will be on vacation until the end of July, so won't be able to
respond to comments until then.
(Continue reading)

Permalink | Reply | 1 comment |
headers
Fritz Mueller | 5 Jul 1993 14:41
Picon

recursively typed lambda calculus


Full Abstraction for a Recursively Typed Lambda Calculus
with Parallel Conditional,
by Fritz M"uller, Universit"at des Saarlandes.

A copy of this report is available by snail mail from the author,
send your address to  mueller@...

Abstract:

We define the syntax and reduction relation of a recursively typed
lambda calculus with a parallel case-function (a parallel
conditional).  The reduction is shown to be confluent.  We interpret
the recursive types as information systems in a restricted form, which
we call prime systems. A denotational semantics is defined with this
interpretation. We define the syntactical normal form approximations
of a term and prove the Approximation Theorem: The semantics of a term
equals the limit of the semantics of its approximations. The proof is
by the inclusive predicate technique. The semantics is adequate with
respect to the observation of boolean values. It is also fully
abstract in the presence of the parallel case-function.
Permalink | Reply | 0 comments |
headers
Jawahar Chirimar | 18 Jul 1993 20:22

(unknown)


Hi :

I have been looking at applicative bisimulation recently. I was
wondering if anyone has used it for justifying program transformations
of interest to compiler writers. 

-Jawahar Chirimar
chirimar@...
Permalink | Reply | 0 comments |
headers
Serena Cerrito | 8 Jul 1993 18:07

limited use of exponentials


Does anybody knows something about decidability (indecidability)
results for FRAGMENTS of linear logic involving a RESTRICTED use
of EXPONENTIALS (where the ``!" modality could be applied just
to formulae of a given simple form) ?  If yes, I would greatly appreciate
any indication of papers which I could look at.

Thanks in advance.

				Serenella Cerrito

moderators note: there are a few results along these these lines.
Prop LL is undecidable even if there are only negative !, and only
wrapping "small" formulas (with two connectives (-o and either * or +) 
and three propositional atoms).  Two sided Tensor Bang LL is decidable
for arbitrary uses of !.  M. Kanovich claims constant-only prop LL
is undecidable, but hasn't published his proof yet.

	 <at> inproceedings(
CL92, 	Author = "J. Chirimar and J. Lipton",
	title = "{Provability in TBLL: A Decision Procedure}",
        Booktitle="Computer Science Logic '91",
	year = "1992",
	publisher = "{\it Lecture Notes in Computer Science, Springer}")

	 <at> article(
LMSS92,	Author="Lincoln, P. and Mitchell, J. and Scedrov, A. and Shankar, N.",
	Title="Decision Problems for Propositional Linear Logic",
	Journal="Annals Pure Appl. Logic",
	Volume="56",
(Continue reading)

Permalink | Reply | 0 comments |
headers
daniel leivant | 22 Jul 1993 03:33
Picon
Picon
Picon
Favicon

LICS'94 Call for Papers


[Since it is clearly relevant, I am distributing this conference
announcement to types.  General conference announcements should go to
the Theory-A list.  -- Philip Wadler, moderator, Types Forum.]

                    Ninth Annual IEEE Symposium on
                      LOGIC IN COMPUTER SCIENCE
                    July 4-7, 1994, Paris, France

                           CALL FOR PAPERS

The LICS symposia aim to attract high quality original papers covering 
theoretical and practical issues in computer science that relate to logic in 
a broad sense, including algebraic, categorical and topological approaches.

Suggested, but not exclusive, topics of interest include:
abstract data types, automated deduction, concurrency, constructive
mathematics, data base theory, finite model theory, knowledge representation, 
lambda and combinatory calculi, logical aspects of computational complexity, 
logics in artificial intelligence, logic programming, modal and temporal 
logics, program logic and semantics, rewrite rules, logical aspects of 
symbolic computing, problem solving environments, software specification, 
type systems, verification.

DATES:
	Submission deadline: December 13, 1993
	Notification: February 21, 1994
	Final papers due: April 15, 1994
	Conference: July 4-7, 1994
(Continue reading)

Permalink | Reply | 0 comments |
headers
Marc Bezem | 23 Jul 1993 11:24
Picon

SLNM 344, corrected ftp-address


Please distribute the following message over the type theory community.
Many thanks, Marc Bezem.
__________________________________________________________

The previous message contained an inaccessible ftp-address.  I am very
sorry to have caused this inconvenience. The fact is, that in the last
few weeks our systems group has installed a new operating system, with
many resultant changes. The message on the new edition was composed
before this change took place. Now one should ftp to

	mail@...

For the sake of completeness I give the corrected message below.
Greetings, A.S. Troelstra.
> 
> _________________________________________
> 
> The volume Metamathematical Investigation of Intuitionistic Arithmetic and
> Analysis, edited by A.S. Troelstra, which appeared in 1973 as volume 344
> of the Springer Lecture Notes in Mathematics, has been out of print for
> several years now. Since there is still a small but steady demand, it was
> decided to bring out a corrected edition as a report of the Institute for
> Logic, Language and Information of the University of Amsterdam.
> The edition is not a complete revision, but incorporates only the errata
> which have come to the notice of the editor.
> Also, it is not in any way a fancy typographical production; the original
> typescript served as a basis into which corrections have been inserted by
> hand, or pasted in, or put in a list of corrections and additions at the
> end.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Joshua Caplan | 27 Jul 1993 01:26
Picon

A question for Martin-L\"of disciples


The definition of "intensional" Martin-L\"of type theory used
by the Swedes (Nordstr\"om, Petersson, Smith, et al.) in their book
_Programming_in_Martin-L\"of's_Type_Theory_ and Simon Thompson in
_Type_Theory_and_Functional_Programming_ does not look
much like that used by Troelstra and van Dalen in _Constructivism_in_
_Mathematics,_Volume_II_.  The former group eschews the rule IExt:

		p : I(A, a, b)
	(IExt)	--------------
		  a = b : A

while the latter cheerfully include it but omit \eta and \xi.

Simon Thompson claims the decidability of judgements [british spelling]
in ML^i; Troelstra and van Dalen seem to make no claim either way about
their system, although there is a cryptic note on page 633 which refers
to the former formulation.

My questions are:

1. Are the two systems "equivalent" (are the sets of theorems in any sense
	the same)?
2. If so, how so, and if not, how solvable are judgements in the
	Troelstra/van Dalen formulation?
Permalink | Reply | 0 comments |
headers
Michel Eytan, LILoL | 27 Jul 1993 17:04

Re: SLNM 344, corrected ftp-address


At 11:24 am 23-7-93 +0200, Marc Bezem wrote:

>The previous message contained an inaccessible ftp-address.  I am very
>sorry to have caused this inconvenience. The fact is, that in the last
>few weeks our systems group has installed a new operating system, with
>many resultant changes. The message on the new edition was composed
>before this change took place. Now one should ftp to
>
>        mail@...
>
>For the sake of completeness I give the corrected message below.
>Greetings, A.S. Troelstra.

Sorry to intervene again. You cannot ftp to an e-mail address -- it's only
to a *site*. The correct ftp address is

        fwi.uva.nl
Permalink | Reply | 1 comment |
headers
Gerry Allwein | 28 Jul 1993 13:59

Banach Spaces & Linear Logic

[This digest includes three related messages.
-- Phil Wadler, moderator, Types Forum]

---------------------------------------------------------------------------
 From: Gerry Allwein <gtall@...>
 Date: Wed, 28 Jul 1993 06:59:14 -0500

Folks, does anyone know of a paper(s) relating linear logic and banach spaces?

Gerry

---------------------------------------------------------------------------
 Date: Fri, 30 Jul 93 13:00:42 EDT
 From: Richard Blute <RBLUTE@...>

Gerry Allwein asks for a reference on the relation between linear logic
and Banach spaces. At this year's MFPS conference, Prakash Panangaden, Robert
Seely and I presented a paper entitled "Holomorphic Models of Exponential
Types in Linear Logic". In this paper, we build a model of the tensor-!
fragment in the category of commutative Banach algebras. Hopefully, we will be
announcing the completed paper soon.

One of the main distinctions between Banach spaces (and Hilbert spaces)
is that the existence of a norm allows one to discuss convergent sequences,
power series (hence holomorphic functions), etc. The specific construction
we use to model ! is called Fock space. Fock space was introduced in quantum
field theory as a framework for modelling the annihilation and creation of
particles. There is a pleasing analogy here between such ideas and that
of infinitely renewable resource.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane