.nr PS 11
.nr VS 14
.so roff.defs
.nr P 1 Presentation Flag
.nr D 0 Document Flag
.LP
.TL
Problems in Logical Foundations for Computer Science
.AU
Roger Bishop Jones
.AI
ICL Defence Systems
.AB
.ct D
Abstract for papers
.cx
.ct P
This presentation identifies some problems in Computer Science
which might benefit from new approaches to logical foundations.
.cx
.AE
.ds LH \s-8DTC/RBJ/048\s+8
.ds CH \s-8Foundation Problems\s+8
.ds RH \s-8Page \\n(PN\s+8
.ds LF \s-8DTC/RBJ/048\s+8
.ds CF \s-8Foundation Problems\s+8
.ds RF \s-8\1987-03-12\s+8
.nr PS 30
.nr VS 34
.KS
.DS C
\f(HBWANTED\fP
.DE


.nr PS 24
.nr VS 24
.DS C
GOOD FOUNDATIONS with \f(HBtype:type\fP
.DE
.nr PS 30
.nr VS 34
.DS C


\f(HBWHY?\fP

.nr PS 20
.nr VS 24
.DE
.LP
.IP "\f(HBWe NEED\fP:"
Specification languages supporting formal reasoning which
are closely integrated with programming languages.

.IP \f(HBSUGGESTS\fP:
enrich type system to enable types to serve as specifications.

.IP \f(HBBUT..\fP
programming languages need \f(HItype:type\fP
.KE
.KS
.nr PS 26
.nr VS 30
.DS C
\f(HBWhat is a FOUNDATION SYSTEM?\fP


\f(HBFOUNDATION

=

LOGIC + ONTOLOGY\fP

.DE
.nr PS 20
.nr VS 24
.LP
\f(HIParadoxes\fP arise from \f(HIontological\fP assumptions,
therefore these should be settled before
we begin to do mathematics.


.LP
This allows questions of consistency to be dealt
with by logicians, rather than software engineers.
.DS


\f(HBDON'T\fP:	add axioms to a logic

\f(HBDO\fP:	add definitions to a foundation system
.DE
.KE
.KS
.nr PS 26
.nr VS 30
.DS C
\f(HBSPECIFICATION LANGUAGES
are
FOUNDATION SYSTEMS\fP

.DE
.nr PS 20
.nr VS 24
.LP
e.g., loosely:

.DS L
\f(HBZ\fP		a derivative of first order set theory

		but semantics fails to give an account of recursive types

\f(HBVDM\fP		used to be described as "set theory"

		but semantics uses "BQM spaces"

\f(HBHOL\fP		(\f(HBH\fPigher \f(HBO\fPrder \f(HBL\fPogic)
		based on Church's type theory.
.DE
.KE
.KS
.nr PS 26
.nr VS 30
.DS C
\f(HBWhy
PROGRAMMING LANGUAGES
need\fP \f(HItype:type\fP

.DE
.nr PS 20
.nr VS 24
.DS C
PERSISTENCE

MODULARITY

TYPE INHERITANCE

DEPENDENT TYPES


.DE
.nr PS 26
.nr VS 30
.DS C
\f(HBOther Related Needs

.DE
.nr PS 20
.nr VS 24
.DS C
DENOTATIONAL SEMANTICS

PARAMETERISATION of SPECIFICATIONS

"POLYMORPHISM"

SELF-APPLICATION
.DE
.KE
.KS
.nr PS 24
.nr VS 28
.DS C
\f(HBSOME RELEVANT WORK\fP


\f(HIFoundations\fP
***************


.DE
.nr PS 20
.nr VS 24
.DS C
\f(HBMartin-Lof\fP  -  Intuitionistic Type Theory

\f(HBConstable\fP et.al.  -  NUPRL

\f(HBCoquand & Huet\fP  -  The Calculus of Constructions

\f(HBPeter Aczel\fP - Logical Theory of Constructions



.DE
.nr PS 24
.nr VS 28
.DS C
\f(HIProgramming Languages\fP
***************************


.DE
.nr PS 20
.nr VS 24
.DS C
\f(HBCardelli\fP's semantics for type:type
.DE
.KE